# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1714727458 -7200
# Node ID c9e8461dd5f246d36ebc74ae726cb3f90cd1a60d
# Parent  88879ff1cef57c38d7fc29be649d7bbac4bbdd58
lsp: clarified preview_request;

diff -r 88879ff1cef5 -r c9e8461dd5f2 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")
         }
       }