# HG changeset patch # User wenzelm # Date 1506710982 -7200 # Node ID 67dbf5cdc056ad50be43e78348e8d8d083866442 # Parent 8737b866bd1ce5890d1e29c35ad932bcfb6c0b86 more informative loaded_theories: dependencies and syntax; diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Fri Sep 29 17:41:39 2017 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Fri Sep 29 20:49:42 2017 +0200 @@ -18,6 +18,10 @@ def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init()) + def merge(syns: List[Outer_Syntax]): Outer_Syntax = + if (syns.isEmpty) Thy_Header.bootstrap_syntax + else (syns.head /: syns.tail)(_ ++ _) + /* string literals */ @@ -98,7 +102,10 @@ } - /* merge */ + /* build */ + + def + (header: Document.Node.Header): Outer_Syntax = + add_keywords(header.keywords).add_abbrevs(header.abbrevs) def ++ (other: Outer_Syntax): Outer_Syntax = if (this eq other) this diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Fri Sep 29 17:41:39 2017 +0200 +++ b/src/Pure/ML/ml_process.scala Fri Sep 29 20:49:42 2017 +0200 @@ -103,7 +103,7 @@ ML_Syntax.print_list(ML_Syntax.print_string)(list) List("Resources.init_session_base" + " {global_theories = " + print_table(base.global_theories.toList) + - ", loaded_theories = " + print_list(base.loaded_theories.toList) + + ", loaded_theories = " + print_list(base.loaded_theories.keys) + ", known_theories = " + print_table(base.dest_known_theories) + "}") } diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Fri Sep 29 17:41:39 2017 +0200 +++ b/src/Pure/PIDE/protocol.scala Fri Sep 29 20:49:42 2017 +0200 @@ -327,7 +327,7 @@ val base = resources.session_base.standard_path protocol_command("Prover.session_base", encode_table(base.global_theories.toList), - encode_list(base.loaded_theories.toList), + encode_list(base.loaded_theories.keys), encode_table(base.dest_known_theories)) } diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Sep 29 17:41:39 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Fri Sep 29 20:49:42 2017 +0200 @@ -114,7 +114,7 @@ sealed case class Base( pos: Position.T = Position.none, global_theories: Map[String, String] = Map.empty, - loaded_theories: Set[String] = Set.empty, + loaded_theories: Graph[String, Outer_Syntax] = Graph.string, known: Known = Known.empty, keywords: Thy_Header.Keywords = Nil, syntax: Outer_Syntax = Outer_Syntax.empty, @@ -126,9 +126,14 @@ def platform_path: Base = copy(known = known.platform_path) def standard_path: Base = copy(known = known.standard_path) - def loaded_theory(name: String): Boolean = loaded_theories.contains(name) + def loaded_theory(name: String): Boolean = loaded_theories.defined(name) def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory) + def loaded_theory_syntax(name: String): Option[Outer_Syntax] = + if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None + def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] = + loaded_theory_syntax(name.theory) + def known_theory(name: String): Option[Document.Node.Name] = known.theories.get(name) diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Fri Sep 29 17:41:39 2017 +0200 +++ b/src/Pure/Thy/thy_info.scala Fri Sep 29 20:49:42 2017 +0200 @@ -53,8 +53,20 @@ lazy val syntax: Outer_Syntax = resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs) - def loaded_theories: Set[String] = - resources.session_base.loaded_theories ++ rev_entries.map(_.name.theory) + def loaded_theories: Graph[String, Outer_Syntax] = + (resources.session_base.loaded_theories /: entries)({ case (graph, entry) => + val name = entry.name.theory + val imports = entry.header.imports.map(p => p._1.theory) + + if (graph.defined(name)) + error("Duplicate loaded theory entry " + quote(name)) + + for (dep <- imports if !graph.defined(dep)) + error("Missing loaded theory entry " + quote(dep) + " for " + quote(name)) + + val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header + (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name)) + }) def loaded_files: List[(String, List[Path])] = { diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Fri Sep 29 17:41:39 2017 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Fri Sep 29 20:49:42 2017 +0200 @@ -101,8 +101,7 @@ else { val header = node.header val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax) - Some((resources.session_base.syntax /: imports_syntax)(_ ++ _) - .add_keywords(header.keywords).add_abbrevs(header.abbrevs)) + Some((resources.session_base.syntax /: imports_syntax)(_ ++ _) + header) } nodes += (name -> node.update_syntax(syntax)) } diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Sep 29 17:41:39 2017 +0200 +++ b/src/Pure/Tools/build.scala Fri Sep 29 20:49:42 2017 +0200 @@ -215,7 +215,7 @@ (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (name, (Path.current, (info.theories, - (base.global_theories.toList, (base.loaded_theories.toList, + (base.global_theories.toList, (base.loaded_theories.keys, base.dest_known_theories))))))))))))))) })