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);
authorwenzelm
Wed, 07 Nov 2018 22:15:03 +0100
changeset 69256 c78c95d2a3d1
parent 69255 800b1ce96fce
child 69257 039edba27102
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);
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/VSCode/src/vscode_resources.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)
--- 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)