src/Tools/VSCode/src/vscode_resources.scala
changeset 66676 39db5bb7eb0a
parent 66674 30d5195299e2
child 66714 9fc4e144693c
     1.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 18 18:11:21 2017 +0200
     1.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 18 18:19:06 2017 +0200
     1.3 @@ -258,7 +258,7 @@
     1.4  
     1.5    /* pending input */
     1.6  
     1.7 -  def flush_input(session: Session)
     1.8 +  def flush_input(session: Session, channel: Channel)
     1.9    {
    1.10      state.change(st =>
    1.11        {
    1.12 @@ -266,10 +266,15 @@
    1.13            (for {
    1.14              file <- st.pending_input.iterator
    1.15              model <- st.models.get(file)
    1.16 -            (edits, model1) <- model.flush_edits(st.document_blobs, st.get_caret(file))
    1.17 +            (edits, model1) <-
    1.18 +              model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file))
    1.19            } yield (edits, (file, model1))).toList
    1.20  
    1.21 -        session.update(st.document_blobs, changed_models.flatMap(_._1))
    1.22 +        for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
    1.23 +          channel.write(Protocol.WorkspaceEdit(workspace_edits))
    1.24 +
    1.25 +        session.update(st.document_blobs, changed_models.flatMap(res => res._1._2))
    1.26 +
    1.27          st.copy(
    1.28            models = st.models ++ changed_models.iterator.map(_._2),
    1.29            pending_input = Set.empty)