File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -159,6 +159,9 @@ div.is-busy-unused {
159159# error_alert_msg {
160160 margin-right : 2em ;
161161}
162+ # error_alert_msg a {
163+ cursor : pointer;
164+ }
162165div .menu_div {
163166 position : absolute;
164167 width : 200px ;
Original file line number Diff line number Diff line change @@ -870,7 +870,7 @@ function getErrorElement(err: WorkerError) {
870870 link . click ( ( ev ) => {
871871 var wnd = projectWindows . createOrShow ( path ) ;
872872 if ( wnd instanceof SourceEditor ) {
873- wnd . setCurrentLine ( err , true ) ;
873+ wnd . navigateToLine ( err . line ) ;
874874 }
875875 } ) ;
876876 }
Original file line number Diff line number Diff line change @@ -341,6 +341,19 @@ export class SourceEditor implements ProjectView {
341341 } ) ;
342342 }
343343
344+ navigateToLine ( line : number ) {
345+ if ( line < 1 || line > this . editor . state . doc . lines ) return ;
346+ const targetLine = this . editor . state . doc . line ( line ) ;
347+ this . editor . dispatch ( {
348+ selection : { anchor : targetLine . from } ,
349+ effects : [
350+ highlightLines . effect . of ( { start : line , end : line } ) ,
351+ EditorView . scrollIntoView ( targetLine . from , { y : "center" } ) ,
352+ ] ,
353+ } ) ;
354+ this . editor . focus ( ) ;
355+ }
356+
344357 getValue ( ) : string {
345358 return this . editor . state . doc . toString ( ) ;
346359 }
Original file line number Diff line number Diff line change @@ -71,7 +71,7 @@ export class ProjectWindows {
7171 this . refreshErrors ( ) ;
7272 wnd . setVisible && wnd . setVisible ( true ) ;
7373 this . id2showfn [ id ] && this . id2showfn [ id ] ( id , wnd ) ;
74- } else {
74+ } else if ( moveCursor ) {
7575 this . refresh ( moveCursor ) ;
7676 }
7777 this . activeid = id ;
You can’t perform that action at this time.
0 commit comments