# HG changeset patch
# User wenzelm
# Date 1505751546 -7200
# Node ID 39db5bb7eb0a92a26250a18f8d1c2b202bb9a26c
# Parent  6f4613dbfef6c9a492cc465c3e147f56cb645e2e
recode Unicode text on the spot, e.g. from copy-paste of output;

diff -r 6f4613dbfef6 -r 39db5bb7eb0a src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Mon Sep 18 18:11:21 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Mon Sep 18 18:19:06 2017 +0200
@@ -45,6 +45,16 @@
     lazy val bibtex_entries: List[Text.Info[String]] =
       try { Bibtex.entries(text) }
       catch { case ERROR(_) => Nil }
+
+    def recode_symbols: List[Protocol.TextEdit] =
+      (for {
+        (line, l) <- doc.lines.iterator.zipWithIndex
+        text1 = Symbol.encode(line.text)
+        if (line.text != text1)
+      } yield {
+        val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length))
+        Protocol.TextEdit(range, text1)
+      }).toList
   }
 
   def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
@@ -166,12 +176,27 @@
     }
   }
 
-  def flush_edits(doc_blobs: Document.Blobs, caret: Option[Line.Position])
-    : Option[(List[Document.Edit_Text], Document_Model)] =
+  def flush_edits(
+      unicode_symbols: Boolean,
+      doc_blobs: Document.Blobs,
+      file: JFile,
+      caret: Option[Line.Position])
+    : Option[((List[Protocol.TextDocumentEdit], List[Document.Edit_Text]), Document_Model)] =
   {
+    val workspace_edits =
+      if (unicode_symbols && version.isDefined) {
+        val edits = content.recode_symbols
+        if (edits.nonEmpty) List(Protocol.TextDocumentEdit(file, version.get, edits))
+        else Nil
+      }
+      else Nil
+
     val (reparse, perspective) = node_perspective(doc_blobs, caret)
-    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
-      val edits = node_edits(node_header, pending_edits, perspective)
+    if (reparse || pending_edits.nonEmpty || last_perspective != perspective ||
+        workspace_edits.nonEmpty)
+    {
+      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)))
     }
     else None
diff -r 6f4613dbfef6 -r 39db5bb7eb0a src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Sep 18 18:11:21 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Mon Sep 18 18:19:06 2017 +0200
@@ -123,7 +123,7 @@
 
   private val delay_input: Standard_Thread.Delay =
     Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
-    { resources.flush_input(session) }
+    { resources.flush_input(session, channel) }
 
   private val delay_load: Standard_Thread.Delay =
     Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
@@ -487,7 +487,7 @@
     /* session */
 
     override def session: Session = server.session
-    override def flush(): Unit = resources.flush_input(session)
+    override def flush(): Unit = resources.flush_input(session, channel)
     override def invoke(): Unit = delay_input.invoke()
 
 
diff -r 6f4613dbfef6 -r 39db5bb7eb0a src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 18 18:11:21 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 18 18:19:06 2017 +0200
@@ -258,7 +258,7 @@
 
   /* pending input */
 
-  def flush_input(session: Session)
+  def flush_input(session: Session, channel: Channel)
   {
     state.change(st =>
       {
@@ -266,10 +266,15 @@
           (for {
             file <- st.pending_input.iterator
             model <- st.models.get(file)
-            (edits, model1) <- model.flush_edits(st.document_blobs, st.get_caret(file))
+            (edits, model1) <-
+              model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file))
           } yield (edits, (file, model1))).toList
 
-        session.update(st.document_blobs, changed_models.flatMap(_._1))
+        for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
+          channel.write(Protocol.WorkspaceEdit(workspace_edits))
+
+        session.update(st.document_blobs, changed_models.flatMap(res => res._1._2))
+
         st.copy(
           models = st.models ++ changed_models.iterator.map(_._2),
           pending_input = Set.empty)