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 Nov 07 22:15:03 2018 +0100 (6 months ago)
changeset 69256c78c95d2a3d1
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
     1.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Nov 07 21:42:16 2018 +0100
     1.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Nov 07 22:15:03 2018 +0100
     1.3 @@ -264,7 +264,7 @@
     1.4      yield {
     1.5        Line.Node_Range(file.getPath,
     1.6          if (range.start > 0) {
     1.7 -          resources.get_file_content(file) match {
     1.8 +          resources.get_file_content(resources.node_name(file)) match {
     1.9              case Some(text) =>
    1.10                val chunk = Symbol.Text_Chunk(text)
    1.11                val doc = Line.Document(text)
     2.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Nov 07 21:42:16 2018 +0100
     2.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Nov 07 22:15:03 2018 +0100
     2.3 @@ -121,16 +121,18 @@
     2.4  
     2.5    /* file content */
     2.6  
     2.7 -  def read_file_content(file: JFile): Option[String] =
     2.8 +  def read_file_content(name: Document.Node.Name): Option[String] =
     2.9    {
    2.10 -    try { Some(Line.normalize(File.read(file))) }
    2.11 -    catch { case ERROR(_) => None }
    2.12 +    make_theory_content(name) orElse {
    2.13 +      try { Some(Line.normalize(File.read(node_file(name)))) }
    2.14 +      catch { case ERROR(_) => None }
    2.15 +    }
    2.16    }
    2.17  
    2.18 -  def get_file_content(file: JFile): Option[String] =
    2.19 -    get_model(file) match {
    2.20 +  def get_file_content(name: Document.Node.Name): Option[String] =
    2.21 +    get_model(name) match {
    2.22        case Some(model) => Some(model.content.text)
    2.23 -      case None => read_file_content(file)
    2.24 +      case None => read_file_content(name)
    2.25      }
    2.26  
    2.27    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    2.28 @@ -186,7 +188,7 @@
    2.29            (for {
    2.30              (file, model) <- st.models.iterator
    2.31              if changed_files(file) && model.external_file
    2.32 -            text <- read_file_content(file)
    2.33 +            text <- read_file_content(model.node_name)
    2.34              model1 <- model.change_text(text)
    2.35            } yield (file, model1)).toList
    2.36          st.update_models(changed_models)
    2.37 @@ -250,7 +252,7 @@
    2.38              node_name <- thy_files1.iterator ++ thy_files2.iterator ++ aux_files.iterator
    2.39              file = node_file(node_name)
    2.40              if !st.models.isDefinedAt(file)
    2.41 -            text <- { file_watcher.register_parent(file); read_file_content(file) }
    2.42 +            text <- { file_watcher.register_parent(file); read_file_content(node_name) }
    2.43            }
    2.44            yield {
    2.45              val model = Document_Model.init(session, editor, node_name)