more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
authorwenzelm
Wed Nov 07 21:42:16 2018 +0100 (6 months ago)
changeset 69255800b1ce96fce
parent 69254 9f8d26b8c731
child 69256 c78c95d2a3d1
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
etc/settings
lib/scripts/getfunctions
src/Pure/PIDE/document.scala
src/Pure/PIDE/document_status.scala
src/Pure/PIDE/headless.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/bibtex.scala
src/Pure/Thy/file_format.scala
src/Pure/Thy/present.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_header.scala
src/Pure/build-jars
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/preview_panel.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/etc/settings	Wed Nov 07 14:06:43 2018 +0100
     1.2 +++ b/etc/settings	Wed Nov 07 21:42:16 2018 +0100
     1.3 @@ -20,6 +20,8 @@
     1.4  
     1.5  classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
     1.6  
     1.7 +isabelle_file_format 'isabelle.Bibtex$File_Format'
     1.8 +
     1.9  #paranoia settings -- avoid intrusion of alien options
    1.10  unset "_JAVA_OPTIONS"
    1.11  unset "JAVA_TOOL_OPTIONS"
     2.1 --- a/lib/scripts/getfunctions	Wed Nov 07 14:06:43 2018 +0100
     2.2 +++ b/lib/scripts/getfunctions	Wed Nov 07 21:42:16 2018 +0100
     2.3 @@ -109,6 +109,22 @@
     2.4  }
     2.5  export -f classpath
     2.6  
     2.7 +#file formats
     2.8 +function isabelle_file_format ()
     2.9 +{
    2.10 +  local X=""
    2.11 +  for X in "$@"
    2.12 +  do
    2.13 +    if [ -z "$ISABELLE_CLASSES_FILE_FORMAT" ]; then
    2.14 +      ISABELLE_CLASSES_FILE_FORMAT="$X"
    2.15 +    else
    2.16 +      ISABELLE_CLASSES_FILE_FORMAT="$ISABELLE_CLASSES_FILE_FORMAT:$X"
    2.17 +    fi
    2.18 +  done
    2.19 +  export ISABELLE_CLASSES_FILE_FORMAT
    2.20 +}
    2.21 +export -f isabelle_file_format
    2.22 +
    2.23  #administrative build
    2.24  if [ -e "$ISABELLE_HOME/Admin/build" ]; then
    2.25    function isabelle_admin_build ()
     3.1 --- a/src/Pure/PIDE/document.scala	Wed Nov 07 14:06:43 2018 +0100
     3.2 +++ b/src/Pure/PIDE/document.scala	Wed Nov 07 21:42:16 2018 +0100
     3.3 @@ -119,9 +119,6 @@
     3.4  
     3.5        def path: Path = Path.explode(File.standard_path(node))
     3.6  
     3.7 -      def is_bibtex: Boolean = Bibtex.is_bibtex(node)
     3.8 -      def is_bibtex_theory: Boolean = Bibtex.is_bibtex(theory)
     3.9 -
    3.10        def is_theory: Boolean = theory.nonEmpty
    3.11  
    3.12        def theory_base_name: String = Long_Name.base_name(theory)
    3.13 @@ -586,8 +583,6 @@
    3.14  
    3.15      def node_required: Boolean
    3.16      def get_blob: Option[Blob]
    3.17 -    def is_bibtex: Boolean = node_name.is_bibtex
    3.18 -    def is_bibtex_theory: Boolean = node_name.is_bibtex_theory
    3.19      def bibtex_entries: List[Text.Info[String]]
    3.20  
    3.21      def node_edits(
     4.1 --- a/src/Pure/PIDE/document_status.scala	Wed Nov 07 14:06:43 2018 +0100
     4.2 +++ b/src/Pure/PIDE/document_status.scala	Wed Nov 07 21:42:16 2018 +0100
     4.3 @@ -248,7 +248,7 @@
     4.4        }
     4.5  
     4.6      def update(
     4.7 -      session_base: Sessions.Base,
     4.8 +      resources: Resources,
     4.9        state: Document.State,
    4.10        version: Document.Version,
    4.11        domain: Option[Set[Document.Node.Name]] = None,
    4.12 @@ -258,8 +258,8 @@
    4.13        val update_iterator =
    4.14          for {
    4.15            name <- domain.getOrElse(nodes1.domain).iterator
    4.16 -          if !Sessions.is_hidden(name) &&
    4.17 -              !session_base.loaded_theory(name) &&
    4.18 +          if !resources.is_hidden(name) &&
    4.19 +              !resources.session_base.loaded_theory(name) &&
    4.20                !nodes1.is_suppressed(name) &&
    4.21                !nodes1(name).is_empty
    4.22            st = Document_Status.Node_Status.make(state, version, name)
     5.1 --- a/src/Pure/PIDE/headless.scala	Wed Nov 07 14:06:43 2018 +0100
     5.2 +++ b/src/Pure/PIDE/headless.scala	Wed Nov 07 21:42:16 2018 +0100
     5.3 @@ -263,7 +263,7 @@
     5.4                        else changed.nodes.iterator.filter(dep_theories_set).toSet
     5.5  
     5.6                      val (nodes_status_changed, nodes_status1) =
     5.7 -                      st.nodes_status.update(resources.session_base, state, version,
     5.8 +                      st.nodes_status.update(resources, state, version,
     5.9                          domain = Some(domain), trim = changed.assignment)
    5.10  
    5.11                      if (nodes_status_delay >= Time.zero && nodes_status_changed) {
     6.1 --- a/src/Pure/PIDE/resources.scala	Wed Nov 07 14:06:43 2018 +0100
     6.2 +++ b/src/Pure/PIDE/resources.scala	Wed Nov 07 21:42:16 2018 +0100
     6.3 @@ -19,6 +19,23 @@
     6.4  {
     6.5    resources =>
     6.6  
     6.7 +
     6.8 +  /* file formats */
     6.9 +
    6.10 +  val file_formats: File_Format.Environment = File_Format.environment()
    6.11 +
    6.12 +  def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] =
    6.13 +    file_formats.get(name).flatMap(_.make_theory_name(resources, name))
    6.14 +
    6.15 +  def make_theory_content(thy_name: Document.Node.Name): Option[String] =
    6.16 +    file_formats.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
    6.17 +
    6.18 +  def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
    6.19 +    file_formats.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
    6.20 +
    6.21 +  def is_hidden(name: Document.Node.Name): Boolean =
    6.22 +    !name.is_theory || name.theory == Sessions.root_name || file_formats.is_theory(name)
    6.23 +
    6.24    def thy_path(path: Path): Path = path.ext("thy")
    6.25  
    6.26  
     7.1 --- a/src/Pure/Thy/bibtex.scala	Wed Nov 07 14:06:43 2018 +0100
     7.2 +++ b/src/Pure/Thy/bibtex.scala	Wed Nov 07 21:42:16 2018 +0100
     7.3 @@ -16,6 +16,54 @@
     7.4  
     7.5  object Bibtex
     7.6  {
     7.7 +  /** file format **/
     7.8 +
     7.9 +  def is_bibtex(name: String): Boolean = name.endsWith(".bib")
    7.10 +
    7.11 +  class File_Format extends isabelle.File_Format
    7.12 +  {
    7.13 +    val format_name: String = "bibtex"
    7.14 +    val node_suffix: String = "bibtex_file"
    7.15 +
    7.16 +    def detect(name: String): Boolean = is_bibtex(name)
    7.17 +
    7.18 +    override def make_theory_name(
    7.19 +      resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
    7.20 +    {
    7.21 +      for { (_, ext_name) <- Thy_Header.split_file_name(name.node) if detect(ext_name) }
    7.22 +      yield {
    7.23 +        val thy_node = resources.append(name.node, Path.explode(node_suffix))
    7.24 +        Document.Node.Name(thy_node, name.master_dir, ext_name)
    7.25 +      }
    7.26 +    }
    7.27 +
    7.28 +    override def make_theory_content(
    7.29 +      resources: Resources, thy_name: Document.Node.Name): Option[String] =
    7.30 +    {
    7.31 +      for {
    7.32 +        (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) if suffix == node_suffix
    7.33 +        (_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name)
    7.34 +      } yield """theory "bib" imports Pure begin bibtex_file """ + quote(ext_name) + """ end"""
    7.35 +    }
    7.36 +
    7.37 +    override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
    7.38 +    {
    7.39 +      val name = snapshot.node_name
    7.40 +      if (detect(name.node)) {
    7.41 +        val title = "Bibliography " + quote(snapshot.node_name.path.base_name)
    7.42 +        val content =
    7.43 +          Isabelle_System.with_tmp_file("bib", "bib") { bib =>
    7.44 +            File.write(bib, snapshot.node.source)
    7.45 +            Bibtex.html_output(List(bib), style = "unsort", title = title)
    7.46 +          }
    7.47 +        Some(Present.Preview(title, content))
    7.48 +      }
    7.49 +      else None
    7.50 +    }
    7.51 +  }
    7.52 +
    7.53 +
    7.54 +
    7.55    /** bibtex errors **/
    7.56  
    7.57    def bibtex_errors(dir: Path, root_name: String): List[String] =
    7.58 @@ -122,37 +170,6 @@
    7.59  
    7.60    /** document model **/
    7.61  
    7.62 -  /* bibtex files */
    7.63 -
    7.64 -  def is_bibtex(name: String): Boolean = name.endsWith(".bib")
    7.65 -
    7.66 -  private val node_suffix: String = "bibtex_file"
    7.67 -
    7.68 -  def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
    7.69 -  {
    7.70 -    Thy_Header.file_name(name.node) match {
    7.71 -      case Some(bib_name) if is_bibtex(bib_name) =>
    7.72 -        val thy_node = resources.append(name.node, Path.explode(node_suffix))
    7.73 -        Some(Document.Node.Name(thy_node, name.master_dir, bib_name))
    7.74 -      case _ => None
    7.75 -    }
    7.76 -  }
    7.77 -
    7.78 -  def make_theory_content(bib_name: String): Option[String] =
    7.79 -    if (is_bibtex(bib_name)) {
    7.80 -      Some("""theory "bib" imports Pure begin bibtex_file """ + quote(bib_name) + """ end""")
    7.81 -    }
    7.82 -    else None
    7.83 -
    7.84 -  def make_theory_content(file: JFile): Option[String] =
    7.85 -    if (file.getName == node_suffix) {
    7.86 -      val parent = file.getParentFile
    7.87 -      if (parent != null && is_bibtex(parent.getName)) make_theory_content(parent.getName)
    7.88 -      else None
    7.89 -    }
    7.90 -    else None
    7.91 -
    7.92 -
    7.93    /* entries */
    7.94  
    7.95    def entries(text: String): List[Text.Info[String]] =
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/Thy/file_format.scala	Wed Nov 07 21:42:16 2018 +0100
     8.3 @@ -0,0 +1,56 @@
     8.4 +/*  Title:      Pure/Thy/file_format.scala
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +Support for user-defined file formats.
     8.8 +*/
     8.9 +
    8.10 +package isabelle
    8.11 +
    8.12 +
    8.13 +object File_Format
    8.14 +{
    8.15 +  def environment(): Environment =
    8.16 +  {
    8.17 +    val file_formats =
    8.18 +      for (name <- space_explode(':', Isabelle_System.getenv_strict("ISABELLE_CLASSES_FILE_FORMAT")))
    8.19 +      yield {
    8.20 +        def err(msg: String): Nothing =
    8.21 +          error("Bad entry " + quote(name) + " in ISABELLE_CLASSES_FILE_FORMAT\n" + msg)
    8.22 +
    8.23 +        try { Class.forName(name).asInstanceOf[Class[File_Format]].newInstance() }
    8.24 +        catch {
    8.25 +          case _: ClassNotFoundException => err("Class not found")
    8.26 +          case exn: Throwable => err(Exn.message(exn))
    8.27 +        }
    8.28 +      }
    8.29 +    new Environment(file_formats)
    8.30 +  }
    8.31 +
    8.32 +  final class Environment private [File_Format](file_formats: List[File_Format])
    8.33 +  {
    8.34 +    override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")
    8.35 +
    8.36 +    def get(name: String): Option[File_Format] = file_formats.find(_.detect(name))
    8.37 +    def get(name: Document.Node.Name): Option[File_Format] = get(name.node)
    8.38 +    def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
    8.39 +    def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined
    8.40 +  }
    8.41 +
    8.42 +  sealed case class Theory_Context(name: Document.Node.Name, content: String)
    8.43 +}
    8.44 +
    8.45 +trait File_Format
    8.46 +{
    8.47 +  def format_name: String
    8.48 +  override def toString = format_name
    8.49 +
    8.50 +  def detect(name: String): Boolean
    8.51 +
    8.52 +  def make_theory_name(
    8.53 +    resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] = None
    8.54 +
    8.55 +  def make_theory_content(
    8.56 +    resources: Resources, thy_name: Document.Node.Name): Option[String] = None
    8.57 +
    8.58 +  def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None
    8.59 +}
     9.1 --- a/src/Pure/Thy/present.scala	Wed Nov 07 14:06:43 2018 +0100
     9.2 +++ b/src/Pure/Thy/present.scala	Wed Nov 07 21:42:16 2018 +0100
     9.3 @@ -105,7 +105,9 @@
     9.4  
     9.5    sealed case class Preview(title: String, content: String)
     9.6  
     9.7 -  def preview(snapshot: Document.Snapshot,
     9.8 +  def preview(
     9.9 +    resources: Resources,
    9.10 +    snapshot: Document.Snapshot,
    9.11      plain_text: Boolean = false,
    9.12      fonts_url: String => String = HTML.fonts_url()): Preview =
    9.13    {
    9.14 @@ -119,26 +121,22 @@
    9.15          List(HTML.source(body)), css = "", structural = false)
    9.16  
    9.17      val name = snapshot.node_name
    9.18 +
    9.19      if (plain_text) {
    9.20        val title = "File " + quote(name.path.base_name)
    9.21        val content = output_document(title, HTML.text(snapshot.node.source))
    9.22        Preview(title, content)
    9.23      }
    9.24 -    else if (name.is_bibtex) {
    9.25 -      val title = "Bibliography " + quote(name.path.base_name)
    9.26 -      val content =
    9.27 -        Isabelle_System.with_tmp_file("bib", "bib") { bib =>
    9.28 -          File.write(bib, snapshot.node.source)
    9.29 -          Bibtex.html_output(List(bib), style = "unsort", title = title)
    9.30 -        }
    9.31 -      Preview(title, content)
    9.32 -    }
    9.33      else {
    9.34 -      val title =
    9.35 -        if (name.is_theory) "Theory " + quote(name.theory_base_name)
    9.36 -        else "File " + quote(name.path.base_name)
    9.37 -      val content = output_document(title, pide_document(snapshot))
    9.38 -      Preview(title, content)
    9.39 +      resources.make_preview(snapshot) match {
    9.40 +        case Some(preview) => preview
    9.41 +        case None =>
    9.42 +          val title =
    9.43 +            if (name.is_theory) "Theory " + quote(name.theory_base_name)
    9.44 +            else "File " + quote(name.path.base_name)
    9.45 +          val content = output_document(title, pide_document(snapshot))
    9.46 +          Preview(title, content)
    9.47 +      }
    9.48      }
    9.49    }
    9.50  
    10.1 --- a/src/Pure/Thy/sessions.scala	Wed Nov 07 14:06:43 2018 +0100
    10.2 +++ b/src/Pure/Thy/sessions.scala	Wed Nov 07 21:42:16 2018 +0100
    10.3 @@ -26,9 +26,6 @@
    10.4  
    10.5    def is_pure(name: String): Boolean = name == Thy_Header.PURE
    10.6  
    10.7 -  def is_hidden(name: Document.Node.Name): Boolean =
    10.8 -    !name.is_theory || name.theory == Sessions.root_name || name.is_bibtex_theory
    10.9 -
   10.10  
   10.11    def exclude_session(name: String): Boolean = name == "" || name == DRAFT
   10.12  
    11.1 --- a/src/Pure/Thy/thy_header.scala	Wed Nov 07 14:06:43 2018 +0100
    11.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Nov 07 21:42:16 2018 +0100
    11.3 @@ -80,14 +80,15 @@
    11.4      (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE)
    11.5  
    11.6    private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    11.7 +  private val Split_File_Name = new Regex("""(.*?)[/\\]*([^/\\:]+)""")
    11.8    private val File_Name = new Regex(""".*?([^/\\:]+)""")
    11.9  
   11.10    def is_base_name(s: String): Boolean =
   11.11      s != "" && !s.exists("/\\:".contains(_))
   11.12  
   11.13 -  def file_name(s: String): Option[String] =
   11.14 +  def split_file_name(s: String): Option[(String, String)] =
   11.15      s match {
   11.16 -      case File_Name(s) => Some(s)
   11.17 +      case Split_File_Name(s1, s2) => Some((s1, s2))
   11.18        case _ => None
   11.19      }
   11.20  
    12.1 --- a/src/Pure/build-jars	Wed Nov 07 14:06:43 2018 +0100
    12.2 +++ b/src/Pure/build-jars	Wed Nov 07 21:42:16 2018 +0100
    12.3 @@ -131,6 +131,7 @@
    12.4    Thy/bibtex.scala
    12.5    Thy/export.scala
    12.6    Thy/export_theory.scala
    12.7 +  Thy/file_format.scala
    12.8    Thy/html.scala
    12.9    Thy/latex.scala
   12.10    Thy/present.scala
    13.1 --- a/src/Tools/VSCode/src/document_model.scala	Wed Nov 07 14:06:43 2018 +0100
    13.2 +++ b/src/Tools/VSCode/src/document_model.scala	Wed Nov 07 21:42:16 2018 +0100
    13.3 @@ -59,7 +59,7 @@
    13.4  
    13.5    def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
    13.6      Document_Model(session, editor, node_name, Content.empty,
    13.7 -      node_required = node_name.is_bibtex_theory)
    13.8 +      node_required = session.resources.file_formats.is_theory(node_name))
    13.9  }
   13.10  
   13.11  sealed case class Document_Model(
    14.1 --- a/src/Tools/VSCode/src/preview_panel.scala	Wed Nov 07 14:06:43 2018 +0100
    14.2 +++ b/src/Tools/VSCode/src/preview_panel.scala	Wed Nov 07 21:42:16 2018 +0100
    14.3 @@ -30,7 +30,7 @@
    14.4                val snapshot = model.snapshot()
    14.5                if (snapshot.is_outdated) m
    14.6                else {
    14.7 -                val preview = Present.preview(snapshot)
    14.8 +                val preview = Present.preview(resources, snapshot)
    14.9                  channel.write(
   14.10                    Protocol.Preview_Response(file, column, preview.title, preview.content))
   14.11                  m - file
    15.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Nov 07 14:06:43 2018 +0100
    15.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Nov 07 21:42:16 2018 +0100
    15.3 @@ -123,10 +123,8 @@
    15.4  
    15.5    def read_file_content(file: JFile): Option[String] =
    15.6    {
    15.7 -    Bibtex.make_theory_content(file) orElse {
    15.8 -      try { Some(Line.normalize(File.read(file))) }
    15.9 -      catch { case ERROR(_) => None }
   15.10 -    }
   15.11 +    try { Some(Line.normalize(File.read(file))) }
   15.12 +    catch { case ERROR(_) => None }
   15.13    }
   15.14  
   15.15    def get_file_content(file: JFile): Option[String] =
   15.16 @@ -226,8 +224,8 @@
   15.17  
   15.18          val thy_files2 =
   15.19            (for {
   15.20 -            (_, model) <- st.models.iterator if model.node_name.is_bibtex
   15.21 -            thy_name <- Bibtex.make_theory_name(resources, model.node_name)
   15.22 +            (_, model) <- st.models.iterator
   15.23 +            thy_name <- resources.make_theory_name(model.node_name)
   15.24            } yield thy_name).toList
   15.25  
   15.26  
    16.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Nov 07 14:06:43 2018 +0100
    16.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Nov 07 21:42:16 2018 +0100
    16.3 @@ -320,7 +320,7 @@
    16.4          yield {
    16.5            val snapshot = model.await_stable_snapshot()
    16.6            val preview =
    16.7 -            Present.preview(snapshot, fonts_url = HTML.fonts_dir(fonts_root),
    16.8 +            Present.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root),
    16.9                plain_text = query.startsWith(plain_text_prefix))
   16.10            HTTP.Response.html(preview.content)
   16.11          })
   16.12 @@ -389,7 +389,7 @@
   16.13      file.foreach(PIDE.plugin.file_watcher.register_parent(_))
   16.14  
   16.15      val content = Document_Model.File_Content(text)
   16.16 -    val node_required1 = node_required || node_name.is_bibtex_theory
   16.17 +    val node_required1 = node_required || session.resources.file_formats.is_theory(node_name)
   16.18      File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
   16.19    }
   16.20  }
   16.21 @@ -427,7 +427,7 @@
   16.22      else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
   16.23  
   16.24    def bibtex_entries: List[Text.Info[String]] =
   16.25 -    if (is_bibtex) content.bibtex_entries else Nil
   16.26 +    if (Bibtex.is_bibtex(node_name.node)) content.bibtex_entries else Nil
   16.27  
   16.28  
   16.29    /* edits */
   16.30 @@ -454,7 +454,7 @@
   16.31  
   16.32    def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
   16.33      if (pending_edits.nonEmpty ||
   16.34 -        !is_bibtex_theory &&
   16.35 +        !session.resources.file_formats.is_theory(node_name) &&
   16.36            (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
   16.37      else {
   16.38        val text_edits = List(Text.Edit.remove(0, content.text))
   16.39 @@ -551,7 +551,7 @@
   16.40  
   16.41    def bibtex_entries: List[Text.Info[String]] =
   16.42      GUI_Thread.require {
   16.43 -      if (is_bibtex) {
   16.44 +      if (Bibtex.is_bibtex(node_name.node)) {
   16.45          _bibtex_entries match {
   16.46            case Some(entries) => entries
   16.47            case None =>
    17.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Nov 07 14:06:43 2018 +0100
    17.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Nov 07 21:42:16 2018 +0100
    17.3 @@ -80,7 +80,7 @@
    17.4  
    17.5    def read_file_content(node_name: Document.Node.Name): Option[String] =
    17.6    {
    17.7 -    Bibtex.make_theory_content(node_name.theory) orElse {
    17.8 +    make_theory_content(node_name) orElse {
    17.9        val name = node_name.node
   17.10        try {
   17.11          val text =
    18.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Nov 07 14:06:43 2018 +0100
    18.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Nov 07 21:42:16 2018 +0100
    18.3 @@ -131,8 +131,8 @@
    18.4  
    18.5            val thy_files2 =
    18.6              (for {
    18.7 -              (name, _) <- models.iterator if name.is_bibtex
    18.8 -              thy_name <- Bibtex.make_theory_name(resources, name)
    18.9 +              (name, _) <- models.iterator
   18.10 +              thy_name <- resources.make_theory_name(name)
   18.11              } yield thy_name).toList
   18.12  
   18.13            val aux_files =
    19.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Nov 07 14:06:43 2018 +0100
    19.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Nov 07 21:42:16 2018 +0100
    19.3 @@ -214,12 +214,11 @@
    19.4    {
    19.5      GUI_Thread.require {}
    19.6  
    19.7 -    val session_base = PIDE.resources.session_base
    19.8      val snapshot = PIDE.session.snapshot()
    19.9  
   19.10      val (nodes_status_changed, nodes_status1) =
   19.11        nodes_status.update(
   19.12 -        session_base, snapshot.state, snapshot.version, domain = domain, trim = trim)
   19.13 +        PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
   19.14  
   19.15      nodes_status = nodes_status1
   19.16      if (nodes_status_changed) status.listData = nodes_status1.present.map(_._1)