--- a/src/Tools/VSCode/src/server.scala Sat Dec 31 14:27:07 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala Sat Dec 31 14:29:16 2016 +0100
@@ -127,7 +127,7 @@
}
private def sync_external(changed: Set[JFile]): Unit =
- if (resources.sync_external(changed)) delay_input.invoke()
+ if (resources.sync_models(changed)) delay_input.invoke()
private val watcher = File_Watcher(sync_external(_))
--- a/src/Tools/VSCode/src/vscode_resources.scala Sat Dec 31 14:27:07 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Dec 31 14:29:16 2016 +0100
@@ -89,7 +89,7 @@
(Some(model), st.copy(models = st.models + (uri -> model.copy(external = true))))
})
- def sync_external(changed_files: Set[JFile]): Boolean =
+ def sync_models(changed_files: Set[JFile]): Boolean =
state.change_result(st =>
{
val changed_models =