--- a/src/Tools/VSCode/src/server.scala Wed Jan 04 22:31:40 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala Wed Jan 04 22:57:39 2017 +0100
@@ -116,7 +116,7 @@
private val delay_load =
Standard_Thread.delay_last(options.seconds("vscode_load_delay"))
- { if (resources.resolve_dependencies(session)) delay_input.invoke() }
+ { if (resources.resolve_dependencies(session, watcher)) delay_input.invoke() }
private val watcher =
File_Watcher(sync_documents(_), options.seconds("vscode_load_delay"))
--- a/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 04 22:31:40 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 04 22:57:39 2017 +0100
@@ -134,7 +134,7 @@
val thy_info = new Thy_Info(this)
- def resolve_dependencies(session: Session): Boolean =
+ def resolve_dependencies(session: Session, watcher: File_Watcher): Boolean =
{
state.change_result(st =>
{
@@ -147,6 +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)
}
yield {