38 (Map.empty[String, Document.Node.Name] /: (bases_iterator ++ names.iterator))({ |
38 (Map.empty[String, Document.Node.Name] /: (bases_iterator ++ names.iterator))({ |
39 case (known, name) => |
39 case (known, name) => |
40 known.get(name.theory) match { |
40 known.get(name.theory) match { |
41 case Some(name1) if name != name1 => |
41 case Some(name1) if name != name1 => |
42 error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) |
42 error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) |
43 case _ => |
43 case _ => known + (name.theory -> name) |
44 known + (name.theory -> name) + |
|
45 (Long_Name.base_name(name.theory) -> name) // legacy |
|
46 } |
44 } |
47 }) |
45 }) |
48 } |
46 } |
49 } |
47 } |
50 |
48 |
51 sealed case class Base( |
49 sealed case class Base( |
52 global_theories: Set[String] = Set.empty, |
50 global_theories: Set[String] = Set.empty, |
53 loaded_theories: Set[String] = Set.empty, |
51 loaded_theories: Map[String, Document.Node.Name] = Map.empty, |
54 known_theories: Map[String, Document.Node.Name] = Map.empty, |
52 known_theories: Map[String, Document.Node.Name] = Map.empty, |
55 keywords: Thy_Header.Keywords = Nil, |
53 keywords: Thy_Header.Keywords = Nil, |
56 syntax: Outer_Syntax = Outer_Syntax.empty, |
54 syntax: Outer_Syntax = Outer_Syntax.empty, |
57 sources: List[(Path, SHA1.Digest)] = Nil, |
55 sources: List[(Path, SHA1.Digest)] = Nil, |
58 session_graph: Graph_Display.Graph = Graph_Display.empty_graph) |
56 session_graph: Graph_Display.Graph = Graph_Display.empty_graph) |
59 { |
57 { |
60 def loaded_theory(name: Document.Node.Name): Boolean = |
58 def loaded_theory(name: Document.Node.Name): Boolean = |
61 loaded_theories.contains(name.theory) |
59 loaded_theories.isDefinedAt(name.theory) |
62 } |
60 } |
63 |
61 |
64 sealed case class Deps(sessions: Map[String, Base]) |
62 sealed case class Deps(sessions: Map[String, Base]) |
65 { |
63 { |
66 def is_empty: Boolean = sessions.isEmpty |
64 def is_empty: Boolean = sessions.isEmpty |