src/Tools/VSCode/src/server.scala
changeset 64722 6df73de0d3c7
parent 64720 8cc2d7c4ada1
child 64724 44dbf8cc2d7f
equal deleted inserted replaced
64721:4b9c96c3850b 64722:6df73de0d3c7
   125       case None =>
   125       case None =>
   126     }
   126     }
   127   }
   127   }
   128 
   128 
   129   private def sync_external(changed: Set[JFile]): Unit =
   129   private def sync_external(changed: Set[JFile]): Unit =
   130     if (resources.sync_external(changed)) delay_input.invoke()
   130     if (resources.sync_models(changed)) delay_input.invoke()
   131 
   131 
   132   private val watcher = File_Watcher(sync_external(_))
   132   private val watcher = File_Watcher(sync_external(_))
   133 
   133 
   134 
   134 
   135   /* input from client */
   135   /* input from client */