# HG changeset patch
# User wenzelm
# Date 1483606526 -3600
# Node ID 22a1b061ae15bb9459a30e5bbb4e696d8cb9a3c2
# Parent  067cacdd1117665d612af8e1a4ec70469dbfc4bb
tuned;

diff -r 067cacdd1117 -r 22a1b061ae15 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Jan 04 21:28:33 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Jan 05 09:55:26 2017 +0100
@@ -147,8 +147,7 @@
             dep <- thy_info.dependencies("", thys).deps.iterator
             file = node_file(dep.name)
             if !st.models.isDefinedAt(file)
-            _ = watcher.register_parent(file)
-            text <- try_read(file)
+            text <- { watcher.register_parent(file); try_read(file) }
           }
           yield {
             val model = Document_Model.init(session, node_name(file))