lsp: clarified preview_request;
authorThomas Lindae <thomas.lindae@in.tum.de>
Fri, 03 May 2024 11:10:58 +0200
changeset 81031 c9e8461dd5f2
parent 81030 88879ff1cef5
child 81032 de94fcfbc3ce
lsp: clarified preview_request;
src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Thu May 09 23:05:10 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Fri May 03 11:10:58 2024 +0200
@@ -197,7 +197,7 @@
       if (preview_panel.flush(channel)) delay_preview.invoke()
     }
 
-  private def request_preview(file: JFile, column: Int): Unit = {
+  private def preview_request(file: JFile, column: Int): Unit = {
     preview_panel.request(file, column)
     delay_preview.invoke()
   }
@@ -457,7 +457,7 @@
           case LSP.State_Auto_Update(state_id, enabled) => State_Panel.auto_update(state_id, enabled)
           case LSP.State_Set_Margin(state_id, margin) => State_Panel.set_margin(state_id, margin)
           case LSP.Symbols_Request(id) => symbols_request(id)
-          case LSP.Preview_Request(file, column) => request_preview(file, column)
+          case LSP.Preview_Request(file, column) => preview_request(file, column)
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }