# HG changeset patch
# User wenzelm
# Date 1483700309 -3600
# Node ID ddbb89e7621d7c522563289513e36dd7d5c3be04
# Parent  05b29c8f0addbf7ad7b00c5b7810ffab8a35e920
tuned signature;

diff -r 05b29c8f0add -r ddbb89e7621d src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Jan 05 22:57:59 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Jan 06 11:58:29 2017 +0100
@@ -120,7 +120,7 @@
           (for {
             (file, model) <- st.models.iterator
             if changed_files(file) && model.external_file
-            text <- try_read(file)
+            text <- read_file_content(file)
             model1 <- model.update_text(text)
           } yield (file, model1)).toList
         if (changed_models.isEmpty) (false, st)
@@ -133,14 +133,14 @@
 
   /* file content */
 
-  def try_read(file: JFile): Option[String] =
+  def read_file_content(file: JFile): Option[String] =
     try { Some(Line.normalize(File.read(file))) }
     catch { case ERROR(_) => None }
 
   def get_file_content(file: JFile): Option[String] =
     get_model(file) match {
       case Some(model) => Some(model.doc.make_text)
-      case None => try_read(file)
+      case None => read_file_content(file)
     }
 
 
@@ -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); try_read(file) }
+            text <- { watcher.register_parent(file); read_file_content(file) }
           }
           yield {
             val model = Document_Model.init(session, node_name)