# HG changeset patch # User wenzelm # Date 1345553669 -7200 # Node ID 6124e0d1120af591c277f2e487dfc4b4ebc81a82 # Parent c82720f054c340ed8e3cc73a08b222e34bf1c266 some support for thy_load_commands; clarified signatures; diff -r c82720f054c3 -r 6124e0d1120a src/Pure/Isar/keyword.ML --- 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 ()); diff -r c82720f054c3 -r 6124e0d1120a src/Pure/Isar/outer_syntax.scala --- 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), diff -r c82720f054c3 -r 6124e0d1120a src/Pure/System/build.scala --- 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)) })) diff -r c82720f054c3 -r 6124e0d1120a src/Pure/Thy/thy_info.scala --- 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) } diff -r c82720f054c3 -r 6124e0d1120a src/Tools/jEdit/src/plugin.scala --- 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) {