# HG changeset patch
# User wenzelm
# Date 1483995099 -3600
# Node ID 316d703f741d999d546cda1e44c0c2df4eb06669
# Parent  5e9bf964510a4308f112f282008a051c998b23a9
tuned;

diff -r 5e9bf964510a -r 316d703f741d src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Jan 09 20:47:45 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Mon Jan 09 21:51:39 2017 +0100
@@ -116,12 +116,12 @@
 
   private val delay_load: Standard_Thread.Delay =
     Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
-      val (invoke_input, invoke_load) = resources.resolve_dependencies(session, watcher)
+      val (invoke_input, invoke_load) = resources.resolve_dependencies(session, file_watcher)
       if (invoke_input) delay_input.invoke()
       if (invoke_load) delay_load.invoke
     }
 
-  private val watcher =
+  private val file_watcher =
     File_Watcher(sync_documents(_), options.seconds("vscode_load_delay"))
 
   private def sync_documents(changed: Set[JFile]): Unit =
@@ -137,7 +137,7 @@
   {
     resources.close_model(file) match {
       case Some(model) =>
-        watcher.register_parent(file)
+        file_watcher.register_parent(file)
         sync_documents(Set(file))
       case None =>
     }
@@ -263,7 +263,7 @@
         session.stop()
         delay_input.revoke()
         delay_output.revoke()
-        watcher.shutdown()
+        file_watcher.shutdown()
         None
       case None =>
         reply("Prover inactive")
diff -r 5e9bf964510a -r 316d703f741d src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Jan 09 20:47:45 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Jan 09 21:51:39 2017 +0100
@@ -148,7 +148,7 @@
 
   /* resolve dependencies */
 
-  def resolve_dependencies(session: Session, watcher: File_Watcher): (Boolean, Boolean) =
+  def resolve_dependencies(session: Session, file_watcher: File_Watcher): (Boolean, Boolean) =
   {
     state.change_result(st =>
       {
@@ -182,7 +182,7 @@
             node_name <- thy_files.iterator ++ aux_files.iterator
             file = node_file(node_name)
             if !st.models.isDefinedAt(file)
-            text <- { watcher.register_parent(file); read_file_content(file) }
+            text <- { file_watcher.register_parent(file); read_file_content(file) }
           }
           yield {
             val model = Document_Model.init(session, node_name)