some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
--- 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 +
--- 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"
--- 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 =>
--- 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 =
--- 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)
}
--- 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)) }))
--- 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 */
--- 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"
--- 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.$$$ ")") [];
--- 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) }
--- 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)
}
--- 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 =
--- 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))
--- 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(_))))
}
}
--- 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 */
--- 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")