--- a/src/Tools/VSCode/src/server.scala Sun Mar 05 14:33:43 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala Sun Mar 05 14:43:39 2017 +0100
@@ -128,20 +128,18 @@
{
if (resources.close_model(file)) {
file_watcher.register_parent(file)
- if (!sync_documents(Set(file))) {
- delay_input.invoke()
- delay_output.invoke()
- }
+ sync_documents(Set(file))
+ delay_input.invoke()
+ delay_output.invoke()
}
}
- private def sync_documents(changed: Set[JFile]): Boolean =
- if (resources.sync_models(changed)) {
- delay_input.invoke()
- delay_output.invoke()
- true
- }
- else false
+ private def sync_documents(changed: Set[JFile])
+ {
+ resources.sync_models(changed)
+ delay_input.invoke()
+ delay_output.invoke()
+ }
private def update_document(file: JFile, text: String)
{
--- a/src/Tools/VSCode/src/vscode_resources.scala Sun Mar 05 14:33:43 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Mar 05 14:43:39 2017 +0100
@@ -131,8 +131,8 @@
case Some(model) => (true, st.update_models(Some(file -> model.external(true))))
})
- def sync_models(changed_files: Set[JFile]): Boolean =
- state.change_result(st =>
+ def sync_models(changed_files: Set[JFile]): Unit =
+ state.change(st =>
{
val changed_models =
(for {
@@ -140,9 +140,8 @@
if changed_files(file) && model.external_file
text <- read_file_content(file)
model1 <- model.update_text(text)
- } yield (file, model1)).toMap
- if (changed_models.isEmpty) (false, st)
- else (true, st.update_models(changed_models))
+ } yield (file, model1)).toList
+ st.update_models(changed_models)
})