some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
authorwenzelm
Wed Apr 30 22:34:11 2014 +0200 (2014-04-30)
changeset 568018dd9df88f647
parent 56800 b904ea8edd73
child 56802 c83eb2435b27
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
src/FOL/ROOT
src/HOL/ROOT
src/Pure/Isar/parse.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.scala
src/Pure/ROOT
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.scala
src/Pure/Tools/build.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/isabelle_logic.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/FOL/ROOT	Wed Apr 30 13:11:24 2014 +0200
     1.2 +++ b/src/FOL/ROOT	Wed Apr 30 22:34:11 2014 +0200
     1.3 @@ -15,7 +15,9 @@
     1.4  
     1.5      Michael Dummett, Elements of Intuitionism (Oxford, 1977)
     1.6    *}
     1.7 -  theories FOL
     1.8 +  global_theories
     1.9 +    IFOL
    1.10 +    FOL
    1.11    document_files "root.tex"
    1.12  
    1.13  session "FOL-ex" in ex = FOL +
     2.1 --- a/src/HOL/ROOT	Wed Apr 30 13:11:24 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Wed Apr 30 22:34:11 2014 +0200
     2.3 @@ -5,7 +5,9 @@
     2.4      Classical Higher-order Logic.
     2.5    *}
     2.6    options [document_graph]
     2.7 -  theories Complex_Main
     2.8 +  global_theories
     2.9 +    Main
    2.10 +    Complex_Main
    2.11    files
    2.12      "Tools/Quickcheck/Narrowing_Engine.hs"
    2.13      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
     3.1 --- a/src/Pure/Isar/parse.scala	Wed Apr 30 13:11:24 2014 +0200
     3.2 +++ b/src/Pure/Isar/parse.scala	Wed Apr 30 22:34:11 2014 +0200
     3.3 @@ -71,6 +71,8 @@
     3.4        atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
     3.5      def theory_name: Parser[String] =
     3.6        atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
     3.7 +    def theory_xname: Parser[String] =
     3.8 +      atom("theory name reference", tok => tok.is_xname && Path.is_wellformed(tok.content))
     3.9  
    3.10      private def tag_name: Parser[String] =
    3.11        atom("tag name", tok =>
     4.1 --- a/src/Pure/PIDE/document.ML	Wed Apr 30 13:11:24 2014 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Wed Apr 30 22:34:11 2014 +0200
     4.3 @@ -429,7 +429,7 @@
     4.4  
     4.5  fun loaded_theory name =
     4.6    (case try (unsuffix ".thy") name of
     4.7 -    SOME a => Thy_Info.lookup_theory a
     4.8 +    SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a]
     4.9    | NONE => NONE);
    4.10  
    4.11  fun init_theory deps node span =
     5.1 --- a/src/Pure/PIDE/document.scala	Wed Apr 30 13:11:24 2014 +0200
     5.2 +++ b/src/Pure/PIDE/document.scala	Wed Apr 30 22:34:11 2014 +0200
     5.3 @@ -123,6 +123,8 @@
     5.4  
     5.5        def is_theory: Boolean = !theory.isEmpty
     5.6        override def toString: String = if (is_theory) theory else node
     5.7 +
     5.8 +      def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
     5.9      }
    5.10  
    5.11  
     6.1 --- a/src/Pure/PIDE/protocol.scala	Wed Apr 30 13:11:24 2014 +0200
     6.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Apr 30 22:34:11 2014 +0200
     6.3 @@ -395,6 +395,7 @@
     6.4            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
     6.5            { case Document.Node.Deps(header) =>
     6.6                val master_dir = Isabelle_System.posix_path_url(name.master_dir)
     6.7 +              val theory = Long_Name.base_name(name.theory)
     6.8                val imports = header.imports.map(_.node)
     6.9                val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
    6.10                (Nil,
    6.11 @@ -402,7 +403,7 @@
    6.12                    pair(list(pair(Encode.string,
    6.13                      option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
    6.14                    list(Encode.string)))))(
    6.15 -                (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
    6.16 +                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
    6.17            { case Document.Node.Perspective(a, b, c) =>
    6.18                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
    6.19                  list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
     7.1 --- a/src/Pure/PIDE/resources.scala	Wed Apr 30 13:11:24 2014 +0200
     7.2 +++ b/src/Pure/PIDE/resources.scala	Wed Apr 30 22:34:11 2014 +0200
     7.3 @@ -18,15 +18,18 @@
     7.4  }
     7.5  
     7.6  
     7.7 -class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Prover.Syntax)
     7.8 +class Resources(
     7.9 +  val loaded_theories: Set[String],
    7.10 +  val known_theories: Map[String, Document.Node.Name],
    7.11 +  val base_syntax: Prover.Syntax)
    7.12  {
    7.13    /* document node names */
    7.14  
    7.15 -  def node_name(raw_path: Path): Document.Node.Name =
    7.16 +  def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
    7.17    {
    7.18      val path = raw_path.expand
    7.19      val node = path.implode
    7.20 -    val theory = Thy_Header.thy_name(node).getOrElse("")
    7.21 +    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
    7.22      val master_dir = if (theory == "") "" else path.dir.implode
    7.23      Document.Node.Name(node, master_dir, theory)
    7.24    }
    7.25 @@ -57,36 +60,50 @@
    7.26      }
    7.27      else Nil
    7.28  
    7.29 -  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
    7.30 +  private def dummy_name(theory: String): Document.Node.Name =
    7.31 +    Document.Node.Name(theory + ".thy", "", theory)
    7.32 +
    7.33 +  def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
    7.34    {
    7.35 -    val theory = Thy_Header.base_name(s)
    7.36 -    if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
    7.37 -    else {
    7.38 -      val path = Path.explode(s)
    7.39 -      val node = append(master.master_dir, Resources.thy_path(path))
    7.40 -      val master_dir = append(master.master_dir, path.dir)
    7.41 -      Document.Node.Name(node, master_dir, theory)
    7.42 +    val thy1 = Thy_Header.base_name(s)
    7.43 +    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1)
    7.44 +    (known_theories.get(thy1) orElse
    7.45 +     known_theories.get(thy2) orElse
    7.46 +     known_theories.get(Long_Name.base_name(thy1))) match {
    7.47 +      case Some(name) if loaded_theories(name.theory) => dummy_name(name.theory)
    7.48 +      case Some(name) => name
    7.49 +      case None =>
    7.50 +        val path = Path.explode(s)
    7.51 +        val theory = path.base.implode
    7.52 +        if (Long_Name.is_qualified(theory)) dummy_name(theory)
    7.53 +        else {
    7.54 +          val node = append(master.master_dir, Resources.thy_path(path))
    7.55 +          val master_dir = append(master.master_dir, path.dir)
    7.56 +          Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory))
    7.57 +        }
    7.58      }
    7.59    }
    7.60  
    7.61 -  def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
    7.62 +  def check_thy_text(qualifier: String, name: Document.Node.Name, text: CharSequence)
    7.63 +    : Document.Node.Header =
    7.64    {
    7.65      try {
    7.66        val header = Thy_Header.read(text)
    7.67  
    7.68 +      val base_name = Long_Name.base_name(name.theory)
    7.69        val name1 = header.name
    7.70 -      if (name.theory != name1)
    7.71 -        error("Bad file name " + Resources.thy_path(Path.basic(name.theory)) +
    7.72 +      if (base_name != name1)
    7.73 +        error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
    7.74            " for theory " + quote(name1))
    7.75  
    7.76 -      val imports = header.imports.map(import_name(name, _))
    7.77 +      val imports = header.imports.map(import_name(qualifier, name, _))
    7.78        Document.Node.Header(imports, header.keywords, Nil)
    7.79      }
    7.80      catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    7.81    }
    7.82  
    7.83 -  def check_thy(name: Document.Node.Name): Document.Node.Header =
    7.84 -    with_thy_text(name, check_thy_text(name, _))
    7.85 +  def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
    7.86 +    with_thy_text(name, check_thy_text(qualifier, name, _))
    7.87  
    7.88  
    7.89    /* document changes */
     8.1 --- a/src/Pure/ROOT	Wed Apr 30 13:11:24 2014 +0200
     8.2 +++ b/src/Pure/ROOT	Wed Apr 30 22:34:11 2014 +0200
     8.3 @@ -26,7 +26,7 @@
     8.4      "ML-Systems/use_context.ML"
     8.5  
     8.6  session Pure =
     8.7 -  theories Pure
     8.8 +  global_theories Pure
     8.9    files
    8.10      "General/exn.ML"
    8.11      "ML-Systems/compiler_polyml.ML"
     9.1 --- a/src/Pure/Thy/thy_header.ML	Wed Apr 30 13:11:24 2014 +0200
     9.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Apr 30 22:34:11 2014 +0200
     9.3 @@ -83,8 +83,9 @@
     9.4  local
     9.5  
     9.6  val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
     9.7 +val theory_xname = Parse.group (fn () => "theory name reference") (Parse.position Parse.xname);
     9.8  
     9.9 -val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name);
    9.10 +val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_xname);
    9.11  
    9.12  val opt_files =
    9.13    Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
    10.1 --- a/src/Pure/Thy/thy_header.scala	Wed Apr 30 13:11:24 2014 +0200
    10.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Apr 30 22:34:11 2014 +0200
    10.3 @@ -67,7 +67,7 @@
    10.4  
    10.5      val args =
    10.6        theory_name ~
    10.7 -      (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    10.8 +      (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    10.9        (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
   10.10        keyword(BEGIN) ^^
   10.11        { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
    11.1 --- a/src/Pure/Thy/thy_info.scala	Wed Apr 30 13:11:24 2014 +0200
    11.2 +++ b/src/Pure/Thy/thy_info.scala	Wed Apr 30 22:34:11 2014 +0200
    11.3 @@ -95,11 +95,11 @@
    11.4      }
    11.5    }
    11.6  
    11.7 -  private def require_thys(initiators: List[Document.Node.Name],
    11.8 +  private def require_thys(session: String, initiators: List[Document.Node.Name],
    11.9        required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   11.10 -    (required /: thys)(require_thy(initiators, _, _))
   11.11 +    (required /: thys)(require_thy(session, initiators, _, _))
   11.12  
   11.13 -  private def require_thy(initiators: List[Document.Node.Name],
   11.14 +  private def require_thy(session: String, initiators: List[Document.Node.Name],
   11.15        required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
   11.16    {
   11.17      val (name, require_pos) = thy
   11.18 @@ -116,10 +116,10 @@
   11.19        try {
   11.20          if (initiators.contains(name)) error(cycle_msg(initiators))
   11.21          val header =
   11.22 -          try { resources.check_thy(name).cat_errors(message) }
   11.23 +          try { resources.check_thy(session, name).cat_errors(message) }
   11.24            catch { case ERROR(msg) => cat_error(msg, message) }
   11.25          val imports = header.imports.map((_, Position.File(name.node)))
   11.26 -        Dep(name, header) :: require_thys(name :: initiators, required1, imports)
   11.27 +        Dep(name, header) :: require_thys(session, name :: initiators, required1, imports)
   11.28        }
   11.29        catch {
   11.30          case e: Throwable =>
   11.31 @@ -128,6 +128,6 @@
   11.32      }
   11.33    }
   11.34  
   11.35 -  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   11.36 -    require_thys(Nil, Dependencies.empty, thys)
   11.37 +  def dependencies(session: String, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   11.38 +    require_thys(session, Nil, Dependencies.empty, thys)
   11.39  }
    12.1 --- a/src/Pure/Tools/build.scala	Wed Apr 30 13:11:24 2014 +0200
    12.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 30 22:34:11 2014 +0200
    12.3 @@ -56,7 +56,7 @@
    12.4      parent: Option[String],
    12.5      description: String,
    12.6      options: List[Options.Spec],
    12.7 -    theories: List[(List[Options.Spec], List[String])],
    12.8 +    theories: List[(Boolean, List[Options.Spec], List[String])],
    12.9      files: List[String],
   12.10      document_files: List[(String, String)]) extends Entry
   12.11  
   12.12 @@ -70,7 +70,7 @@
   12.13      parent: Option[String],
   12.14      description: String,
   12.15      options: Options,
   12.16 -    theories: List[(Options, List[Path])],
   12.17 +    theories: List[(Boolean, Options, List[Path])],
   12.18      files: List[Path],
   12.19      document_files: List[(Path, Path)],
   12.20      entry_digest: SHA1.Digest)
   12.21 @@ -89,8 +89,8 @@
   12.22        val session_options = options ++ entry.options
   12.23  
   12.24        val theories =
   12.25 -        entry.theories.map({ case (opts, thys) =>
   12.26 -          (session_options ++ opts, thys.map(Path.explode(_))) })
   12.27 +        entry.theories.map({ case (global, opts, thys) =>
   12.28 +          (global, session_options ++ opts, thys.map(Path.explode(_))) })
   12.29        val files = entry.files.map(Path.explode(_))
   12.30        val document_files =
   12.31          entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
   12.32 @@ -179,8 +179,8 @@
   12.33          if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
   12.34          else pre_selected
   12.35  
   12.36 -      val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet))
   12.37 -      (selected, tree1)
   12.38 +      val graph1 = graph.restrict(graph.all_preds(selected).toSet)
   12.39 +      (selected, new Session_Tree(graph1))
   12.40      }
   12.41  
   12.42      def topological_order: List[(String, Session_Info)] =
   12.43 @@ -199,6 +199,7 @@
   12.44    private val IN = "in"
   12.45    private val DESCRIPTION = "description"
   12.46    private val OPTIONS = "options"
   12.47 +  private val GLOBAL_THEORIES = "global_theories"
   12.48    private val THEORIES = "theories"
   12.49    private val FILES = "files"
   12.50    private val DOCUMENT_FILES = "document_files"
   12.51 @@ -206,7 +207,7 @@
   12.52    lazy val root_syntax =
   12.53      Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   12.54        (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
   12.55 -      IN + DESCRIPTION + OPTIONS + THEORIES + FILES + DOCUMENT_FILES
   12.56 +      IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
   12.57  
   12.58    object Parser extends Parse.Parser
   12.59    {
   12.60 @@ -226,8 +227,9 @@
   12.61        val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
   12.62  
   12.63        val theories =
   12.64 -        keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
   12.65 -          { case _ ~ (x ~ y) => (x, y) }
   12.66 +        (keyword(GLOBAL_THEORIES) | keyword(THEORIES)) ~!
   12.67 +          ((options | success(Nil)) ~ rep(theory_xname)) ^^
   12.68 +          { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
   12.69  
   12.70        val document_files =
   12.71          keyword(DOCUMENT_FILES) ~!
   12.72 @@ -407,6 +409,7 @@
   12.73  
   12.74    sealed case class Session_Content(
   12.75      loaded_theories: Set[String],
   12.76 +    known_theories: Map[String, Document.Node.Name],
   12.77      keywords: Thy_Header.Keywords,
   12.78      syntax: Outer_Syntax,
   12.79      sources: List[(Path, SHA1.Digest)])
   12.80 @@ -425,15 +428,14 @@
   12.81            if (progress.stopped) throw Exn.Interrupt()
   12.82  
   12.83            try {
   12.84 -            val (preloaded, parent_syntax) =
   12.85 -              info.parent match {
   12.86 +            val (loaded_theories0, known_theories0, syntax0) =
   12.87 +              info.parent.map(deps(_)) match {
   12.88                  case None =>
   12.89 -                  (Set.empty[String], Outer_Syntax.init())
   12.90 -                case Some(parent_name) =>
   12.91 -                  val parent = deps(parent_name)
   12.92 -                  (parent.loaded_theories, parent.syntax)
   12.93 +                  (Set.empty[String], Map.empty[String, Document.Node.Name], Outer_Syntax.init())
   12.94 +                case Some(parent) =>
   12.95 +                  (parent.loaded_theories, parent.known_theories, parent.syntax)
   12.96                }
   12.97 -            val resources = new Resources(preloaded, parent_syntax)
   12.98 +            val resources = new Resources(loaded_theories0, known_theories0, syntax0)
   12.99              val thy_info = new Thy_Info(resources)
  12.100  
  12.101              if (verbose || list_files) {
  12.102 @@ -444,15 +446,33 @@
  12.103              }
  12.104  
  12.105              val thy_deps =
  12.106 -              thy_info.dependencies(
  12.107 -                info.theories.map(_._2).flatten.
  12.108 -                  map(thy => (resources.node_name(info.dir + Resources.thy_path(thy)), info.pos)))
  12.109 +            {
  12.110 +              val root_theories =
  12.111 +                info.theories.flatMap({
  12.112 +                  case (global, _, thys) =>
  12.113 +                    thys.map(thy =>
  12.114 +                      (resources.node_name(
  12.115 +                        if (global) "" else name, info.dir + Resources.thy_path(thy)), info.pos))
  12.116 +                })
  12.117 +              val thy_deps = thy_info.dependencies(name, root_theories)
  12.118  
  12.119 -            thy_deps.errors match {
  12.120 -              case Nil =>
  12.121 -              case errs => error(cat_lines(errs))
  12.122 +              thy_deps.errors match {
  12.123 +                case Nil => thy_deps
  12.124 +                case errs => error(cat_lines(errs))
  12.125 +              }
  12.126              }
  12.127  
  12.128 +            val known_theories =
  12.129 +              (known_theories0 /: thy_deps.deps)({ case (known, dep) =>
  12.130 +                val name = dep.name
  12.131 +                known.get(name.theory) match {
  12.132 +                  case Some(name1) if name != name1 =>
  12.133 +                    error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
  12.134 +                  case _ =>
  12.135 +                    known + (name.theory -> name) + (Long_Name.base_name(name.theory) -> name)
  12.136 +                }
  12.137 +              })
  12.138 +
  12.139              val loaded_theories = thy_deps.loaded_theories
  12.140              val keywords = thy_deps.keywords
  12.141              val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
  12.142 @@ -480,7 +500,9 @@
  12.143  
  12.144              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
  12.145  
  12.146 -            deps + (name -> Session_Content(loaded_theories, keywords, syntax, sources))
  12.147 +            val content =
  12.148 +              Session_Content(loaded_theories, known_theories, keywords, syntax, sources)
  12.149 +            deps + (name -> content)
  12.150            }
  12.151            catch {
  12.152              case ERROR(msg) =>
  12.153 @@ -528,12 +550,13 @@
  12.154        if (is_pure(name)) Options.encode(info.options)
  12.155        else
  12.156          {
  12.157 +          val theories = info.theories.map(x => (x._2, x._3))
  12.158            import XML.Encode._
  12.159                pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
  12.160                  pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string,
  12.161                    list(pair(Options.encode, list(Path.encode))))))))))))(
  12.162                (command_timings, (do_output, (info.options, (verbose, (browser_info,
  12.163 -                (info.document_files, (parent, (info.chapter, (name, info.theories))))))))))
  12.164 +                (info.document_files, (parent, (info.chapter, (name, theories))))))))))
  12.165          }))
  12.166  
  12.167      private val env =
    13.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Apr 30 13:11:24 2014 +0200
    13.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Apr 30 22:34:11 2014 +0200
    13.3 @@ -70,7 +70,7 @@
    13.4      if (is_theory) {
    13.5        JEdit_Lib.buffer_lock(buffer) {
    13.6          Exn.capture {
    13.7 -          PIDE.resources.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
    13.8 +          PIDE.resources.check_thy_text("", node_name, buffer.getSegment(0, buffer.getLength))
    13.9          } match {
   13.10            case Exn.Res(header) => header
   13.11            case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
    14.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Wed Apr 30 13:11:24 2014 +0200
    14.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Wed Apr 30 22:34:11 2014 +0200
    14.3 @@ -82,7 +82,9 @@
    14.4    {
    14.5      val dirs = session_dirs()
    14.6      val name = session_args().last
    14.7 -    Build.session_content(PIDE.options.value, inlined_files, dirs, name)
    14.8 +    val content = Build.session_content(PIDE.options.value, inlined_files, dirs, name)
    14.9 +    content.copy(known_theories =
   14.10 +      content.known_theories.mapValues(name => name.map(Isabelle_System.jvm_path(_))))
   14.11    }
   14.12  }
   14.13  
    15.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 30 13:11:24 2014 +0200
    15.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 30 22:34:11 2014 +0200
    15.3 @@ -19,8 +19,11 @@
    15.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
    15.5  
    15.6  
    15.7 -class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
    15.8 -  extends Resources(loaded_theories, base_syntax)
    15.9 +class JEdit_Resources(
   15.10 +    loaded_theories: Set[String],
   15.11 +    known_theories: Map[String, Document.Node.Name],
   15.12 +    base_syntax: Outer_Syntax)
   15.13 +  extends Resources(loaded_theories, known_theories, base_syntax)
   15.14  {
   15.15    /* document node names */
   15.16  
    16.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Apr 30 13:11:24 2014 +0200
    16.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Apr 30 22:34:11 2014 +0200
    16.3 @@ -35,7 +35,8 @@
    16.4    @volatile var startup_notified = false
    16.5  
    16.6    @volatile var plugin: Plugin = null
    16.7 -  @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty))
    16.8 +  @volatile var session: Session =
    16.9 +    new Session(new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty))
   16.10  
   16.11    def options_changed() { plugin.options_changed() }
   16.12    def deps_changed() { plugin.deps_changed() }
   16.13 @@ -210,7 +211,7 @@
   16.14  
   16.15            val thy_info = new Thy_Info(PIDE.resources)
   16.16            // FIXME avoid I/O in Swing thread!?!
   16.17 -          val files = thy_info.dependencies(thys).deps.map(_.name.node).
   16.18 +          val files = thy_info.dependencies("", thys).deps.map(_.name.node).
   16.19              filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
   16.20  
   16.21            if (!files.isEmpty) {
   16.22 @@ -350,7 +351,8 @@
   16.23        JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
   16.24  
   16.25        val content = Isabelle_Logic.session_content(false)
   16.26 -      val resources = new JEdit_Resources(content.loaded_theories, content.syntax)
   16.27 +      val resources =
   16.28 +        new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
   16.29  
   16.30        PIDE.session = new Session(resources) {
   16.31          override def output_delay = PIDE.options.seconds("editor_output_delay")