merged
authorwenzelm
Fri Sep 29 22:45:58 2017 +0200 (19 months ago)
changeset 6672318cc87e2335f
parent 66710 676258a1cf01
parent 66722 9c661b74ce92
child 66724 1e1f9f603385
merged
     1.1 --- a/NEWS	Fri Sep 29 16:55:08 2017 +0100
     1.2 +++ b/NEWS	Fri Sep 29 22:45:58 2017 +0200
     1.3 @@ -7,6 +7,14 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Session-qualified theory names are mandatory: it is no longer possible
    1.10 +to refer to unqualified theories from the parent session.
    1.11 +INCOMPATIBILITY for old developments that have not been updated to
    1.12 +Isabelle2017 yet (using the "isabelle imports" tool).
    1.13 +
    1.14 +
    1.15  *** HOL ***
    1.16  
    1.17  * SMT module:
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Sep 29 16:55:08 2017 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Fri Sep 29 22:45:58 2017 +0200
     2.3 @@ -18,6 +18,10 @@
     2.4  
     2.5    def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
     2.6  
     2.7 +  def merge(syns: List[Outer_Syntax]): Outer_Syntax =
     2.8 +    if (syns.isEmpty) Thy_Header.bootstrap_syntax
     2.9 +    else (syns.head /: syns.tail)(_ ++ _)
    2.10 +
    2.11  
    2.12    /* string literals */
    2.13  
    2.14 @@ -98,7 +102,10 @@
    2.15      }
    2.16  
    2.17  
    2.18 -  /* merge */
    2.19 +  /* build */
    2.20 +
    2.21 +  def + (header: Document.Node.Header): Outer_Syntax =
    2.22 +    add_keywords(header.keywords).add_abbrevs(header.abbrevs)
    2.23  
    2.24    def ++ (other: Outer_Syntax): Outer_Syntax =
    2.25      if (this eq other) this
     3.1 --- a/src/Pure/ML/ml_process.scala	Fri Sep 29 16:55:08 2017 +0100
     3.2 +++ b/src/Pure/ML/ml_process.scala	Fri Sep 29 22:45:58 2017 +0200
     3.3 @@ -99,9 +99,11 @@
     3.4              ML_Syntax.print_list(
     3.5                ML_Syntax.print_pair(
     3.6                  ML_Syntax.print_string, ML_Syntax.print_string))(table)
     3.7 +          def print_list(list: List[String]): String =
     3.8 +            ML_Syntax.print_list(ML_Syntax.print_string)(list)
     3.9            List("Resources.init_session_base" +
    3.10              " {global_theories = " + print_table(base.global_theories.toList) +
    3.11 -            ", loaded_theories = " + print_table(base.loaded_theories.toList) +
    3.12 +            ", loaded_theories = " + print_list(base.loaded_theories.keys) +
    3.13              ", known_theories = " + print_table(base.dest_known_theories) + "}")
    3.14        }
    3.15  
     4.1 --- a/src/Pure/PIDE/document.scala	Fri Sep 29 16:55:08 2017 +0100
     4.2 +++ b/src/Pure/PIDE/document.scala	Fri Sep 29 22:45:58 2017 +0200
     4.3 @@ -116,6 +116,8 @@
     4.4            case _ => false
     4.5          }
     4.6  
     4.7 +      def path: Path = Path.explode(node)
     4.8 +
     4.9        def is_theory: Boolean = theory.nonEmpty
    4.10  
    4.11        def theory_base_name: String = Long_Name.base_name(theory)
    4.12 @@ -126,6 +128,11 @@
    4.13        def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
    4.14      }
    4.15  
    4.16 +    sealed case class Entry(name: Node.Name, header: Node.Header)
    4.17 +    {
    4.18 +      override def toString: String = name.toString
    4.19 +    }
    4.20 +
    4.21  
    4.22      /* node overlays */
    4.23  
     5.1 --- a/src/Pure/PIDE/protocol.ML	Fri Sep 29 16:55:08 2017 +0100
     5.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Sep 29 22:45:58 2017 +0200
     5.3 @@ -22,10 +22,11 @@
     5.4      (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
     5.5        let
     5.6          val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
     5.7 +        val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
     5.8        in
     5.9          Resources.init_session_base
    5.10            {global_theories = decode_table global_theories_yxml,
    5.11 -           loaded_theories = decode_table loaded_theories_yxml,
    5.12 +           loaded_theories = decode_list loaded_theories_yxml,
    5.13             known_theories = decode_table known_theories_yxml}
    5.14        end);
    5.15  
     6.1 --- a/src/Pure/PIDE/protocol.scala	Fri Sep 29 16:55:08 2017 +0100
     6.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Sep 29 22:45:58 2017 +0200
     6.3 @@ -316,12 +316,18 @@
     6.4      Symbol.encode_yxml(list(pair(string, string))(table))
     6.5    }
     6.6  
     6.7 +  private def encode_list(lst: List[String]): String =
     6.8 +  {
     6.9 +    import XML.Encode._
    6.10 +    Symbol.encode_yxml(list(string)(lst))
    6.11 +  }
    6.12 +
    6.13    def session_base(resources: Resources)
    6.14    {
    6.15      val base = resources.session_base.standard_path
    6.16      protocol_command("Prover.session_base",
    6.17        encode_table(base.global_theories.toList),
    6.18 -      encode_table(base.loaded_theories.toList),
    6.19 +      encode_list(base.loaded_theories.keys),
    6.20        encode_table(base.dest_known_theories))
    6.21    }
    6.22  
     7.1 --- a/src/Pure/PIDE/resources.ML	Fri Sep 29 16:55:08 2017 +0100
     7.2 +++ b/src/Pure/PIDE/resources.ML	Fri Sep 29 22:45:58 2017 +0200
     7.3 @@ -9,19 +9,18 @@
     7.4    val default_qualifier: string
     7.5    val init_session_base:
     7.6      {global_theories: (string * string) list,
     7.7 -     loaded_theories: (string * string) list,
     7.8 +     loaded_theories: string list,
     7.9       known_theories: (string * string) list} -> unit
    7.10    val finish_session_base: unit -> unit
    7.11    val global_theory: string -> string option
    7.12 -  val loaded_theory: string -> string option
    7.13 +  val loaded_theory: string -> bool
    7.14    val known_theory: string -> Path.T option
    7.15    val master_directory: theory -> Path.T
    7.16    val imports_of: theory -> (string * Position.T) list
    7.17    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
    7.18    val thy_path: Path.T -> Path.T
    7.19    val theory_qualifier: string -> string
    7.20 -  val import_name: string -> Path.T -> string ->
    7.21 -    {node_name: Path.T, master_dir: Path.T, theory_name: string}
    7.22 +  val import_name: string -> Path.T -> string -> {master_dir: Path.T, theory_name: string}
    7.23    val check_thy: Path.T -> string ->
    7.24     {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
    7.25      imports: (string * Position.T) list, keywords: Thy_Header.keywords}
    7.26 @@ -40,7 +39,7 @@
    7.27  
    7.28  val empty_session_base =
    7.29    {global_theories = Symtab.empty: string Symtab.table,
    7.30 -   loaded_theories = Symtab.empty: string Symtab.table,
    7.31 +   loaded_theories = Symtab.empty: unit Symtab.table,
    7.32     known_theories = Symtab.empty: Path.T Symtab.table};
    7.33  
    7.34  val global_session_base =
    7.35 @@ -50,7 +49,7 @@
    7.36    Synchronized.change global_session_base
    7.37      (fn _ =>
    7.38        {global_theories = Symtab.make global_theories,
    7.39 -       loaded_theories = Symtab.make loaded_theories,
    7.40 +       loaded_theories = Symtab.make_set loaded_theories,
    7.41         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    7.42  
    7.43  fun finish_session_base () =
    7.44 @@ -63,7 +62,7 @@
    7.45  fun get_session_base f = f (Synchronized.value global_session_base);
    7.46  
    7.47  fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
    7.48 -fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
    7.49 +fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
    7.50  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    7.51  
    7.52  
    7.53 @@ -108,26 +107,24 @@
    7.54      SOME qualifier => qualifier
    7.55    | NONE => Long_Name.qualifier theory);
    7.56  
    7.57 -fun theory_name qualifier theory0 =
    7.58 -  (case loaded_theory theory0 of
    7.59 -    SOME theory => (true, theory)
    7.60 -  | NONE =>
    7.61 -      let val theory =
    7.62 -        if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
    7.63 -        then theory0
    7.64 -        else Long_Name.qualify qualifier theory0
    7.65 -      in (false, theory) end);
    7.66 +fun theory_name qualifier theory =
    7.67 +  if loaded_theory theory then (true, theory)
    7.68 +  else
    7.69 +    let val theory' =
    7.70 +      if Long_Name.is_qualified theory orelse is_some (global_theory theory)
    7.71 +      then theory
    7.72 +      else Long_Name.qualify qualifier theory
    7.73 +    in (false, theory') end;
    7.74  
    7.75  fun import_name qualifier dir s =
    7.76    (case theory_name qualifier (Thy_Header.import_name s) of
    7.77 -    (true, theory) =>
    7.78 -      {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
    7.79 +    (true, theory) => {master_dir = Path.current, theory_name = theory}
    7.80    | (false, theory) =>
    7.81        let val node_name =
    7.82          (case known_theory theory of
    7.83            SOME node_name => node_name
    7.84          | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))))
    7.85 -      in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end);
    7.86 +      in {master_dir = Path.dir node_name, theory_name = theory} end);
    7.87  
    7.88  fun check_file dir file = File.check_file (File.full_path dir file);
    7.89  
     8.1 --- a/src/Pure/PIDE/resources.scala	Fri Sep 29 16:55:08 2017 +0100
     8.2 +++ b/src/Pure/PIDE/resources.scala	Fri Sep 29 22:45:58 2017 +0200
     8.3 @@ -88,15 +88,14 @@
     8.4    def theory_qualifier(name: Document.Node.Name): String =
     8.5      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     8.6  
     8.7 -  def theory_name(qualifier: String, theory0: String): (Boolean, String) =
     8.8 -    session_base.loaded_theories.get(theory0) match {
     8.9 -      case Some(theory) => (true, theory)
    8.10 -      case None =>
    8.11 -        val theory =
    8.12 -          if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0))
    8.13 -            theory0
    8.14 -          else Long_Name.qualify(qualifier, theory0)
    8.15 -        (false, theory)
    8.16 +  def theory_name(qualifier: String, theory: String): (Boolean, String) =
    8.17 +    if (session_base.loaded_theory(theory)) (true, theory)
    8.18 +    else {
    8.19 +      val theory1 =
    8.20 +        if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
    8.21 +          theory
    8.22 +        else Long_Name.qualify(qualifier, theory)
    8.23 +      (false, theory1)
    8.24      }
    8.25  
    8.26    def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
    8.27 @@ -118,7 +117,7 @@
    8.28  
    8.29    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    8.30    {
    8.31 -    val path = File.check_file(Path.explode(name.node))
    8.32 +    val path = File.check_file(name.path)
    8.33      val reader = Scan.byte_reader(path.file)
    8.34      try { f(reader) } finally { reader.close }
    8.35    }
    8.36 @@ -128,7 +127,7 @@
    8.37    {
    8.38      if (node_name.is_theory && reader.source.length > 0) {
    8.39        try {
    8.40 -        val header = Thy_Header.read(reader, start, strict).decode_symbols
    8.41 +        val header = Thy_Header.read(reader, start, strict)
    8.42  
    8.43          val base_name = node_name.theory_base_name
    8.44          val (name, pos) = header.name
     9.1 --- a/src/Pure/PIDE/session.scala	Fri Sep 29 16:55:08 2017 +0100
     9.2 +++ b/src/Pure/PIDE/session.scala	Fri Sep 29 22:45:58 2017 +0200
     9.3 @@ -220,7 +220,7 @@
     9.4  
     9.5    def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     9.6      global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
     9.7 -    resources.session_base.syntax
     9.8 +    resources.session_base.overall_syntax
     9.9  
    9.10  
    9.11    /* pipelined change parsing */
    10.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 16:55:08 2017 +0100
    10.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 22:45:58 2017 +0200
    10.3 @@ -40,8 +40,7 @@
    10.4        def local_theories_iterator =
    10.5        {
    10.6          val local_path = local_dir.canonical_file.toPath
    10.7 -        theories.iterator.filter(name =>
    10.8 -          Path.explode(name.node).canonical_file.toPath.startsWith(local_path))
    10.9 +        theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
   10.10        }
   10.11  
   10.12        val known_theories =
   10.13 @@ -62,7 +61,7 @@
   10.14          (Map.empty[JFile, List[Document.Node.Name]] /:
   10.15              (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
   10.16            case (known, name) =>
   10.17 -            val file = Path.explode(name.node).canonical_file
   10.18 +            val file = name.path.canonical_file
   10.19              val theories1 = known.getOrElse(file, Nil)
   10.20              if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
   10.21                known
   10.22 @@ -103,22 +102,18 @@
   10.23  
   10.24    object Base
   10.25    {
   10.26 -    def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
   10.27 -
   10.28      def bootstrap(global_theories: Map[String, String]): Base =
   10.29        Base(
   10.30          global_theories = global_theories,
   10.31 -        keywords = Thy_Header.bootstrap_header,
   10.32 -        syntax = Thy_Header.bootstrap_syntax)
   10.33 +        overall_syntax = Thy_Header.bootstrap_syntax)
   10.34    }
   10.35  
   10.36    sealed case class Base(
   10.37      pos: Position.T = Position.none,
   10.38      global_theories: Map[String, String] = Map.empty,
   10.39 -    loaded_theories: Map[String, String] = Map.empty,
   10.40 +    loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
   10.41      known: Known = Known.empty,
   10.42 -    keywords: Thy_Header.Keywords = Nil,
   10.43 -    syntax: Outer_Syntax = Outer_Syntax.empty,
   10.44 +    overall_syntax: Outer_Syntax = Outer_Syntax.empty,
   10.45      sources: List[(Path, SHA1.Digest)] = Nil,
   10.46      session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
   10.47      errors: List[String] = Nil,
   10.48 @@ -127,8 +122,16 @@
   10.49      def platform_path: Base = copy(known = known.platform_path)
   10.50      def standard_path: Base = copy(known = known.standard_path)
   10.51  
   10.52 -    def loaded_theory(name: Document.Node.Name): Boolean =
   10.53 -      loaded_theories.isDefinedAt(name.theory)
   10.54 +    def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
   10.55 +    def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
   10.56 +
   10.57 +    def loaded_theory_syntax(name: String): Option[Outer_Syntax] =
   10.58 +      if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None
   10.59 +    def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
   10.60 +      loaded_theory_syntax(name.theory)
   10.61 +
   10.62 +    def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Option[Outer_Syntax] =
   10.63 +      nodes(name).syntax orElse loaded_theory_syntax(name)
   10.64  
   10.65      def known_theory(name: String): Option[Document.Node.Name] =
   10.66        known.theories.get(name)
   10.67 @@ -203,13 +206,13 @@
   10.68                resources.thy_info.dependencies(root_theories)
   10.69              }
   10.70  
   10.71 -            val syntax = thy_deps.syntax
   10.72 +            val overall_syntax = thy_deps.overall_syntax
   10.73  
   10.74 -            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
   10.75 +            val theory_files = thy_deps.names.map(_.path)
   10.76              val loaded_files =
   10.77                if (inlined_files) {
   10.78                  if (Sessions.is_pure(info.name)) {
   10.79 -                  (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) ::
   10.80 +                  (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) ::
   10.81                      thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
   10.82                  }
   10.83                  else thy_deps.loaded_files
   10.84 @@ -224,8 +227,10 @@
   10.85              if (list_files)
   10.86                progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
   10.87  
   10.88 -            if (check_keywords.nonEmpty)
   10.89 -              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
   10.90 +            if (check_keywords.nonEmpty) {
   10.91 +              Check_Keywords.check_keywords(
   10.92 +                progress, overall_syntax.keywords, check_keywords, theory_files)
   10.93 +            }
   10.94  
   10.95              val session_graph: Graph_Display.Graph =
   10.96              {
   10.97 @@ -251,18 +256,18 @@
   10.98                        val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
   10.99                        ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
  10.100  
  10.101 -              (graph0 /: thy_deps.deps)(
  10.102 -                { case (g, dep) =>
  10.103 -                    val a = node(dep.name)
  10.104 +              (graph0 /: thy_deps.entries)(
  10.105 +                { case (g, entry) =>
  10.106 +                    val a = node(entry.name)
  10.107                      val bs =
  10.108 -                      dep.header.imports.map({ case (name, _) => node(name) }).
  10.109 +                      entry.header.imports.map({ case (name, _) => node(name) }).
  10.110                          filterNot(_ == a)
  10.111                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
  10.112              }
  10.113  
  10.114              val known =
  10.115                Known.make(info.dir, List(imports_base),
  10.116 -                theories = thy_deps.deps.map(_.name),
  10.117 +                theories = thy_deps.names,
  10.118                  loaded_files = loaded_files)
  10.119  
  10.120              val sources =
  10.121 @@ -276,8 +281,7 @@
  10.122                  global_theories = global_theories,
  10.123                  loaded_theories = thy_deps.loaded_theories,
  10.124                  known = known,
  10.125 -                keywords = thy_deps.keywords,
  10.126 -                syntax = syntax,
  10.127 +                overall_syntax = overall_syntax,
  10.128                  sources = sources,
  10.129                  session_graph = session_graph,
  10.130                  errors = thy_deps.errors ::: sources_errors,
    11.1 --- a/src/Pure/Thy/thy_header.scala	Fri Sep 29 16:55:08 2017 +0100
    11.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Sep 29 22:45:58 2017 +0200
    11.3 @@ -138,7 +138,14 @@
    11.4        (opt($$$(ABBREVS) ~! abbrevs) ^^
    11.5          { case None => Nil case Some(_ ~ xs) => xs }) ~
    11.6        $$$(BEGIN) ^^
    11.7 -      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
    11.8 +      { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ =>
    11.9 +          val f = Symbol.decode _
   11.10 +          Thy_Header((f(name), pos),
   11.11 +            imports.map({ case (a, b) => (f(a), b) }),
   11.12 +            keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
   11.13 +              (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
   11.14 +            abbrevs.map({ case (a, b) => (f(a), f(b)) }))
   11.15 +      }
   11.16  
   11.17      val heading =
   11.18        (command(CHAPTER) |
   11.19 @@ -197,20 +204,8 @@
   11.20    }
   11.21  }
   11.22  
   11.23 -
   11.24  sealed case class Thy_Header(
   11.25    name: (String, Position.T),
   11.26    imports: List[(String, Position.T)],
   11.27    keywords: Thy_Header.Keywords,
   11.28    abbrevs: Thy_Header.Abbrevs)
   11.29 -{
   11.30 -  def decode_symbols: Thy_Header =
   11.31 -  {
   11.32 -    val f = Symbol.decode _
   11.33 -    Thy_Header((f(name._1), name._2),
   11.34 -      imports.map({ case (a, b) => (f(a), b) }),
   11.35 -      keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
   11.36 -        (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
   11.37 -      abbrevs.map({ case (a, b) => (f(a), f(b)) }))
   11.38 -  }
   11.39 -}
    12.1 --- a/src/Pure/Thy/thy_info.ML	Fri Sep 29 16:55:08 2017 +0100
    12.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Sep 29 22:45:58 2017 +0200
    12.3 @@ -160,7 +160,7 @@
    12.4    in res :: map Exn.Exn exns end;
    12.5  
    12.6  datatype task =
    12.7 -  Task of Path.T * string list * (theory list -> result) |
    12.8 +  Task of string list * (theory list -> result) |
    12.9    Finished of theory;
   12.10  
   12.11  fun task_finished (Task _) = false
   12.12 @@ -171,7 +171,7 @@
   12.13  val schedule_seq =
   12.14    String_Graph.schedule (fn deps => fn (_, task) =>
   12.15      (case task of
   12.16 -      Task (_, parents, body) =>
   12.17 +      Task (parents, body) =>
   12.18          let
   12.19            val result = body (task_parents deps parents);
   12.20            val _ = Par_Exn.release_all (join_theory result);
   12.21 @@ -185,7 +185,7 @@
   12.22      val futures = tasks
   12.23        |> String_Graph.schedule (fn deps => fn (name, task) =>
   12.24          (case task of
   12.25 -          Task (_, parents, body) =>
   12.26 +          Task (parents, body) =>
   12.27              (singleton o Future.forks)
   12.28                {name = "theory:" ^ name, group = NONE,
   12.29                  deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
   12.30 @@ -335,19 +335,10 @@
   12.31        |>> forall I
   12.32  and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
   12.33    let
   12.34 -    val {node_name, master_dir, theory_name} = Resources.import_name qualifier dir s;
   12.35 -    fun check_entry (Task (node_name', _, _)) =
   12.36 -          if op = (apply2 File.platform_path (node_name, node_name'))
   12.37 -          then ()
   12.38 -          else
   12.39 -            error ("Incoherent imports for theory " ^ quote theory_name ^
   12.40 -              Position.here require_pos ^ ":\n" ^
   12.41 -              "  " ^ Path.print node_name ^ "\n" ^
   12.42 -              "  " ^ Path.print node_name')
   12.43 -      | check_entry _ = ();
   12.44 +    val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
   12.45    in
   12.46      (case try (String_Graph.get_node tasks) theory_name of
   12.47 -      SOME task => (check_entry task; (task_finished task, tasks))
   12.48 +      SOME task => (task_finished task, tasks)
   12.49      | NONE =>
   12.50          let
   12.51            val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
   12.52 @@ -378,7 +369,7 @@
   12.53                      val load =
   12.54                        load_thy document symbols last_timing initiators update_time dep
   12.55                          text (theory_name, theory_pos) keywords;
   12.56 -                  in Task (node_name, parents, load) end);
   12.57 +                  in Task (parents, load) end);
   12.58  
   12.59            val tasks'' = new_entry theory_name parents task tasks';
   12.60          in (all_current, tasks'') end)
    13.1 --- a/src/Pure/Thy/thy_info.scala	Fri Sep 29 16:55:08 2017 +0100
    13.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Sep 29 22:45:58 2017 +0200
    13.3 @@ -7,18 +7,6 @@
    13.4  package isabelle
    13.5  
    13.6  
    13.7 -object Thy_Info
    13.8 -{
    13.9 -  /* dependencies */
   13.10 -
   13.11 -  sealed case class Dep(
   13.12 -    name: Document.Node.Name,
   13.13 -    header: Document.Node.Header)
   13.14 -  {
   13.15 -    override def toString: String = name.toString
   13.16 -  }
   13.17 -}
   13.18 -
   13.19  class Thy_Info(resources: Resources)
   13.20  {
   13.21    /* messages */
   13.22 @@ -38,64 +26,50 @@
   13.23  
   13.24    object Dependencies
   13.25    {
   13.26 -    val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty)
   13.27 +    val empty = new Dependencies(Nil, Set.empty)
   13.28    }
   13.29  
   13.30    final class Dependencies private(
   13.31 -    rev_deps: List[Thy_Info.Dep],
   13.32 -    val keywords: Thy_Header.Keywords,
   13.33 -    val abbrevs: Thy_Header.Abbrevs,
   13.34 -    val seen: Set[Document.Node.Name],
   13.35 -    val seen_theory: Multi_Map[String, (Document.Node.Name, Position.T)])
   13.36 +    rev_entries: List[Document.Node.Entry],
   13.37 +    val seen: Set[Document.Node.Name])
   13.38    {
   13.39 -    def :: (dep: Thy_Info.Dep): Dependencies =
   13.40 -      new Dependencies(
   13.41 -        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
   13.42 -        seen, seen_theory)
   13.43 +    def :: (entry: Document.Node.Entry): Dependencies =
   13.44 +      new Dependencies(entry :: rev_entries, seen)
   13.45  
   13.46 -    def + (thy: (Document.Node.Name, Position.T)): Dependencies =
   13.47 -    {
   13.48 -      val (name, _) = thy
   13.49 -      new Dependencies(rev_deps, keywords, abbrevs, seen + name, seen_theory + (name.theory -> thy))
   13.50 -    }
   13.51 +    def + (name: Document.Node.Name): Dependencies =
   13.52 +      new Dependencies(rev_entries, seen + name)
   13.53  
   13.54 -    def deps: List[Thy_Info.Dep] = rev_deps.reverse
   13.55 +    def entries: List[Document.Node.Entry] = rev_entries.reverse
   13.56 +    def names: List[Document.Node.Name] = entries.map(_.name)
   13.57 +
   13.58 +    def errors: List[String] = entries.flatMap(_.header.errors)
   13.59  
   13.60 -    def errors: List[String] =
   13.61 -    {
   13.62 -      val header_errors = deps.flatMap(dep => dep.header.errors)
   13.63 -      val import_errors =
   13.64 -        (for {
   13.65 -          (theory, imports) <- seen_theory.iterator_list
   13.66 -          if !resources.session_base.loaded_theories.isDefinedAt(theory)
   13.67 -          if imports.length > 1
   13.68 -        } yield {
   13.69 -          "Incoherent imports for theory " + quote(theory) + ":\n" +
   13.70 -            cat_lines(imports.map({ case (name, pos) =>
   13.71 -              "  " + quote(name.node) + Position.here(pos) }))
   13.72 -        }).toList
   13.73 -      header_errors ::: import_errors
   13.74 -    }
   13.75 +    lazy val loaded_theories: Graph[String, Outer_Syntax] =
   13.76 +      (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
   13.77 +        val name = entry.name.theory
   13.78 +        val imports = entry.header.imports.map(p => p._1.theory)
   13.79  
   13.80 -    lazy val syntax: Outer_Syntax =
   13.81 -      resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
   13.82 +        if (graph.defined(name))
   13.83 +          error("Duplicate loaded theory entry " + quote(name))
   13.84  
   13.85 -    def loaded_theories: Map[String, String] =
   13.86 -      (resources.session_base.loaded_theories /: rev_deps) {
   13.87 -        case (loaded, dep) =>
   13.88 -          val name = dep.name
   13.89 -          loaded + (name.theory -> name.theory) +
   13.90 -            (name.theory_base_name -> name.theory)  // legacy
   13.91 -      }
   13.92 +        for (dep <- imports if !graph.defined(dep))
   13.93 +          error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
   13.94 +
   13.95 +        val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
   13.96 +        (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
   13.97 +      })
   13.98  
   13.99      def loaded_files: List[(String, List[Path])] =
  13.100      {
  13.101 -      val names = deps.map(_.name)
  13.102        names.map(_.theory) zip
  13.103 -        Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
  13.104 +        Par_List.map((e: () => List[Path]) => e(),
  13.105 +          names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
  13.106      }
  13.107  
  13.108 -    override def toString: String = deps.toString
  13.109 +    lazy val overall_syntax: Outer_Syntax =
  13.110 +      Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
  13.111 +
  13.112 +    override def toString: String = entries.toString
  13.113    }
  13.114  
  13.115    private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
  13.116 @@ -105,13 +79,13 @@
  13.117    private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
  13.118      thy: (Document.Node.Name, Position.T)): Dependencies =
  13.119    {
  13.120 -    val (name, require_pos) = thy
  13.121 +    val (name, pos) = thy
  13.122  
  13.123      def message: String =
  13.124        "The error(s) above occurred for theory " + quote(name.theory) +
  13.125 -        required_by(initiators) + Position.here(require_pos)
  13.126 +        required_by(initiators) + Position.here(pos)
  13.127  
  13.128 -    val required1 = required + thy
  13.129 +    val required1 = required + name
  13.130      if (required.seen(name)) required
  13.131      else if (resources.session_base.loaded_theory(name)) required1
  13.132      else {
  13.133 @@ -120,11 +94,12 @@
  13.134          val header =
  13.135            try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
  13.136            catch { case ERROR(msg) => cat_error(msg, message) }
  13.137 -        Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports)
  13.138 +        Document.Node.Entry(name, header) ::
  13.139 +          require_thys(name :: initiators, required1, header.imports)
  13.140        }
  13.141        catch {
  13.142          case e: Throwable =>
  13.143 -          Thy_Info.Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
  13.144 +          Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
  13.145        }
  13.146      }
  13.147    }
    14.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 16:55:08 2017 +0100
    14.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 22:45:58 2017 +0200
    14.3 @@ -100,9 +100,10 @@
    14.4          if (node.is_empty) None
    14.5          else {
    14.6            val header = node.header
    14.7 -          val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
    14.8 -          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _)
    14.9 -            .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
   14.10 +          val imports_syntax =
   14.11 +            Outer_Syntax.merge(
   14.12 +              header.imports.flatMap(p => resources.session_base.node_syntax(nodes, p._1)))
   14.13 +          Some(imports_syntax + header)
   14.14          }
   14.15        nodes += (name -> node.update_syntax(syntax))
   14.16      }
   14.17 @@ -324,7 +325,9 @@
   14.18          node_edits foreach {
   14.19            case (name, edits) =>
   14.20              val node = nodes(name)
   14.21 -            val syntax = node.syntax getOrElse resources.session_base.syntax
   14.22 +            val syntax =
   14.23 +              resources.session_base.node_syntax(nodes, name) getOrElse
   14.24 +              Thy_Header.bootstrap_syntax
   14.25              val commands = node.commands
   14.26  
   14.27              val node1 =
    15.1 --- a/src/Pure/Tools/build.ML	Fri Sep 29 16:55:08 2017 +0100
    15.2 +++ b/src/Pure/Tools/build.ML	Fri Sep 29 22:45:58 2017 +0200
    15.3 @@ -147,7 +147,7 @@
    15.4    master_dir: Path.T,
    15.5    theories: (Options.T * (string * Position.T) list) list,
    15.6    global_theories: (string * string) list,
    15.7 -  loaded_theories: (string * string) list,
    15.8 +  loaded_theories: string list,
    15.9    known_theories: (string * string) list};
   15.10  
   15.11  fun decode_args yxml =
   15.12 @@ -162,7 +162,7 @@
   15.13            (pair string
   15.14              (pair (((list (pair Options.decode (list (pair string position))))))
   15.15                (pair (list (pair string string))
   15.16 -                (pair (list (pair string string)) (list (pair string string)))))))))))))))
   15.17 +                (pair (list string) (list (pair string string)))))))))))))))
   15.18        (YXML.parse_body yxml);
   15.19    in
   15.20      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
    16.1 --- a/src/Pure/Tools/build.scala	Fri Sep 29 16:55:08 2017 +0100
    16.2 +++ b/src/Pure/Tools/build.scala	Fri Sep 29 22:45:58 2017 +0200
    16.3 @@ -209,13 +209,13 @@
    16.4                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    16.5                  pair(string, pair(string, pair(string, pair(Path.encode,
    16.6                  pair(list(pair(Options.encode, list(pair(string, properties)))),
    16.7 -                pair(list(pair(string, string)), pair(list(pair(string, string)),
    16.8 +                pair(list(pair(string, string)), pair(list(string),
    16.9                  list(pair(string, string))))))))))))))))(
   16.10                (Symbol.codes, (command_timings, (do_output, (verbose,
   16.11                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
   16.12                  (parent, (info.chapter, (name, (Path.current,
   16.13                  (info.theories,
   16.14 -                (base.global_theories.toList, (base.loaded_theories.toList,
   16.15 +                (base.global_theories.toList, (base.loaded_theories.keys,
   16.16                  base.dest_known_theories)))))))))))))))
   16.17              })
   16.18  
    17.1 --- a/src/Pure/Tools/imports.scala	Fri Sep 29 16:55:08 2017 +0100
    17.2 +++ b/src/Pure/Tools/imports.scala	Fri Sep 29 22:45:58 2017 +0200
    17.3 @@ -105,7 +105,7 @@
    17.4            (for {
    17.5              (_, a) <- session_resources.session_base.known.theories.iterator
    17.6              if session_resources.theory_qualifier(a) == info.theory_qualifier
    17.7 -            b <- deps.all_known.get_file(Path.explode(a.node).file)
    17.8 +            b <- deps.all_known.get_file(a.path.file)
    17.9              qualifier = session_resources.theory_qualifier(b)
   17.10              if !declared_imports.contains(qualifier)
   17.11            } yield qualifier).toSet
   17.12 @@ -146,7 +146,7 @@
   17.13              val s1 =
   17.14                if (imports_base.loaded_theory(name)) name.theory
   17.15                else {
   17.16 -                imports_base.known.get_file(Path.explode(name.node).file) match {
   17.17 +                imports_base.known.get_file(name.path.file) match {
   17.18                    case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
   17.19                      name1.theory
   17.20                    case Some(name1) if Thy_Header.is_base_name(s) =>
   17.21 @@ -170,7 +170,7 @@
   17.22                (_, name) <- session_base.known.theories_local.toList
   17.23                if session_resources.theory_qualifier(name) == info.theory_qualifier
   17.24                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   17.25 -              upd <- update_name(session_base.syntax.keywords, pos,
   17.26 +              upd <- update_name(session_base.overall_syntax.keywords, pos,
   17.27                  standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
   17.28              } yield upd
   17.29  
    18.1 --- a/src/Tools/VSCode/src/build_vscode.scala	Fri Sep 29 16:55:08 2017 +0100
    18.2 +++ b/src/Tools/VSCode/src/build_vscode.scala	Fri Sep 29 22:45:58 2017 +0200
    18.3 @@ -20,7 +20,7 @@
    18.4    def build_grammar(options: Options, progress: Progress = No_Progress)
    18.5    {
    18.6      val logic = Grammar.default_logic
    18.7 -    val keywords = Sessions.session_base(options, logic).syntax.keywords
    18.8 +    val keywords = Sessions.session_base(options, logic).overall_syntax.keywords
    18.9  
   18.10      val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
   18.11      progress.echo(output_path.implode)
    19.1 --- a/src/Tools/VSCode/src/grammar.scala	Fri Sep 29 16:55:08 2017 +0100
    19.2 +++ b/src/Tools/VSCode/src/grammar.scala	Fri Sep 29 22:45:58 2017 +0200
    19.3 @@ -157,7 +157,7 @@
    19.4      val more_args = getopts(args)
    19.5      if (more_args.nonEmpty) getopts.usage()
    19.6  
    19.7 -    val keywords = Sessions.session_base(Options.init(), logic, dirs).syntax.keywords
    19.8 +    val keywords = Sessions.session_base(Options.init(), logic, dirs).overall_syntax.keywords
    19.9      val output_path = output getOrElse Path.explode(default_output(logic))
   19.10  
   19.11      Output.writeln(output_path.implode)
    20.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 29 16:55:08 2017 +0100
    20.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 29 22:45:58 2017 +0200
    20.3 @@ -216,7 +216,7 @@
    20.4            (for ((_, model) <- st.models.iterator if model.is_theory)
    20.5             yield (model.node_name, Position.none)).toList
    20.6  
    20.7 -        val thy_files = thy_info.dependencies(thys).deps.map(_.name)
    20.8 +        val thy_files = thy_info.dependencies(thys).names
    20.9  
   20.10  
   20.11          /* auxiliary files */
    21.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Sep 29 16:55:08 2017 +0100
    21.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Sep 29 22:45:58 2017 +0200
    21.3 @@ -253,7 +253,7 @@
    21.4                val pending_nodes = for ((node_name, None) <- purged) yield node_name
    21.5                (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
    21.6              }
    21.7 -            val retain = PIDE.resources.thy_info.dependencies(imports).deps.map(_.name).toSet
    21.8 +            val retain = PIDE.resources.thy_info.dependencies(imports).names.toSet
    21.9  
   21.10              for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
   21.11                yield edit
    22.1 --- a/src/Tools/jEdit/src/isabelle.scala	Fri Sep 29 16:55:08 2017 +0100
    22.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Fri Sep 29 22:45:58 2017 +0200
    22.3 @@ -50,7 +50,7 @@
    22.4  
    22.5    def mode_syntax(mode: String): Option[Outer_Syntax] =
    22.6      mode match {
    22.7 -      case "isabelle" => Some(PIDE.resources.session_base.syntax)
    22.8 +      case "isabelle" => Some(PIDE.resources.session_base.overall_syntax)
    22.9        case "isabelle-options" => Some(Options.options_syntax)
   22.10        case "isabelle-root" => Some(Sessions.root_syntax)
   22.11        case "isabelle-ml" => Some(ml_syntax)
    23.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Sep 29 16:55:08 2017 +0100
    23.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 29 22:45:58 2017 +0200
    23.3 @@ -126,7 +126,7 @@
    23.4            val thys =
    23.5              (for ((node_name, model) <- models.iterator if model.is_theory)
    23.6                yield (node_name, Position.none)).toList
    23.7 -          val thy_files = resources.thy_info.dependencies(thys).deps.map(_.name)
    23.8 +          val thy_files = resources.thy_info.dependencies(thys).names
    23.9  
   23.10            val aux_files =
   23.11              if (options.bool("jedit_auto_resolve")) {