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( |
|
28 known_theories: Map[String, Document.Node.Name] = Map.empty, |
|
29 known_theories_local: Map[String, Document.Node.Name] = Map.empty, |
|
30 known_files: Map[JFile, List[Document.Node.Name]] = Map.empty) |
|
31 |
27 object Base |
32 object Base |
28 { |
33 { |
29 def pure(options: Options): Base = session_base(options, Thy_Header.PURE) |
34 def pure(options: Options): Base = session_base(options, Thy_Header.PURE) |
30 |
35 |
31 lazy val bootstrap: Base = |
36 lazy val bootstrap: Base = |
32 Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax) |
37 Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax) |
33 |
38 |
34 private[Sessions] def known_theories(bases: Iterable[Base], names: Iterable[Document.Node.Name]) |
39 private[Sessions] def known_theories( |
35 : (Map[String, Document.Node.Name], Map[JFile, List[Document.Node.Name]]) = |
40 local_dir: Path, |
36 { |
41 bases: List[Base], |
37 def bases_iterator = |
42 theories: List[Document.Node.Name]): Known_Theories = |
38 for { base <- bases.iterator; (_, name) <- base.known_theories.iterator } |
43 { |
39 yield name |
44 def bases_iterator(local: Boolean) = |
|
45 for { |
|
46 base <- bases.iterator |
|
47 (_, name) <- (if (local) base.known_theories_local else base.known_theories).iterator |
|
48 } yield name |
|
49 |
|
50 def local_theories_iterator = |
|
51 { |
|
52 val local_path = local_dir.file.getCanonicalFile.toPath |
|
53 theories.iterator.filter(name => |
|
54 Path.explode(name.node).file.getCanonicalFile.toPath.startsWith(local_path)) |
|
55 } |
40 |
56 |
41 val known_theories = |
57 val known_theories = |
42 (Map.empty[String, Document.Node.Name] /: (bases_iterator ++ names.iterator))({ |
58 (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({ |
43 case (known, name) => |
59 case (known, name) => |
44 known.get(name.theory) match { |
60 known.get(name.theory) match { |
45 case Some(name1) if name != name1 => |
61 case Some(name1) if name != name1 => |
46 error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) |
62 error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) |
47 case _ => known + (name.theory -> name) |
63 case _ => known + (name.theory -> name) |
48 } |
64 } |
49 }) |
65 }) |
|
66 val known_theories_local = |
|
67 (Map.empty[String, Document.Node.Name] /: |
|
68 (bases_iterator(true) ++ local_theories_iterator))({ |
|
69 case (known, name) => known + (name.theory -> name) |
|
70 }) |
50 val known_files = |
71 val known_files = |
51 (Map.empty[JFile, List[Document.Node.Name]] /: (bases_iterator ++ names.iterator))({ |
72 (Map.empty[JFile, List[Document.Node.Name]] /: |
|
73 (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({ |
52 case (known, name) => |
74 case (known, name) => |
53 val file = Path.explode(name.node).file.getCanonicalFile |
75 val file = Path.explode(name.node).file.getCanonicalFile |
54 val names1 = known.getOrElse(file, Nil) |
76 val theories1 = known.getOrElse(file, Nil) |
55 if (names1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) |
77 if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) |
56 known |
78 known |
57 else known + (file -> (name :: names1)) |
79 else known + (file -> (name :: theories1)) |
58 }) |
80 }) |
59 (known_theories, known_files) |
81 Known_Theories(known_theories, known_theories_local, |
|
82 known_files.iterator.map(p => (p._1, p._2.reverse)).toMap) |
60 } |
83 } |
61 } |
84 } |
62 |
85 |
63 sealed case class Base( |
86 sealed case class Base( |
64 global_theories: Map[String, String] = Map.empty, |
87 global_theories: Map[String, String] = Map.empty, |
65 loaded_theories: Map[String, Document.Node.Name] = Map.empty, |
88 loaded_theories: Map[String, Document.Node.Name] = Map.empty, |
66 known_theories: Map[String, Document.Node.Name] = Map.empty, |
89 known_theories: Map[String, Document.Node.Name] = Map.empty, |
67 known_files: Map[JFile, List[Document.Node.Name]] = Multi_Map.empty, |
90 known_theories_local: Map[String, Document.Node.Name] = Map.empty, |
|
91 known_files: Map[JFile, List[Document.Node.Name]] = Map.empty, |
68 keywords: Thy_Header.Keywords = Nil, |
92 keywords: Thy_Header.Keywords = Nil, |
69 syntax: Outer_Syntax = Outer_Syntax.empty, |
93 syntax: Outer_Syntax = Outer_Syntax.empty, |
70 sources: List[(Path, SHA1.Digest)] = Nil, |
94 sources: List[(Path, SHA1.Digest)] = Nil, |
71 session_graph: Graph_Display.Graph = Graph_Display.empty_graph) |
95 session_graph: Graph_Display.Graph = Graph_Display.empty_graph) |
72 { |
96 { |
|
97 def platform_path: Base = |
|
98 copy( |
|
99 loaded_theories = |
|
100 for ((a, b) <- loaded_theories) yield (a, b.map(File.platform_path(_))), |
|
101 known_theories = |
|
102 for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))), |
|
103 known_theories_local = |
|
104 for ((a, b) <- known_theories_local) yield (a, b.map(File.platform_path(_))), |
|
105 known_files = |
|
106 for ((a, b) <- known_files) yield (a, b.map(c => c.map(File.platform_path(_))))) |
|
107 |
73 def loaded_theory(name: Document.Node.Name): Boolean = |
108 def loaded_theory(name: Document.Node.Name): Boolean = |
74 loaded_theories.isDefinedAt(name.theory) |
109 loaded_theories.isDefinedAt(name.theory) |
75 |
110 |
76 def dest_loaded_theories: List[(String, String)] = |
111 def dest_loaded_theories: List[(String, String)] = |
77 for ((theory, node_name) <- loaded_theories.toList) |
112 for ((theory, node_name) <- loaded_theories.toList) |
80 def dest_known_theories: List[(String, String)] = |
115 def dest_known_theories: List[(String, String)] = |
81 for ((theory, node_name) <- known_theories.toList) |
116 for ((theory, node_name) <- known_theories.toList) |
82 yield (theory, node_name.node) |
117 yield (theory, node_name.node) |
83 } |
118 } |
84 |
119 |
85 sealed case class Deps(sessions: Map[String, Base]) |
120 sealed case class Deps( |
86 { |
121 session_bases: Map[String, Base], |
87 def is_empty: Boolean = sessions.isEmpty |
122 all_known_theories: Known_Theories) |
88 def apply(name: String): Base = sessions(name) |
123 { |
89 def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2) |
124 def is_empty: Boolean = session_bases.isEmpty |
90 |
125 def apply(name: String): Base = session_bases(name) |
91 def all_known_theories: (Map[String, Document.Node.Name], Map[JFile, List[Document.Node.Name]]) = |
126 def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2) |
92 Base.known_theories(sessions.toList.map(_._2), Nil) |
|
93 } |
127 } |
94 |
128 |
95 def deps(sessions: T, |
129 def deps(sessions: T, |
96 progress: Progress = No_Progress, |
130 progress: Progress = No_Progress, |
97 inlined_files: Boolean = false, |
131 inlined_files: Boolean = false, |
98 verbose: Boolean = false, |
132 verbose: Boolean = false, |
99 list_files: Boolean = false, |
133 list_files: Boolean = false, |
100 check_keywords: Set[String] = Set.empty, |
134 check_keywords: Set[String] = Set.empty, |
101 global_theories: Map[String, String] = Map.empty): Deps = |
135 global_theories: Map[String, String] = Map.empty, |
102 { |
136 all_known_theories: Boolean = false): Deps = |
103 Deps((Map.empty[String, Base] /: sessions.imports_topological_order)({ |
137 { |
104 case (sessions, (session_name, info)) => |
138 val session_bases = |
105 if (progress.stopped) throw Exn.Interrupt() |
139 (Map.empty[String, Base] /: sessions.imports_topological_order)({ |
106 |
140 case (session_bases, (session_name, info)) => |
107 try { |
141 if (progress.stopped) throw Exn.Interrupt() |
108 val parent_base = |
142 |
109 info.parent match { |
143 try { |
110 case None => Base.bootstrap |
144 val parent_base = |
111 case Some(parent) => sessions(parent) |
145 info.parent match { |
|
146 case None => Base.bootstrap |
|
147 case Some(parent) => session_bases(parent) |
|
148 } |
|
149 val resources = new Resources(parent_base, |
|
150 default_qualifier = info.theory_qualifier(session_name)) |
|
151 |
|
152 if (verbose || list_files) { |
|
153 val groups = |
|
154 if (info.groups.isEmpty) "" |
|
155 else info.groups.mkString(" (", " ", ")") |
|
156 progress.echo("Session " + info.chapter + "/" + session_name + groups) |
112 } |
157 } |
113 val resources = new Resources(parent_base, |
158 |
114 default_qualifier = info.theory_qualifier(session_name)) |
159 val thy_deps = |
115 |
160 { |
116 if (verbose || list_files) { |
161 val root_theories = |
117 val groups = |
162 info.theories.flatMap({ case (_, thys) => |
118 if (info.groups.isEmpty) "" |
163 thys.map(thy => |
119 else info.groups.mkString(" (", " ", ")") |
164 (resources.import_name(session_name, info.dir.implode, thy), info.pos)) |
120 progress.echo("Session " + info.chapter + "/" + session_name + groups) |
165 }) |
|
166 val thy_deps = resources.thy_info.dependencies(root_theories) |
|
167 |
|
168 thy_deps.errors match { |
|
169 case Nil => thy_deps |
|
170 case errs => error(cat_lines(errs)) |
|
171 } |
|
172 } |
|
173 |
|
174 val known_theories = |
|
175 Base.known_theories(info.dir, |
|
176 parent_base :: info.imports.map(session_bases(_)), |
|
177 thy_deps.deps.map(_.name)) |
|
178 |
|
179 val syntax = thy_deps.syntax |
|
180 |
|
181 val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node)) |
|
182 val loaded_files = |
|
183 if (inlined_files) { |
|
184 val pure_files = |
|
185 if (is_pure(session_name)) { |
|
186 val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1)) |
|
187 val files = |
|
188 roots.flatMap(root => resources.loaded_files(syntax, File.read(root))). |
|
189 map(file => info.dir + Path.explode(file)) |
|
190 roots ::: files |
|
191 } |
|
192 else Nil |
|
193 pure_files ::: thy_deps.loaded_files |
|
194 } |
|
195 else Nil |
|
196 |
|
197 val all_files = |
|
198 (theory_files ::: loaded_files ::: |
|
199 info.files.map(file => info.dir + file) ::: |
|
200 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) |
|
201 |
|
202 if (list_files) |
|
203 progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _))) |
|
204 |
|
205 if (check_keywords.nonEmpty) |
|
206 Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files) |
|
207 |
|
208 val base = |
|
209 Base(global_theories = global_theories, |
|
210 loaded_theories = thy_deps.loaded_theories, |
|
211 known_theories = known_theories.known_theories, |
|
212 known_theories_local = known_theories.known_theories_local, |
|
213 known_files = known_theories.known_files, |
|
214 keywords = thy_deps.keywords, |
|
215 syntax = syntax, |
|
216 sources = all_files.map(p => (p, SHA1.digest(p.file))), |
|
217 session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base)) |
|
218 |
|
219 session_bases + (session_name -> base) |
121 } |
220 } |
122 |
221 catch { |
123 val thy_deps = |
222 case ERROR(msg) => |
124 { |
223 cat_error(msg, "The error(s) above occurred in session " + |
125 val root_theories = |
224 quote(session_name) + Position.here(info.pos)) |
126 info.theories.flatMap({ case (_, thys) => |
|
127 thys.map(thy => |
|
128 (resources.import_name(session_name, info.dir.implode, thy), info.pos)) |
|
129 }) |
|
130 val thy_deps = resources.thy_info.dependencies(root_theories) |
|
131 |
|
132 thy_deps.errors match { |
|
133 case Nil => thy_deps |
|
134 case errs => error(cat_lines(errs)) |
|
135 } |
|
136 } |
225 } |
137 |
226 }) |
138 val (known_theories, known_files) = |
227 |
139 Base.known_theories( |
228 val known_theories = |
140 parent_base :: info.imports.map(sessions(_)), thy_deps.deps.map(_.name)) |
229 if (all_known_theories) |
141 |
230 Base.known_theories(Path.current, session_bases.toList.map(_._2), Nil) |
142 val syntax = thy_deps.syntax |
231 else Known_Theories() |
143 |
232 |
144 val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node)) |
233 Deps(session_bases, known_theories) |
145 val loaded_files = |
|
146 if (inlined_files) { |
|
147 val pure_files = |
|
148 if (is_pure(session_name)) { |
|
149 val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1)) |
|
150 val files = |
|
151 roots.flatMap(root => resources.loaded_files(syntax, File.read(root))). |
|
152 map(file => info.dir + Path.explode(file)) |
|
153 roots ::: files |
|
154 } |
|
155 else Nil |
|
156 pure_files ::: thy_deps.loaded_files |
|
157 } |
|
158 else Nil |
|
159 |
|
160 val all_files = |
|
161 (theory_files ::: loaded_files ::: |
|
162 info.files.map(file => info.dir + file) ::: |
|
163 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) |
|
164 |
|
165 if (list_files) |
|
166 progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _))) |
|
167 |
|
168 if (check_keywords.nonEmpty) |
|
169 Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files) |
|
170 |
|
171 val base = |
|
172 Base(global_theories = global_theories, |
|
173 loaded_theories = thy_deps.loaded_theories, |
|
174 known_theories = known_theories, |
|
175 known_files = known_files, |
|
176 keywords = thy_deps.keywords, |
|
177 syntax = syntax, |
|
178 sources = all_files.map(p => (p, SHA1.digest(p.file))), |
|
179 session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base)) |
|
180 |
|
181 sessions + (session_name -> base) |
|
182 } |
|
183 catch { |
|
184 case ERROR(msg) => |
|
185 cat_error(msg, "The error(s) above occurred in session " + |
|
186 quote(session_name) + Position.here(info.pos)) |
|
187 } |
|
188 })) |
|
189 } |
234 } |
190 |
235 |
191 def session_base( |
236 def session_base( |
192 options: Options, |
237 options: Options, |
193 session: String, |
238 session: String, |