@@ -10,10 +10,18 @@ export class DiagnosticProvider {
1010        private  diagnosticCollection : vscode . DiagnosticCollection , 
1111    )  { 
1212        rtlDebugger . onDidChangeSession ( ( session )  =>  { 
13-             this . update ( session ) ; 
14-             if  ( session  !==  null )  { 
15-                 session . onDidChangeSimulationStatus ( ( _simulationStatus )  =>  this . update ( session ) ) ; 
16-                 session . onDidChangeTimeCursor ( ( _timeCursor )  =>  this . update ( session ) ) ; 
13+             if  ( session  ===  null )  { 
14+                 this . clear ( ) ; 
15+             }  else  { 
16+                 session . onDidChangeSimulationStatus ( ( simulationStatus )  =>  { 
17+                     if  ( simulationStatus . status  ===  'running' )  { 
18+                         this . clear ( ) ; 
19+                     } 
20+                 } ) ; 
21+                 session . onDidChangeTimeCursor ( ( _timeCursor )  =>  { 
22+                     this . request ( session ) ; 
23+                 } ) ; 
24+                 this . request ( session ) ; 
1725            } 
1826        } ) ; 
1927    } 
@@ -22,17 +30,20 @@ export class DiagnosticProvider {
2230        this . diagnosticCollection . dispose ( ) ; 
2331    } 
2432
25-     private  async  update ( session :  Session   |   null )  { 
26-         if   ( session   ===   null   ||   session ?. simulationStatus . status   ===   'running' )   { 
27-              this . apply ( [ ] ) ; 
28-          }   else   { 
29-              const   sample   =   await   session . queryAtCursor ( {   diagnostics :  true   } ) ; 
30-              this . apply ( sample . diagnostics ! ) ; 
31-         } 
33+     private  async  clear ( )  { 
34+         this . apply ( [ ] ) ; 
35+     } 
36+ 
37+     private   async   request ( session :  Session )   { 
38+         const   sample   =   await   session . queryAtCursor ( {   diagnostics :  true   } ) ; 
39+         this . apply ( sample . diagnostics ! ) ; 
3240    } 
3341
3442    private  apply ( diagnostics : Diagnostic [ ] )  { 
3543        const  diagnosticMap  =  new  Map ( ) ; 
44+         let  mostImportantDiagnostic  =  null ; 
45+         let  mostImportantDiagnosticSeverity  =  vscode . DiagnosticSeverity . Hint ; 
46+         let  multipleImportantDiagnostics  =  false ; 
3647        for  ( const  diagnostic  of  diagnostics )  { 
3748            if  ( diagnostic . location  ===  null )  { 
3849                continue ; 
@@ -85,6 +96,17 @@ export class DiagnosticProvider {
8596                    severity  =  vscode . DiagnosticSeverity . Error ; 
8697                    break ; 
8798            } 
99+             if  ( severity  !==  vscode . DiagnosticSeverity . Information  &&  diagnostic . location  !==  null )  { 
100+                 // Prioritize assertions/assumptions over breakpoints. (It's unclear whether this 
101+                 // specific prioritization is the best one, but one of them should probably take 
102+                 // priority over the other.) 
103+                 multipleImportantDiagnostics  =  ( mostImportantDiagnostic  !==  null ) ; 
104+                 if  ( severity  <  mostImportantDiagnosticSeverity )  { 
105+                     mostImportantDiagnostic  =  diagnostic ; 
106+                     mostImportantDiagnosticSeverity  =  severity ; 
107+                 } 
108+             } 
109+ 
88110            if  ( message  !==  '' )  { 
89111                const  mappedDiagnostic  =  new  vscode . Diagnostic ( range ,  message ,  severity ) ; 
90112                mappedDiagnostic . code  =  < string > diagnostic . type ; 
@@ -95,5 +117,18 @@ export class DiagnosticProvider {
95117
96118        this . diagnosticCollection . clear ( ) ; 
97119        this . diagnosticCollection . set ( Array . from ( diagnosticMap . entries ( ) ) ) ; 
120+ 
121+         if  ( mostImportantDiagnostic  !==  null )  { 
122+             this . focus ( mostImportantDiagnostic ,  multipleImportantDiagnostics ) ; 
123+         } 
124+     } 
125+ 
126+     private  async  focus ( diagnostic : Diagnostic ,  showDiagnosticsPane : boolean  =  false )  { 
127+         if  ( showDiagnosticsPane )  { 
128+             await  vscode . commands . executeCommand ( 'workbench.actions.view.problems' ) ; 
129+         } 
130+         // 2024-11-14: Upsettingly, this is the best (and, more or less, only) way to expand a diagnostic. 
131+         await  vscode . window . showTextDocument ( ...diagnostic . location ! . openCommandArguments ( ) ) ; 
132+         await  vscode . commands . executeCommand ( 'editor.action.marker.next' ) ; 
98133    } 
99134} 
0 commit comments