22 |
22 |
23 val DRAFT = "Draft" |
23 val DRAFT = "Draft" |
24 |
24 |
25 def is_pure(name: String): Boolean = name == Thy_Header.PURE |
25 def is_pure(name: String): Boolean = name == Thy_Header.PURE |
26 |
26 |
27 sealed case class Known_Theories( |
27 object Known |
28 known_theories: Map[String, Document.Node.Name] = Map.empty, |
28 { |
29 known_theories_local: Map[String, Document.Node.Name] = Map.empty, |
29 val empty: Known = Known() |
30 known_files: Map[JFile, List[Document.Node.Name]] = Map.empty) |
30 |
31 |
31 def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known = |
32 object Base |
|
33 { |
|
34 def pure(options: Options): Base = session_base(options, Thy_Header.PURE) |
|
35 |
|
36 def bootstrap(global_theories: Map[String, String]): Base = |
|
37 Base( |
|
38 global_theories = global_theories, |
|
39 keywords = Thy_Header.bootstrap_header, |
|
40 syntax = Thy_Header.bootstrap_syntax) |
|
41 |
|
42 private[Sessions] def known_theories( |
|
43 local_dir: Path, |
|
44 bases: List[Base], |
|
45 theories: List[Document.Node.Name]): Known_Theories = |
|
46 { |
32 { |
47 def bases_iterator(local: Boolean) = |
33 def bases_iterator(local: Boolean) = |
48 for { |
34 for { |
49 base <- bases.iterator |
35 base <- bases.iterator |
50 (_, name) <- (if (local) base.known_theories_local else base.known_theories).iterator |
36 (_, name) <- (if (local) base.known_theories_local else base.known_theories).iterator |
79 val theories1 = known.getOrElse(file, Nil) |
65 val theories1 = known.getOrElse(file, Nil) |
80 if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) |
66 if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) |
81 known |
67 known |
82 else known + (file -> (name :: theories1)) |
68 else known + (file -> (name :: theories1)) |
83 }) |
69 }) |
84 Known_Theories(known_theories, known_theories_local, |
70 Known(known_theories, known_theories_local, |
85 known_files.iterator.map(p => (p._1, p._2.reverse)).toMap) |
71 known_files.iterator.map(p => (p._1, p._2.reverse)).toMap) |
86 } |
72 } |
87 } |
73 } |
88 |
74 |
89 sealed case class Base( |
75 sealed case class Known( |
90 global_theories: Map[String, String] = Map.empty, |
|
91 loaded_theories: Map[String, String] = Map.empty, |
|
92 known_theories: Map[String, Document.Node.Name] = Map.empty, |
76 known_theories: Map[String, Document.Node.Name] = Map.empty, |
93 known_theories_local: Map[String, Document.Node.Name] = Map.empty, |
77 known_theories_local: Map[String, Document.Node.Name] = Map.empty, |
94 known_files: Map[JFile, List[Document.Node.Name]] = Map.empty, |
78 known_files: Map[JFile, List[Document.Node.Name]] = Map.empty) |
95 keywords: Thy_Header.Keywords = Nil, |
79 { |
96 syntax: Outer_Syntax = Outer_Syntax.empty, |
80 def platform_path: Known = |
97 sources: List[(Path, SHA1.Digest)] = Nil, |
|
98 session_graph: Graph_Display.Graph = Graph_Display.empty_graph) |
|
99 { |
|
100 def platform_path: Base = |
|
101 copy( |
81 copy( |
102 known_theories = |
82 known_theories = |
103 for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))), |
83 for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))), |
104 known_theories_local = |
84 known_theories_local = |
105 for ((a, b) <- known_theories_local) yield (a, b.map(File.platform_path(_))), |
85 for ((a, b) <- known_theories_local) yield (a, b.map(File.platform_path(_))), |
106 known_files = |
86 known_files = |
107 for ((a, b) <- known_files) yield (a, b.map(c => c.map(File.platform_path(_))))) |
87 for ((a, b) <- known_files) yield (a, b.map(c => c.map(File.platform_path(_))))) |
|
88 } |
|
89 |
|
90 object Base |
|
91 { |
|
92 def pure(options: Options): Base = session_base(options, Thy_Header.PURE) |
|
93 |
|
94 def bootstrap(global_theories: Map[String, String]): Base = |
|
95 Base( |
|
96 global_theories = global_theories, |
|
97 keywords = Thy_Header.bootstrap_header, |
|
98 syntax = Thy_Header.bootstrap_syntax) |
|
99 } |
|
100 |
|
101 sealed case class Base( |
|
102 global_theories: Map[String, String] = Map.empty, |
|
103 loaded_theories: Map[String, String] = Map.empty, |
|
104 known: Known = Known.empty, |
|
105 keywords: Thy_Header.Keywords = Nil, |
|
106 syntax: Outer_Syntax = Outer_Syntax.empty, |
|
107 sources: List[(Path, SHA1.Digest)] = Nil, |
|
108 session_graph: Graph_Display.Graph = Graph_Display.empty_graph) |
|
109 { |
|
110 def platform_path: Base = copy(known = known.platform_path) |
108 |
111 |
109 def loaded_theory(name: Document.Node.Name): Boolean = |
112 def loaded_theory(name: Document.Node.Name): Boolean = |
110 loaded_theories.isDefinedAt(name.theory) |
113 loaded_theories.isDefinedAt(name.theory) |
|
114 |
|
115 def known_theories: Map[String, Document.Node.Name] = known.known_theories |
|
116 def known_theories_local: Map[String, Document.Node.Name] = known.known_theories_local |
|
117 def known_files: Map[JFile, List[Document.Node.Name]] = known.known_files |
111 |
118 |
112 def dest_known_theories: List[(String, String)] = |
119 def dest_known_theories: List[(String, String)] = |
113 for ((theory, node_name) <- known_theories.toList) |
120 for ((theory, node_name) <- known_theories.toList) |
114 yield (theory, node_name.node) |
121 yield (theory, node_name.node) |
115 } |
122 } |
116 |
123 |
117 sealed case class Deps( |
124 sealed case class Deps(session_bases: Map[String, Base], all_known: Known) |
118 session_bases: Map[String, Base], |
|
119 all_known_theories: Known_Theories) |
|
120 { |
125 { |
121 def is_empty: Boolean = session_bases.isEmpty |
126 def is_empty: Boolean = session_bases.isEmpty |
122 def apply(name: String): Base = session_bases(name) |
127 def apply(name: String): Base = session_bases(name) |
123 def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2) |
128 def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2) |
124 } |
129 } |
128 inlined_files: Boolean = false, |
133 inlined_files: Boolean = false, |
129 verbose: Boolean = false, |
134 verbose: Boolean = false, |
130 list_files: Boolean = false, |
135 list_files: Boolean = false, |
131 check_keywords: Set[String] = Set.empty, |
136 check_keywords: Set[String] = Set.empty, |
132 global_theories: Map[String, String] = Map.empty, |
137 global_theories: Map[String, String] = Map.empty, |
133 all_known_theories: Boolean = false): Deps = |
138 all_known: Boolean = false): Deps = |
134 { |
139 { |
135 val session_bases = |
140 val session_bases = |
136 (Map.empty[String, Base] /: sessions.imports_topological_order)({ |
141 (Map.empty[String, Base] /: sessions.imports_topological_order)({ |
137 case (session_bases, (session_name, info)) => |
142 case (session_bases, (session_name, info)) => |
138 if (progress.stopped) throw Exn.Interrupt() |
143 if (progress.stopped) throw Exn.Interrupt() |
203 Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files) |
208 Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files) |
204 |
209 |
205 val base = |
210 val base = |
206 Base(global_theories = global_theories, |
211 Base(global_theories = global_theories, |
207 loaded_theories = thy_deps.loaded_theories, |
212 loaded_theories = thy_deps.loaded_theories, |
208 known_theories = known_theories.known_theories, |
213 known = known, |
209 known_theories_local = known_theories.known_theories_local, |
|
210 known_files = known_theories.known_files, |
|
211 keywords = thy_deps.keywords, |
214 keywords = thy_deps.keywords, |
212 syntax = syntax, |
215 syntax = syntax, |
213 sources = all_files.map(p => (p, SHA1.digest(p.file))), |
216 sources = all_files.map(p => (p, SHA1.digest(p.file))), |
214 session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base)) |
217 session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base)) |
215 |
218 |
220 cat_error(msg, "The error(s) above occurred in session " + |
223 cat_error(msg, "The error(s) above occurred in session " + |
221 quote(session_name) + Position.here(info.pos)) |
224 quote(session_name) + Position.here(info.pos)) |
222 } |
225 } |
223 }) |
226 }) |
224 |
227 |
225 val known_theories = |
228 val known = |
226 if (all_known_theories) |
229 if (all_known) Known.make(Path.current, session_bases.toList.map(_._2), Nil) |
227 Base.known_theories(Path.current, session_bases.toList.map(_._2), Nil) |
230 else Known.empty |
228 else Known_Theories() |
231 |
229 |
232 Deps(session_bases, known) |
230 Deps(session_bases, known_theories) |
|
231 } |
233 } |
232 |
234 |
233 def session_base( |
235 def session_base( |
234 options: Options, |
236 options: Options, |
235 session: String, |
237 session: String, |
236 dirs: List[Path] = Nil, |
238 dirs: List[Path] = Nil, |
237 all_known_theories: Boolean = false): Base = |
239 all_known: Boolean = false): Base = |
238 { |
240 { |
239 val full_sessions = load(options, dirs = dirs) |
241 val full_sessions = load(options, dirs = dirs) |
240 val global_theories = full_sessions.global_theories |
242 val global_theories = full_sessions.global_theories |
241 val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2 |
243 val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2 |
242 |
244 |
243 if (all_known_theories) { |
245 if (all_known) { |
244 val deps = Sessions.deps( |
246 val deps = Sessions.deps( |
245 full_sessions, global_theories = global_theories, all_known_theories = all_known_theories) |
247 full_sessions, global_theories = global_theories, all_known = all_known) |
246 deps(session).copy( |
248 deps(session).copy(known = deps.all_known) |
247 known_theories = deps.all_known_theories.known_theories, |
|
248 known_theories_local = deps.all_known_theories.known_theories_local, |
|
249 known_files = deps.all_known_theories.known_files) |
|
250 } |
249 } |
251 else |
250 else |
252 deps(selected_sessions, global_theories = global_theories)(session) |
251 deps(selected_sessions, global_theories = global_theories)(session) |
253 } |
252 } |
254 |
253 |