# HG changeset patch
# User wenzelm
# Date 1488721657 -3600
# Node ID 29c19bc97d201a1979ce51838d9f36df9e4ba576
# Parent  06d9bcb66ef3d9fb2300aa305dd57da98da4b6a8
tuned;

diff -r 06d9bcb66ef3 -r 29c19bc97d20 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 05 14:43:39 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 05 14:47:37 2017 +0100
@@ -187,7 +187,7 @@
             val model = Document_Model.init(session, node_name)
             val model1 = (model.update_text(text) getOrElse model).external(true)
             (file, model1)
-          }).toMap
+          }).toList
 
         val invoke_input = loaded_models.nonEmpty
         val invoke_load = stable_tip_version.isEmpty