# HG changeset patch
# User wenzelm
# Date 1541625303 -3600
# Node ID c78c95d2a3d1beaad7489d2c198b8ed557ad4a66
# Parent  800b1ce96fce617ffe3000ac489789896346aaa5
more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);

diff -r 800b1ce96fce -r c78c95d2a3d1 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Nov 07 21:42:16 2018 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Nov 07 22:15:03 2018 +0100
@@ -264,7 +264,7 @@
     yield {
       Line.Node_Range(file.getPath,
         if (range.start > 0) {
-          resources.get_file_content(file) match {
+          resources.get_file_content(resources.node_name(file)) match {
             case Some(text) =>
               val chunk = Symbol.Text_Chunk(text)
               val doc = Line.Document(text)
diff -r 800b1ce96fce -r c78c95d2a3d1 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Nov 07 21:42:16 2018 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Nov 07 22:15:03 2018 +0100
@@ -121,16 +121,18 @@
 
   /* file content */
 
-  def read_file_content(file: JFile): Option[String] =
+  def read_file_content(name: Document.Node.Name): Option[String] =
   {
-    try { Some(Line.normalize(File.read(file))) }
-    catch { case ERROR(_) => None }
+    make_theory_content(name) orElse {
+      try { Some(Line.normalize(File.read(node_file(name)))) }
+      catch { case ERROR(_) => None }
+    }
   }
 
-  def get_file_content(file: JFile): Option[String] =
-    get_model(file) match {
+  def get_file_content(name: Document.Node.Name): Option[String] =
+    get_model(name) match {
       case Some(model) => Some(model.content.text)
-      case None => read_file_content(file)
+      case None => read_file_content(name)
     }
 
   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
@@ -186,7 +188,7 @@
           (for {
             (file, model) <- st.models.iterator
             if changed_files(file) && model.external_file
-            text <- read_file_content(file)
+            text <- read_file_content(model.node_name)
             model1 <- model.change_text(text)
           } yield (file, model1)).toList
         st.update_models(changed_models)
@@ -250,7 +252,7 @@
             node_name <- thy_files1.iterator ++ thy_files2.iterator ++ aux_files.iterator
             file = node_file(node_name)
             if !st.models.isDefinedAt(file)
-            text <- { file_watcher.register_parent(file); read_file_content(file) }
+            text <- { file_watcher.register_parent(file); read_file_content(node_name) }
           }
           yield {
             val model = Document_Model.init(session, editor, node_name)