39 { |
39 { |
40 val empty: Known = Known() |
40 val empty: Known = Known() |
41 |
41 |
42 def make(local_dir: Path, bases: List[Base], |
42 def make(local_dir: Path, bases: List[Base], |
43 sessions: List[(String, Position.T)] = Nil, |
43 sessions: List[(String, Position.T)] = Nil, |
44 theories: List[Document.Node.Name] = Nil, |
44 theories: List[Document.Node.Entry] = Nil, |
45 loaded_files: List[(String, List[Path])] = Nil): Known = |
45 loaded_files: List[(String, List[Path])] = Nil): Known = |
46 { |
46 { |
47 def bases_iterator(local: Boolean) = |
47 def bases_iterator(local: Boolean) = |
48 for { |
48 for { |
49 base <- bases.iterator |
49 base <- bases.iterator |
50 (_, name) <- (if (local) base.known.theories_local else base.known.theories).iterator |
50 (_, entry) <- (if (local) base.known.theories_local else base.known.theories).iterator |
51 } yield name |
51 } yield entry |
52 |
52 |
53 def local_theories_iterator = |
53 def local_theories_iterator = |
54 { |
54 { |
55 val local_path = local_dir.canonical_file.toPath |
55 val local_path = local_dir.canonical_file.toPath |
56 theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path)) |
56 theories.iterator.filter(entry => |
|
57 entry.name.path.canonical_file.toPath.startsWith(local_path)) |
57 } |
58 } |
58 |
59 |
59 val known_sessions = |
60 val known_sessions = |
60 (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions }) |
61 (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions }) |
61 |
62 |
62 val known_theories = |
63 val known_theories = |
63 (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({ |
64 (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({ |
64 case (known, name) => |
65 case (known, entry) => |
65 known.get(name.theory) match { |
66 known.get(entry.name.theory) match { |
66 case Some(name1) if name != name1 => |
67 case Some(entry1) if entry.name != entry1.name => |
67 error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) |
68 error("Duplicate theory " + quote(entry.name.node) + " vs. " + |
68 case _ => known + (name.theory -> name) |
69 quote(entry1.name.node)) |
|
70 case _ => known + (entry.name.theory -> entry) |
69 } |
71 } |
70 }) |
72 }) |
71 val known_theories_local = |
73 val known_theories_local = |
72 (Map.empty[String, Document.Node.Name] /: |
74 (Map.empty[String, Document.Node.Entry] /: |
73 (bases_iterator(true) ++ local_theories_iterator))({ |
75 (bases_iterator(true) ++ local_theories_iterator))({ |
74 case (known, name) => known + (name.theory -> name) |
76 case (known, entry) => known + (entry.name.theory -> entry) |
75 }) |
77 }) |
76 val known_files = |
78 val known_files = |
77 (Map.empty[JFile, List[Document.Node.Name]] /: |
79 (Map.empty[JFile, List[Document.Node.Name]] /: |
78 (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({ |
80 (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({ |
79 case (known, name) => |
81 case (known, entry) => |
|
82 val name = entry.name |
80 val file = name.path.canonical_file |
83 val file = name.path.canonical_file |
81 val theories1 = known.getOrElse(file, Nil) |
84 val theories1 = known.getOrElse(file, Nil) |
82 if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) |
85 if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) |
83 known |
86 known |
84 else known + (file -> (name :: theories1)) |
87 else known + (file -> (name :: theories1)) |
87 val known_loaded_files = |
90 val known_loaded_files = |
88 (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _) |
91 (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _) |
89 |
92 |
90 Known( |
93 Known( |
91 known_sessions, |
94 known_sessions, |
92 known_theories, known_theories_local, |
95 known_theories, |
|
96 known_theories_local, |
93 known_files.iterator.map(p => (p._1, p._2.reverse)).toMap, |
97 known_files.iterator.map(p => (p._1, p._2.reverse)).toMap, |
94 known_loaded_files) |
98 known_loaded_files) |
95 } |
99 } |
96 } |
100 } |
97 |
101 |
98 sealed case class Known( |
102 sealed case class Known( |
99 sessions: Map[String, Position.T] = Map.empty, |
103 sessions: Map[String, Position.T] = Map.empty, |
100 theories: Map[String, Document.Node.Name] = Map.empty, |
104 theories: Map[String, Document.Node.Entry] = Map.empty, |
101 theories_local: Map[String, Document.Node.Name] = Map.empty, |
105 theories_local: Map[String, Document.Node.Entry] = Map.empty, |
102 files: Map[JFile, List[Document.Node.Name]] = Map.empty, |
106 files: Map[JFile, List[Document.Node.Name]] = Map.empty, |
103 loaded_files: Map[String, List[Path]] = Map.empty) |
107 loaded_files: Map[String, List[Path]] = Map.empty) |
104 { |
108 { |
105 def platform_path: Known = |
109 def platform_path: Known = |
106 copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))), |
110 copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))), |
109 |
113 |
110 def standard_path: Known = |
114 def standard_path: Known = |
111 copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))), |
115 copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))), |
112 theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))), |
116 theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))), |
113 files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_))))) |
117 files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_))))) |
|
118 |
|
119 def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList |
|
120 |
|
121 lazy val theory_graph: Graph[Document.Node.Name, Unit] = |
|
122 { |
|
123 val graph0 = |
|
124 (Graph.empty[Document.Node.Name, Unit](Document.Node.Name.Ordering) /: theories)( |
|
125 { |
|
126 case (g1, (_, entry)) => |
|
127 (g1.default_node(entry.name, ()) /: entry.header.imports)( |
|
128 { case (g2, (parent, _)) => g2.default_node(parent, ()) }) |
|
129 }) |
|
130 (graph0 /: theories)( |
|
131 { |
|
132 case (g1, (_, entry)) => |
|
133 (g1 /: entry.header.imports)( |
|
134 { case (g2, (parent, _)) => g2.add_edge(parent, entry.name) }) |
|
135 }) |
|
136 } |
114 |
137 |
115 def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] = |
138 def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] = |
116 { |
139 { |
117 val res = files.getOrElse(File.canonical(file), Nil).headOption |
140 val res = files.getOrElse(File.canonical(file), Nil).headOption |
118 if (bootstrap) res.map(_.map_theory(Thy_Header.bootstrap_name(_))) else res |
141 if (bootstrap) res.map(_.map_theory(Thy_Header.bootstrap_name(_))) else res |
157 |
180 |
158 def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax = |
181 def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax = |
159 nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax |
182 nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax |
160 |
183 |
161 def known_theory(name: String): Option[Document.Node.Name] = |
184 def known_theory(name: String): Option[Document.Node.Name] = |
162 known.theories.get(name) |
185 known.theories.get(name).map(_.name) |
163 |
186 |
164 def dest_known_theories: List[(String, String)] = |
187 def dest_known_theories: List[(String, String)] = |
165 for ((theory, node_name) <- known.theories.toList) |
188 for ((theory, entry) <- known.theories.toList) |
166 yield (theory, node_name.node) |
189 yield (theory, entry.name.node) |
167 |
190 |
168 def get_imports: Base = imports getOrElse Base.bootstrap(global_theories) |
191 def get_imports: Base = imports getOrElse Base.bootstrap(global_theories) |
169 } |
192 } |
170 |
193 |
171 sealed case class Deps( |
194 sealed case class Deps( |