# HG changeset patch
# User wenzelm
# Date 1483181124 -3600
# Node ID 55c871fc39e3fb9d48aedceada0e1d223b9bb460
# Parent  3197b68f43147f6292528b3529cda8c0ec62300c
tuned;

diff -r 3197b68f4314 -r 55c871fc39e3 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Dec 31 11:43:06 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Dec 31 11:45:24 2016 +0100
@@ -92,14 +92,14 @@
   def sync_external(changed_files: Set[JFile]): Boolean =
     state.change_result(st =>
       {
-        val changed =
+        val changed_models =
           (for {
             (uri, model) <- st.models.iterator
             if changed_files(model.file)
             model1 <- model.update_file
           } yield (uri, model)).toList
-        if (changed.isEmpty) (false, st)
-        else (true, st.copy(models = (st.models /: changed)(_ + _)))
+        if (changed_models.isEmpty) (false, st)
+        else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
       })
 
 
@@ -109,16 +109,16 @@
   {
     state.change(st =>
       {
-        val changed =
+        val changed_models =
           (for {
             uri <- st.pending_input.iterator
             model <- st.models.get(uri)
             res <- model.flush_edits
           } yield res).toList
 
-        session.update(Document.Blobs.empty, changed.flatMap(_._1))
+        session.update(Document.Blobs.empty, changed_models.flatMap(_._1))
         st.copy(
-          models = (st.models /: changed) { case (ms, (_, m)) => ms + (m.uri -> m) },
+          models = (st.models /: changed_models) { case (ms, (_, m)) => ms + (m.uri -> m) },
           pending_input = Set.empty)
       })
   }