# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1719754365 -7200
# Node ID a5d42b37331fdd50e612c8897041b555ef5139b1
# Parent  b2df8bf17071247dcd0e802535a0490b19aa8ea1
lsp: removed code that is never run;

diff -r b2df8bf17071 -r a5d42b37331f src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Sun Jun 30 15:32:39 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_model.scala	Sun Jun 30 15:32:45 2024 +0200
@@ -176,25 +176,15 @@
   }
 
   def flush_edits(
-      unicode_symbols: Boolean,
       doc_blobs: Document.Blobs,
       file: JFile,
       caret: Option[Line.Position]
-  ): Option[((List[LSP.TextDocumentEdit], List[Document.Edit_Text]), VSCode_Model)] = {
-    val workspace_edits =
-      if (unicode_symbols && version.isDefined) {
-        val edits = content.recode_symbols
-        if (edits.nonEmpty) List(LSP.TextDocumentEdit(file, version.get, edits))
-        else Nil
-      }
-      else Nil
-
+  ): Option[(List[Document.Edit_Text], VSCode_Model)] = {
     val (reparse, perspective) = node_perspective(doc_blobs, caret)
-    if (reparse || pending_edits.nonEmpty || last_perspective != perspective ||
-        workspace_edits.nonEmpty) {
+    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
       val prover_edits = node_edits(node_header, pending_edits, perspective)
-      val edits = (workspace_edits, prover_edits)
-      Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
+      val edits = (prover_edits)
+      Some(edits, copy(pending_edits = Nil, last_perspective = perspective))
     }
     else None
   }
diff -r b2df8bf17071 -r a5d42b37331f src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Jun 30 15:32:39 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Jun 30 15:32:45 2024 +0200
@@ -276,13 +276,10 @@
           file <- st.pending_input.iterator
           model <- st.models.get(file)
           (edits, model1) <-
-            model.flush_edits(false, st.document_blobs, file, st.get_caret(file))
+            model.flush_edits(st.document_blobs, file, st.get_caret(file))
         } yield (edits, (file, model1))).toList
 
-      for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
-        channel.write(LSP.WorkspaceEdit(workspace_edits))
-
-      session.update(st.document_blobs, changed_models.flatMap(res => res._1._2))
+      session.update(st.document_blobs, changed_models.flatMap(res => res._1))
 
       st.copy(
         models = st.models ++ changed_models.iterator.map(_._2),