--- a/src/Pure/Isar/keyword.ML Tue Aug 21 13:29:34 2012 +0200
+++ b/src/Pure/Isar/keyword.ML Tue Aug 21 14:54:29 2012 +0200
@@ -52,6 +52,7 @@
val command_keyword: string -> T option
val command_files: string -> string list
val command_tags: string -> string list
+ val thy_load_commands: unit -> string list
val dest: unit -> string list * string list
val status: unit -> unit
val define: string * T option -> unit
@@ -198,6 +199,9 @@
val command_files = these o Option.map (#2 o kind_files_of) o command_keyword;
val command_tags = these o Option.map tags_of o command_keyword;
+fun thy_load_commands () =
+ Symtab.fold (fn (name, k) => kind_of k = kind_of thy_load ? cons name) (get_commands ()) [];
+
fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
--- a/src/Pure/Isar/outer_syntax.scala Tue Aug 21 13:29:34 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Tue Aug 21 14:54:29 2012 +0200
@@ -58,6 +58,9 @@
def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
+ def thy_load_commands: List[String] =
+ (for ((name, (Keyword.THY_LOAD, _)) <- keywords.iterator) yield name).toList
+
def + (name: String, kind: (String, List[String]), replace: String): Outer_Syntax =
new Outer_Syntax(
keywords + (name -> kind),
--- a/src/Pure/System/build.scala Tue Aug 21 13:29:34 2012 +0200
+++ b/src/Pure/System/build.scala Tue Aug 21 14:54:29 2012 +0200
@@ -353,19 +353,11 @@
info.theories.map(_._2).flatten.
map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
- val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
- val syntax0 = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
- val syntax =
- // FIXME avoid hardwired stuff!?
- // FIXME broken?!
- if (name == "Pure")
- syntax0 +
- ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
- ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
- else syntax0
+ val loaded_theories = thy_deps.loaded_theories
+ val syntax = thy_deps.syntax
val all_files =
- thy_deps.map({ case (n, h) =>
+ thy_deps.deps.map({ case (n, h) =>
val thy = Path.explode(n.node).expand
val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
thy :: uses
@@ -377,7 +369,7 @@
error(msg + "\nThe error(s) above occurred in session " +
quote(name) + Position.str_of(info.pos))
}
- val errors = parent_errors ::: thy_deps.map(d => d._2.errors).flatten
+ val errors = parent_errors ::: thy_deps.deps.map(d => d._2.errors).flatten
deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
}))
--- a/src/Pure/Thy/thy_info.scala Tue Aug 21 13:29:34 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala Tue Aug 21 14:54:29 2012 +0200
@@ -25,20 +25,47 @@
/* dependencies */
type Dep = (Document.Node.Name, Document.Node.Header)
- private sealed case class Required(
- deps: List[Dep] = Nil,
- seen: Set[Document.Node.Name] = Set.empty)
+
+ object Dependencies
+ {
+ val empty = new Dependencies(Nil, Set.empty)
+ }
+
+ final class Dependencies private(
+ rev_deps: List[Dep],
+ val seen: Set[Document.Node.Name])
{
- def :: (dep: Dep): Required = copy(deps = dep :: deps)
- def + (name: Document.Node.Name): Required = copy(seen = seen + name)
+ def :: (dep: Dep): Dependencies = new Dependencies(dep :: rev_deps, seen)
+ def + (name: Document.Node.Name): Dependencies = new Dependencies(rev_deps, seen = seen + name)
+
+ def deps: List[Dep] = rev_deps.reverse
+
+ def thy_load_commands: List[String] =
+ (for ((_, h) <- rev_deps; (cmd, Some(((Keyword.THY_LOAD, _), _))) <- h.keywords) yield cmd) :::
+ thy_load.base_syntax.thy_load_commands
+
+ def loaded_theories: Set[String] =
+ (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory }
+
+ def syntax: Outer_Syntax =
+ (thy_load.base_syntax /: rev_deps) { case (syn, (name, h)) =>
+ val syn1 = syn.add_keywords(h)
+ // FIXME avoid hardwired stuff!?
+ // FIXME broken?!
+ if (name.theory == "Pure")
+ syn1 +
+ ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
+ ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
+ else syn1
+ }
}
private def require_thys(initiators: List[Document.Node.Name],
- required: Required, names: List[Document.Node.Name]): Required =
+ required: Dependencies, names: List[Document.Node.Name]): Dependencies =
(required /: names)(require_thy(initiators, _, _))
private def require_thy(initiators: List[Document.Node.Name],
- required: Required, name: Document.Node.Name): Required =
+ required: Dependencies, name: Document.Node.Name): Dependencies =
{
if (required.seen(name)) required
else if (thy_load.loaded_theories(name.theory)) required + name
@@ -61,6 +88,6 @@
}
}
- def dependencies(names: List[Document.Node.Name]): List[Dep] =
- require_thys(Nil, Required(), names).deps.reverse
+ def dependencies(names: List[Document.Node.Name]): Dependencies =
+ require_thys(Nil, Dependencies.empty, names)
}
--- a/src/Tools/jEdit/src/plugin.scala Tue Aug 21 13:29:34 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 21 14:54:29 2012 +0200
@@ -366,7 +366,7 @@
val thy_info = new Thy_Info(Isabelle.thy_load)
// FIXME avoid I/O in Swing thread!?!
- val files = thy_info.dependencies(thys).map(_._1.node).
+ val files = thy_info.dependencies(thys).deps.map(_._1.node).
filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
if (!files.isEmpty) {