more informative loaded_theories: dependencies and syntax;
authorwenzelm
Fri Sep 29 20:49:42 2017 +0200 (19 months ago)
changeset 6671767dbf5cdc056
parent 66716 8737b866bd1c
child 66718 514c4907ff0b
more informative loaded_theories: dependencies and syntax;
src/Pure/Isar/outer_syntax.scala
src/Pure/ML/ml_process.scala
src/Pure/PIDE/protocol.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Sep 29 17:41:39 2017 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Fri Sep 29 20:49:42 2017 +0200
     1.3 @@ -18,6 +18,10 @@
     1.4  
     1.5    def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
     1.6  
     1.7 +  def merge(syns: List[Outer_Syntax]): Outer_Syntax =
     1.8 +    if (syns.isEmpty) Thy_Header.bootstrap_syntax
     1.9 +    else (syns.head /: syns.tail)(_ ++ _)
    1.10 +
    1.11  
    1.12    /* string literals */
    1.13  
    1.14 @@ -98,7 +102,10 @@
    1.15      }
    1.16  
    1.17  
    1.18 -  /* merge */
    1.19 +  /* build */
    1.20 +
    1.21 +  def + (header: Document.Node.Header): Outer_Syntax =
    1.22 +    add_keywords(header.keywords).add_abbrevs(header.abbrevs)
    1.23  
    1.24    def ++ (other: Outer_Syntax): Outer_Syntax =
    1.25      if (this eq other) this
     2.1 --- a/src/Pure/ML/ml_process.scala	Fri Sep 29 17:41:39 2017 +0200
     2.2 +++ b/src/Pure/ML/ml_process.scala	Fri Sep 29 20:49:42 2017 +0200
     2.3 @@ -103,7 +103,7 @@
     2.4              ML_Syntax.print_list(ML_Syntax.print_string)(list)
     2.5            List("Resources.init_session_base" +
     2.6              " {global_theories = " + print_table(base.global_theories.toList) +
     2.7 -            ", loaded_theories = " + print_list(base.loaded_theories.toList) +
     2.8 +            ", loaded_theories = " + print_list(base.loaded_theories.keys) +
     2.9              ", known_theories = " + print_table(base.dest_known_theories) + "}")
    2.10        }
    2.11  
     3.1 --- a/src/Pure/PIDE/protocol.scala	Fri Sep 29 17:41:39 2017 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Sep 29 20:49:42 2017 +0200
     3.3 @@ -327,7 +327,7 @@
     3.4      val base = resources.session_base.standard_path
     3.5      protocol_command("Prover.session_base",
     3.6        encode_table(base.global_theories.toList),
     3.7 -      encode_list(base.loaded_theories.toList),
     3.8 +      encode_list(base.loaded_theories.keys),
     3.9        encode_table(base.dest_known_theories))
    3.10    }
    3.11  
     4.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 17:41:39 2017 +0200
     4.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 20:49:42 2017 +0200
     4.3 @@ -114,7 +114,7 @@
     4.4    sealed case class Base(
     4.5      pos: Position.T = Position.none,
     4.6      global_theories: Map[String, String] = Map.empty,
     4.7 -    loaded_theories: Set[String] = Set.empty,
     4.8 +    loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     4.9      known: Known = Known.empty,
    4.10      keywords: Thy_Header.Keywords = Nil,
    4.11      syntax: Outer_Syntax = Outer_Syntax.empty,
    4.12 @@ -126,9 +126,14 @@
    4.13      def platform_path: Base = copy(known = known.platform_path)
    4.14      def standard_path: Base = copy(known = known.standard_path)
    4.15  
    4.16 -    def loaded_theory(name: String): Boolean = loaded_theories.contains(name)
    4.17 +    def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
    4.18      def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
    4.19  
    4.20 +    def loaded_theory_syntax(name: String): Option[Outer_Syntax] =
    4.21 +      if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None
    4.22 +    def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
    4.23 +      loaded_theory_syntax(name.theory)
    4.24 +
    4.25      def known_theory(name: String): Option[Document.Node.Name] =
    4.26        known.theories.get(name)
    4.27  
     5.1 --- a/src/Pure/Thy/thy_info.scala	Fri Sep 29 17:41:39 2017 +0200
     5.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Sep 29 20:49:42 2017 +0200
     5.3 @@ -53,8 +53,20 @@
     5.4      lazy val syntax: Outer_Syntax =
     5.5        resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
     5.6  
     5.7 -    def loaded_theories: Set[String] =
     5.8 -      resources.session_base.loaded_theories ++ rev_entries.map(_.name.theory)
     5.9 +    def loaded_theories: Graph[String, Outer_Syntax] =
    5.10 +      (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
    5.11 +        val name = entry.name.theory
    5.12 +        val imports = entry.header.imports.map(p => p._1.theory)
    5.13 +
    5.14 +        if (graph.defined(name))
    5.15 +          error("Duplicate loaded theory entry " + quote(name))
    5.16 +
    5.17 +        for (dep <- imports if !graph.defined(dep))
    5.18 +          error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
    5.19 +
    5.20 +        val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
    5.21 +        (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
    5.22 +      })
    5.23  
    5.24      def loaded_files: List[(String, List[Path])] =
    5.25      {
     6.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 17:41:39 2017 +0200
     6.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 20:49:42 2017 +0200
     6.3 @@ -101,8 +101,7 @@
     6.4          else {
     6.5            val header = node.header
     6.6            val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
     6.7 -          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _)
     6.8 -            .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
     6.9 +          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _) + header)
    6.10          }
    6.11        nodes += (name -> node.update_syntax(syntax))
    6.12      }
     7.1 --- a/src/Pure/Tools/build.scala	Fri Sep 29 17:41:39 2017 +0200
     7.2 +++ b/src/Pure/Tools/build.scala	Fri Sep 29 20:49:42 2017 +0200
     7.3 @@ -215,7 +215,7 @@
     7.4                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
     7.5                  (parent, (info.chapter, (name, (Path.current,
     7.6                  (info.theories,
     7.7 -                (base.global_theories.toList, (base.loaded_theories.toList,
     7.8 +                (base.global_theories.toList, (base.loaded_theories.keys,
     7.9                  base.dest_known_theories)))))))))))))))
    7.10              })
    7.11