# HG changeset patch # User wenzelm # Date 1398890051 -7200 # Node ID 8dd9df88f647519c5dc5de664c4a3554763c485a # Parent b904ea8edd73c079d729ca9952982c79f90c382a some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path; diff -r b904ea8edd73 -r 8dd9df88f647 src/FOL/ROOT --- a/src/FOL/ROOT Wed Apr 30 13:11:24 2014 +0200 +++ b/src/FOL/ROOT Wed Apr 30 22:34:11 2014 +0200 @@ -15,7 +15,9 @@ Michael Dummett, Elements of Intuitionism (Oxford, 1977) *} - theories FOL + global_theories + IFOL + FOL document_files "root.tex" session "FOL-ex" in ex = FOL + diff -r b904ea8edd73 -r 8dd9df88f647 src/HOL/ROOT --- a/src/HOL/ROOT Wed Apr 30 13:11:24 2014 +0200 +++ b/src/HOL/ROOT Wed Apr 30 22:34:11 2014 +0200 @@ -5,7 +5,9 @@ Classical Higher-order Logic. *} options [document_graph] - theories Complex_Main + global_theories + Main + Complex_Main files "Tools/Quickcheck/Narrowing_Engine.hs" "Tools/Quickcheck/PNF_Narrowing_Engine.hs" diff -r b904ea8edd73 -r 8dd9df88f647 src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Pure/Isar/parse.scala Wed Apr 30 22:34:11 2014 +0200 @@ -71,6 +71,8 @@ atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content)) def theory_name: Parser[String] = atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content)) + def theory_xname: Parser[String] = + atom("theory name reference", tok => tok.is_xname && Path.is_wellformed(tok.content)) private def tag_name: Parser[String] = atom("tag name", tok => diff -r b904ea8edd73 -r 8dd9df88f647 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Pure/PIDE/document.ML Wed Apr 30 22:34:11 2014 +0200 @@ -429,7 +429,7 @@ fun loaded_theory name = (case try (unsuffix ".thy") name of - SOME a => Thy_Info.lookup_theory a + SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a] | NONE => NONE); fun init_theory deps node span = diff -r b904ea8edd73 -r 8dd9df88f647 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Pure/PIDE/document.scala Wed Apr 30 22:34:11 2014 +0200 @@ -123,6 +123,8 @@ def is_theory: Boolean = !theory.isEmpty override def toString: String = if (is_theory) theory else node + + def map(f: String => String): Name = copy(f(node), f(master_dir), theory) } diff -r b904ea8edd73 -r 8dd9df88f647 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Pure/PIDE/protocol.scala Wed Apr 30 22:34:11 2014 +0200 @@ -395,6 +395,7 @@ { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, { case Document.Node.Deps(header) => val master_dir = Isabelle_System.posix_path_url(name.master_dir) + val theory = Long_Name.base_name(name.theory) val imports = header.imports.map(_.node) val keywords = header.keywords.map({ case (a, b, _) => (a, b) }) (Nil, @@ -402,7 +403,7 @@ pair(list(pair(Encode.string, option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))), list(Encode.string)))))( - (master_dir, (name.theory, (imports, (keywords, header.errors)))))) }, + (master_dir, (theory, (imports, (keywords, header.errors)))))) }, { case Document.Node.Perspective(a, b, c) => (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) })) diff -r b904ea8edd73 -r 8dd9df88f647 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Pure/PIDE/resources.scala Wed Apr 30 22:34:11 2014 +0200 @@ -18,15 +18,18 @@ } -class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Prover.Syntax) +class Resources( + val loaded_theories: Set[String], + val known_theories: Map[String, Document.Node.Name], + val base_syntax: Prover.Syntax) { /* document node names */ - def node_name(raw_path: Path): Document.Node.Name = + def node_name(qualifier: String, raw_path: Path): Document.Node.Name = { val path = raw_path.expand val node = path.implode - val theory = Thy_Header.thy_name(node).getOrElse("") + val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse("")) val master_dir = if (theory == "") "" else path.dir.implode Document.Node.Name(node, master_dir, theory) } @@ -57,36 +60,50 @@ } else Nil - def import_name(master: Document.Node.Name, s: String): Document.Node.Name = + private def dummy_name(theory: String): Document.Node.Name = + Document.Node.Name(theory + ".thy", "", theory) + + def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name = { - val theory = Thy_Header.base_name(s) - if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory) - else { - val path = Path.explode(s) - val node = append(master.master_dir, Resources.thy_path(path)) - val master_dir = append(master.master_dir, path.dir) - Document.Node.Name(node, master_dir, theory) + val thy1 = Thy_Header.base_name(s) + val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1) + (known_theories.get(thy1) orElse + known_theories.get(thy2) orElse + known_theories.get(Long_Name.base_name(thy1))) match { + case Some(name) if loaded_theories(name.theory) => dummy_name(name.theory) + case Some(name) => name + case None => + val path = Path.explode(s) + val theory = path.base.implode + if (Long_Name.is_qualified(theory)) dummy_name(theory) + else { + val node = append(master.master_dir, Resources.thy_path(path)) + val master_dir = append(master.master_dir, path.dir) + Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory)) + } } } - def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = + def check_thy_text(qualifier: String, name: Document.Node.Name, text: CharSequence) + : Document.Node.Header = { try { val header = Thy_Header.read(text) + val base_name = Long_Name.base_name(name.theory) val name1 = header.name - if (name.theory != name1) - error("Bad file name " + Resources.thy_path(Path.basic(name.theory)) + + if (base_name != name1) + error("Bad file name " + Resources.thy_path(Path.basic(base_name)) + " for theory " + quote(name1)) - val imports = header.imports.map(import_name(name, _)) + val imports = header.imports.map(import_name(qualifier, name, _)) Document.Node.Header(imports, header.keywords, Nil) } catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } } - def check_thy(name: Document.Node.Name): Document.Node.Header = - with_thy_text(name, check_thy_text(name, _)) + def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header = + with_thy_text(name, check_thy_text(qualifier, name, _)) /* document changes */ diff -r b904ea8edd73 -r 8dd9df88f647 src/Pure/ROOT --- a/src/Pure/ROOT Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Pure/ROOT Wed Apr 30 22:34:11 2014 +0200 @@ -26,7 +26,7 @@ "ML-Systems/use_context.ML" session Pure = - theories Pure + global_theories Pure files "General/exn.ML" "ML-Systems/compiler_polyml.ML" diff -r b904ea8edd73 -r 8dd9df88f647 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Pure/Thy/thy_header.ML Wed Apr 30 22:34:11 2014 +0200 @@ -83,8 +83,9 @@ local val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name); +val theory_xname = Parse.group (fn () => "theory name reference") (Parse.position Parse.xname); -val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name); +val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_xname); val opt_files = Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; diff -r b904ea8edd73 -r 8dd9df88f647 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Pure/Thy/thy_header.scala Wed Apr 30 22:34:11 2014 +0200 @@ -67,7 +67,7 @@ val args = theory_name ~ - (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ + (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ keyword(BEGIN) ^^ { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } diff -r b904ea8edd73 -r 8dd9df88f647 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Pure/Thy/thy_info.scala Wed Apr 30 22:34:11 2014 +0200 @@ -95,11 +95,11 @@ } } - private def require_thys(initiators: List[Document.Node.Name], + private def require_thys(session: String, initiators: List[Document.Node.Name], required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies = - (required /: thys)(require_thy(initiators, _, _)) + (required /: thys)(require_thy(session, initiators, _, _)) - private def require_thy(initiators: List[Document.Node.Name], + private def require_thy(session: String, initiators: List[Document.Node.Name], required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies = { val (name, require_pos) = thy @@ -116,10 +116,10 @@ try { if (initiators.contains(name)) error(cycle_msg(initiators)) val header = - try { resources.check_thy(name).cat_errors(message) } + try { resources.check_thy(session, name).cat_errors(message) } catch { case ERROR(msg) => cat_error(msg, message) } val imports = header.imports.map((_, Position.File(name.node))) - Dep(name, header) :: require_thys(name :: initiators, required1, imports) + Dep(name, header) :: require_thys(session, name :: initiators, required1, imports) } catch { case e: Throwable => @@ -128,6 +128,6 @@ } } - def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies = - require_thys(Nil, Dependencies.empty, thys) + def dependencies(session: String, thys: List[(Document.Node.Name, Position.T)]): Dependencies = + require_thys(session, Nil, Dependencies.empty, thys) } diff -r b904ea8edd73 -r 8dd9df88f647 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Pure/Tools/build.scala Wed Apr 30 22:34:11 2014 +0200 @@ -56,7 +56,7 @@ parent: Option[String], description: String, options: List[Options.Spec], - theories: List[(List[Options.Spec], List[String])], + theories: List[(Boolean, List[Options.Spec], List[String])], files: List[String], document_files: List[(String, String)]) extends Entry @@ -70,7 +70,7 @@ parent: Option[String], description: String, options: Options, - theories: List[(Options, List[Path])], + theories: List[(Boolean, Options, List[Path])], files: List[Path], document_files: List[(Path, Path)], entry_digest: SHA1.Digest) @@ -89,8 +89,8 @@ val session_options = options ++ entry.options val theories = - entry.theories.map({ case (opts, thys) => - (session_options ++ opts, thys.map(Path.explode(_))) }) + entry.theories.map({ case (global, opts, thys) => + (global, session_options ++ opts, thys.map(Path.explode(_))) }) val files = entry.files.map(Path.explode(_)) val document_files = entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) @@ -179,8 +179,8 @@ if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList else pre_selected - val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet)) - (selected, tree1) + val graph1 = graph.restrict(graph.all_preds(selected).toSet) + (selected, new Session_Tree(graph1)) } def topological_order: List[(String, Session_Info)] = @@ -199,6 +199,7 @@ private val IN = "in" private val DESCRIPTION = "description" private val OPTIONS = "options" + private val GLOBAL_THEORIES = "global_theories" private val THEORIES = "theories" private val FILES = "files" private val DOCUMENT_FILES = "document_files" @@ -206,7 +207,7 @@ lazy val root_syntax = Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) + - IN + DESCRIPTION + OPTIONS + THEORIES + FILES + DOCUMENT_FILES + IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES object Parser extends Parse.Parser { @@ -226,8 +227,9 @@ val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]") val theories = - keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^ - { case _ ~ (x ~ y) => (x, y) } + (keyword(GLOBAL_THEORIES) | keyword(THEORIES)) ~! + ((options | success(Nil)) ~ rep(theory_xname)) ^^ + { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) } val document_files = keyword(DOCUMENT_FILES) ~! @@ -407,6 +409,7 @@ sealed case class Session_Content( loaded_theories: Set[String], + known_theories: Map[String, Document.Node.Name], keywords: Thy_Header.Keywords, syntax: Outer_Syntax, sources: List[(Path, SHA1.Digest)]) @@ -425,15 +428,14 @@ if (progress.stopped) throw Exn.Interrupt() try { - val (preloaded, parent_syntax) = - info.parent match { + val (loaded_theories0, known_theories0, syntax0) = + info.parent.map(deps(_)) match { case None => - (Set.empty[String], Outer_Syntax.init()) - case Some(parent_name) => - val parent = deps(parent_name) - (parent.loaded_theories, parent.syntax) + (Set.empty[String], Map.empty[String, Document.Node.Name], Outer_Syntax.init()) + case Some(parent) => + (parent.loaded_theories, parent.known_theories, parent.syntax) } - val resources = new Resources(preloaded, parent_syntax) + val resources = new Resources(loaded_theories0, known_theories0, syntax0) val thy_info = new Thy_Info(resources) if (verbose || list_files) { @@ -444,15 +446,33 @@ } val thy_deps = - thy_info.dependencies( - info.theories.map(_._2).flatten. - map(thy => (resources.node_name(info.dir + Resources.thy_path(thy)), info.pos))) + { + val root_theories = + info.theories.flatMap({ + case (global, _, thys) => + thys.map(thy => + (resources.node_name( + if (global) "" else name, info.dir + Resources.thy_path(thy)), info.pos)) + }) + val thy_deps = thy_info.dependencies(name, root_theories) - thy_deps.errors match { - case Nil => - case errs => error(cat_lines(errs)) + thy_deps.errors match { + case Nil => thy_deps + case errs => error(cat_lines(errs)) + } } + val known_theories = + (known_theories0 /: thy_deps.deps)({ case (known, dep) => + val name = dep.name + known.get(name.theory) match { + case Some(name1) if name != name1 => + error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) + case _ => + known + (name.theory -> name) + (Long_Name.base_name(name.theory) -> name) + } + }) + val loaded_theories = thy_deps.loaded_theories val keywords = thy_deps.keywords val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax] @@ -480,7 +500,9 @@ val sources = all_files.map(p => (p, SHA1.digest(p.file))) - deps + (name -> Session_Content(loaded_theories, keywords, syntax, sources)) + val content = + Session_Content(loaded_theories, known_theories, keywords, syntax, sources) + deps + (name -> content) } catch { case ERROR(msg) => @@ -528,12 +550,13 @@ if (is_pure(name)) Options.encode(info.options) else { + val theories = info.theories.map(x => (x._2, x._3)) import XML.Encode._ pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))))( (command_timings, (do_output, (info.options, (verbose, (browser_info, - (info.document_files, (parent, (info.chapter, (name, info.theories)))))))))) + (info.document_files, (parent, (info.chapter, (name, theories)))))))))) })) private val env = diff -r b904ea8edd73 -r 8dd9df88f647 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Wed Apr 30 22:34:11 2014 +0200 @@ -70,7 +70,7 @@ if (is_theory) { JEdit_Lib.buffer_lock(buffer) { Exn.capture { - PIDE.resources.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength)) + PIDE.resources.check_thy_text("", node_name, buffer.getSegment(0, buffer.getLength)) } match { case Exn.Res(header) => header case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn)) diff -r b904ea8edd73 -r 8dd9df88f647 src/Tools/jEdit/src/isabelle_logic.scala --- a/src/Tools/jEdit/src/isabelle_logic.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed Apr 30 22:34:11 2014 +0200 @@ -82,7 +82,9 @@ { val dirs = session_dirs() val name = session_args().last - Build.session_content(PIDE.options.value, inlined_files, dirs, name) + val content = Build.session_content(PIDE.options.value, inlined_files, dirs, name) + content.copy(known_theories = + content.known_theories.mapValues(name => name.map(Isabelle_System.jvm_path(_)))) } } diff -r b904ea8edd73 -r 8dd9df88f647 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Apr 30 22:34:11 2014 +0200 @@ -19,8 +19,11 @@ import org.gjt.sp.jedit.bufferio.BufferIORequest -class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax) - extends Resources(loaded_theories, base_syntax) +class JEdit_Resources( + loaded_theories: Set[String], + known_theories: Map[String, Document.Node.Name], + base_syntax: Outer_Syntax) + extends Resources(loaded_theories, known_theories, base_syntax) { /* document node names */ diff -r b904ea8edd73 -r 8dd9df88f647 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Apr 30 13:11:24 2014 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Wed Apr 30 22:34:11 2014 +0200 @@ -35,7 +35,8 @@ @volatile var startup_notified = false @volatile var plugin: Plugin = null - @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty)) + @volatile var session: Session = + new Session(new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty)) def options_changed() { plugin.options_changed() } def deps_changed() { plugin.deps_changed() } @@ -210,7 +211,7 @@ val thy_info = new Thy_Info(PIDE.resources) // FIXME avoid I/O in Swing thread!?! - val files = thy_info.dependencies(thys).deps.map(_.name.node). + val files = thy_info.dependencies("", thys).deps.map(_.name.node). filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file)) if (!files.isEmpty) { @@ -350,7 +351,8 @@ JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _) val content = Isabelle_Logic.session_content(false) - val resources = new JEdit_Resources(content.loaded_theories, content.syntax) + val resources = + new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax) PIDE.session = new Session(resources) { override def output_delay = PIDE.options.seconds("editor_output_delay")