clarified theory syntax vs. overall session syntax;
authorwenzelm
Fri Sep 29 21:30:31 2017 +0200 (19 months ago)
changeset 66719d37efafd55b5
parent 66718 514c4907ff0b
child 66720 b07192253605
clarified theory syntax vs. overall session syntax;
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 21:03:04 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 21:30:31 2017 +0200
     1.3 @@ -205,13 +205,13 @@
     1.4                resources.thy_info.dependencies(root_theories)
     1.5              }
     1.6  
     1.7 -            val syntax = thy_deps.syntax
     1.8 +            val session_syntax = thy_deps.overall_syntax
     1.9  
    1.10              val theory_files = thy_deps.names.map(_.path)
    1.11              val loaded_files =
    1.12                if (inlined_files) {
    1.13                  if (Sessions.is_pure(info.name)) {
    1.14 -                  (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) ::
    1.15 +                  (Thy_Header.PURE -> resources.pure_files(session_syntax, info.dir)) ::
    1.16                      thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    1.17                  }
    1.18                  else thy_deps.loaded_files
    1.19 @@ -226,8 +226,10 @@
    1.20              if (list_files)
    1.21                progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    1.22  
    1.23 -            if (check_keywords.nonEmpty)
    1.24 -              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
    1.25 +            if (check_keywords.nonEmpty) {
    1.26 +              Check_Keywords.check_keywords(
    1.27 +                progress, session_syntax.keywords, check_keywords, theory_files)
    1.28 +            }
    1.29  
    1.30              val session_graph: Graph_Display.Graph =
    1.31              {
    1.32 @@ -278,7 +280,7 @@
    1.33                  global_theories = global_theories,
    1.34                  loaded_theories = thy_deps.loaded_theories,
    1.35                  known = known,
    1.36 -                syntax = syntax,
    1.37 +                syntax = session_syntax,
    1.38                  sources = sources,
    1.39                  session_graph = session_graph,
    1.40                  errors = thy_deps.errors ::: sources_errors,
     2.1 --- a/src/Pure/Thy/thy_info.scala	Fri Sep 29 21:03:04 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Sep 29 21:30:31 2017 +0200
     2.3 @@ -26,34 +26,25 @@
     2.4  
     2.5    object Dependencies
     2.6    {
     2.7 -    val empty = new Dependencies(Nil, Nil, Nil, Set.empty)
     2.8 +    val empty = new Dependencies(Nil, Set.empty)
     2.9    }
    2.10  
    2.11    final class Dependencies private(
    2.12      rev_entries: List[Document.Node.Entry],
    2.13 -    val keywords: Thy_Header.Keywords,
    2.14 -    val abbrevs: Thy_Header.Abbrevs,
    2.15      val seen: Set[Document.Node.Name])
    2.16    {
    2.17      def :: (entry: Document.Node.Entry): Dependencies =
    2.18 -      new Dependencies(
    2.19 -        entry :: rev_entries,
    2.20 -        entry.header.keywords ::: keywords,
    2.21 -        entry.header.abbrevs ::: abbrevs,
    2.22 -        seen)
    2.23 +      new Dependencies(entry :: rev_entries, seen)
    2.24  
    2.25      def + (name: Document.Node.Name): Dependencies =
    2.26 -      new Dependencies(rev_entries, keywords, abbrevs, seen + name)
    2.27 +      new Dependencies(rev_entries, seen + name)
    2.28  
    2.29      def entries: List[Document.Node.Entry] = rev_entries.reverse
    2.30      def names: List[Document.Node.Name] = entries.map(_.name)
    2.31  
    2.32      def errors: List[String] = entries.flatMap(_.header.errors)
    2.33  
    2.34 -    lazy val syntax: Outer_Syntax =
    2.35 -      resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    2.36 -
    2.37 -    def loaded_theories: Graph[String, Outer_Syntax] =
    2.38 +    lazy val loaded_theories: Graph[String, Outer_Syntax] =
    2.39        (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
    2.40          val name = entry.name.theory
    2.41          val imports = entry.header.imports.map(p => p._1.theory)
    2.42 @@ -71,9 +62,13 @@
    2.43      def loaded_files: List[(String, List[Path])] =
    2.44      {
    2.45        names.map(_.theory) zip
    2.46 -        Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
    2.47 +        Par_List.map((e: () => List[Path]) => e(),
    2.48 +          names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
    2.49      }
    2.50  
    2.51 +    lazy val overall_syntax: Outer_Syntax =
    2.52 +      Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
    2.53 +
    2.54      override def toString: String = entries.toString
    2.55    }
    2.56