93 def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax = |
93 def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax = |
94 nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax |
94 nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax |
95 } |
95 } |
96 |
96 |
97 val bootstrap_base: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax) |
97 val bootstrap_base: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax) |
98 |
|
99 sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) { |
|
100 override def toString: String = "Sessions.Deps(" + sessions_structure + ")" |
|
101 |
|
102 def is_empty: Boolean = session_bases.keysIterator.forall(_.isEmpty) |
|
103 def apply(name: String): Base = session_bases(name) |
|
104 def get(name: String): Option[Base] = session_bases.get(name) |
|
105 |
|
106 def imported_sources(name: String): List[SHA1.Digest] = |
|
107 session_bases(name).imported_sources.map(_._2) |
|
108 |
|
109 def session_sources(name: String): List[SHA1.Digest] = |
|
110 session_bases(name).session_sources.map(_._2) |
|
111 |
|
112 def errors: List[String] = |
|
113 (for { |
|
114 (name, base) <- session_bases.iterator |
|
115 if base.errors.nonEmpty |
|
116 } yield cat_lines(base.errors) + |
|
117 "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.session_pos) |
|
118 ).toList |
|
119 |
|
120 def check_errors: Deps = |
|
121 errors match { |
|
122 case Nil => this |
|
123 case errs => error(cat_lines(errs)) |
|
124 } |
|
125 |
|
126 def base_info(session: String): Base_Info = |
|
127 Base_Info(base = apply(session), sessions_structure = sessions_structure, errors = errors) |
|
128 } |
|
129 |
|
130 def deps(sessions_structure: Structure, |
|
131 progress: Progress = new Progress, |
|
132 inlined_files: Boolean = false, |
|
133 verbose: Boolean = false, |
|
134 list_files: Boolean = false, |
|
135 check_keywords: Set[String] = Set.empty |
|
136 ): Deps = { |
|
137 var cache_sources = Map.empty[JFile, SHA1.Digest] |
|
138 def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = { |
|
139 for { |
|
140 path <- paths |
|
141 file = path.file |
|
142 if cache_sources.isDefinedAt(file) || file.isFile |
|
143 } |
|
144 yield { |
|
145 cache_sources.get(file) match { |
|
146 case Some(digest) => (path, digest) |
|
147 case None => |
|
148 val digest = SHA1.digest(file) |
|
149 cache_sources = cache_sources + (file -> digest) |
|
150 (path, digest) |
|
151 } |
|
152 } |
|
153 } |
|
154 |
|
155 val session_bases = |
|
156 sessions_structure.imports_topological_order.foldLeft( |
|
157 Map(Sessions.bootstrap_base.session_entry)) { |
|
158 case (session_bases, session_name) => |
|
159 progress.expose_interrupt() |
|
160 |
|
161 val info = sessions_structure(session_name) |
|
162 try { |
|
163 val deps_base = info.deps_base(session_bases) |
|
164 val resources = new Resources(sessions_structure, deps_base) |
|
165 |
|
166 if (verbose || list_files) { |
|
167 val groups = |
|
168 if (info.groups.isEmpty) "" |
|
169 else info.groups.mkString(" (", " ", ")") |
|
170 progress.echo("Session " + info.chapter + "/" + session_name + groups) |
|
171 } |
|
172 |
|
173 val dependencies = resources.session_dependencies(info) |
|
174 |
|
175 val overall_syntax = dependencies.overall_syntax |
|
176 |
|
177 val proper_session_theories = |
|
178 dependencies.theories.filter(name => |
|
179 sessions_structure.theory_qualifier(name) == session_name) |
|
180 |
|
181 val theory_files = dependencies.theories.map(_.path) |
|
182 |
|
183 val (load_commands, load_commands_errors) = |
|
184 try { if (inlined_files) (dependencies.load_commands, Nil) else (Nil, Nil) } |
|
185 catch { case ERROR(msg) => (Nil, List(msg)) } |
|
186 |
|
187 val loaded_files = |
|
188 load_commands.map({ case (name, spans) => dependencies.loaded_files(name, spans) }) |
|
189 |
|
190 val session_files = |
|
191 (theory_files ::: loaded_files.flatMap(_._2) ::: |
|
192 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) |
|
193 |
|
194 val imported_files = if (inlined_files) dependencies.imported_files else Nil |
|
195 |
|
196 if (list_files) { |
|
197 progress.echo(cat_lines(session_files.map(_.implode).sorted.map(" " + _))) |
|
198 } |
|
199 |
|
200 if (check_keywords.nonEmpty) { |
|
201 Check_Keywords.check_keywords( |
|
202 progress, overall_syntax.keywords, check_keywords, theory_files) |
|
203 } |
|
204 |
|
205 val session_graph_display: Graph_Display.Graph = { |
|
206 def session_node(name: String): Graph_Display.Node = |
|
207 Graph_Display.Node("[" + name + "]", "session." + name) |
|
208 |
|
209 def node(name: Document.Node.Name): Graph_Display.Node = { |
|
210 val qualifier = sessions_structure.theory_qualifier(name) |
|
211 if (qualifier == info.name) { |
|
212 Graph_Display.Node(name.theory_base_name, "theory." + name.theory) |
|
213 } |
|
214 else session_node(qualifier) |
|
215 } |
|
216 |
|
217 val required_sessions = |
|
218 dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory)) |
|
219 .map(theory => sessions_structure.theory_qualifier(theory)) |
|
220 .filter(name => name != info.name && sessions_structure.defined(name)) |
|
221 |
|
222 val required_subgraph = |
|
223 sessions_structure.imports_graph |
|
224 .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet) |
|
225 .transitive_closure |
|
226 .restrict(required_sessions.toSet) |
|
227 .transitive_reduction_acyclic |
|
228 |
|
229 val graph0 = |
|
230 required_subgraph.topological_order.foldLeft(Graph_Display.empty_graph) { |
|
231 case (g, session) => |
|
232 val a = session_node(session) |
|
233 val bs = required_subgraph.imm_preds(session).toList.map(session_node) |
|
234 bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a)) |
|
235 } |
|
236 |
|
237 dependencies.entries.foldLeft(graph0) { |
|
238 case (g, entry) => |
|
239 val a = node(entry.name) |
|
240 val bs = entry.header.imports.map(node).filterNot(_ == a) |
|
241 bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a)) |
|
242 } |
|
243 } |
|
244 |
|
245 val known_theories = |
|
246 dependencies.entries.iterator.map(entry => entry.name.theory -> entry). |
|
247 foldLeft(deps_base.known_theories)(_ + _) |
|
248 |
|
249 val known_loaded_files = deps_base.known_loaded_files ++ loaded_files |
|
250 |
|
251 val import_errors = { |
|
252 val known_sessions = |
|
253 sessions_structure.imports_requirements(List(session_name)).toSet |
|
254 for { |
|
255 name <- dependencies.theories |
|
256 qualifier = sessions_structure.theory_qualifier(name) |
|
257 if !known_sessions(qualifier) |
|
258 } yield "Bad import of theory " + quote(name.toString) + |
|
259 ": need to include sessions " + quote(qualifier) + " in ROOT" |
|
260 } |
|
261 |
|
262 val document_errors = |
|
263 info.document_theories.flatMap( |
|
264 { |
|
265 case (thy, pos) => |
|
266 val build_hierarchy = |
|
267 if (sessions_structure.build_graph.defined(session_name)) { |
|
268 sessions_structure.build_hierarchy(session_name) |
|
269 } |
|
270 else Nil |
|
271 |
|
272 def err(msg: String): Option[String] = |
|
273 Some(msg + " " + quote(thy) + Position.here(pos)) |
|
274 |
|
275 known_theories.get(thy).map(_.name) match { |
|
276 case None => err("Unknown document theory") |
|
277 case Some(name) => |
|
278 val qualifier = sessions_structure.theory_qualifier(name) |
|
279 if (proper_session_theories.contains(name)) { |
|
280 err("Redundant document theory from this session:") |
|
281 } |
|
282 else if (build_hierarchy.contains(qualifier)) None |
|
283 else if (dependencies.theories.contains(name)) None |
|
284 else err("Document theory from other session not imported properly:") |
|
285 } |
|
286 }) |
|
287 val document_theories = |
|
288 info.document_theories.map({ case (thy, _) => known_theories(thy).name }) |
|
289 |
|
290 val dir_errors = { |
|
291 val ok = info.dirs.map(_.canonical_file).toSet |
|
292 val bad = |
|
293 (for { |
|
294 name <- proper_session_theories.iterator |
|
295 path = name.master_dir_path |
|
296 if !ok(path.canonical_file) |
|
297 path1 = File.relative_path(info.dir.canonical, path).getOrElse(path) |
|
298 } yield (path1, name)).toList |
|
299 val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted |
|
300 |
|
301 val errs1 = |
|
302 for { (path1, name) <- bad } |
|
303 yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString) |
|
304 val errs2 = |
|
305 if (bad_dirs.isEmpty) Nil |
|
306 else List("Implicit use of session directories: " + commas(bad_dirs)) |
|
307 val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p |
|
308 val errs4 = |
|
309 (for { |
|
310 name <- proper_session_theories.iterator |
|
311 name1 <- resources.find_theory_node(name.theory) |
|
312 if name.node != name1.node |
|
313 } yield "Incoherent theory file import:\n " + name.path + " vs. \n " + name1.path) |
|
314 .toList |
|
315 |
|
316 errs1 ::: errs2 ::: errs3 ::: errs4 |
|
317 } |
|
318 |
|
319 val sources_errors = |
|
320 for (p <- session_files if !p.is_file) yield "No such file: " + p |
|
321 |
|
322 val path_errors = |
|
323 try { Path.check_case_insensitive(session_files ::: imported_files); Nil } |
|
324 catch { case ERROR(msg) => List(msg) } |
|
325 |
|
326 val bibtex_errors = |
|
327 try { info.bibtex_entries; Nil } |
|
328 catch { case ERROR(msg) => List(msg) } |
|
329 |
|
330 val base = |
|
331 Base( |
|
332 session_name = info.name, |
|
333 session_pos = info.pos, |
|
334 proper_session_theories = proper_session_theories, |
|
335 document_theories = document_theories, |
|
336 loaded_theories = dependencies.loaded_theories, |
|
337 used_theories = dependencies.theories_adjunct, |
|
338 load_commands = load_commands.toMap, |
|
339 known_theories = known_theories, |
|
340 known_loaded_files = known_loaded_files, |
|
341 overall_syntax = overall_syntax, |
|
342 imported_sources = check_sources(imported_files), |
|
343 session_sources = check_sources(session_files), |
|
344 session_graph_display = session_graph_display, |
|
345 errors = dependencies.errors ::: load_commands_errors ::: import_errors ::: |
|
346 document_errors ::: dir_errors ::: sources_errors ::: path_errors ::: |
|
347 bibtex_errors) |
|
348 |
|
349 session_bases + base.session_entry |
|
350 } |
|
351 catch { |
|
352 case ERROR(msg) => |
|
353 cat_error(msg, "The error(s) above occurred in session " + |
|
354 quote(info.name) + Position.here(info.pos)) |
|
355 } |
|
356 } |
|
357 |
|
358 Deps(sessions_structure, session_bases) |
|
359 } |
|
360 |
|
361 |
|
362 /* base info */ |
|
363 |
98 |
364 sealed case class Base_Info( |
99 sealed case class Base_Info( |
365 base: Base, |
100 base: Base, |
366 sessions_structure: Structure = Structure.empty, |
101 sessions_structure: Structure = Structure.empty, |
367 errors: List[String] = Nil, |
102 errors: List[String] = Nil, |
454 |
189 |
455 val deps1 = Sessions.deps(selected_sessions1, progress = progress) |
190 val deps1 = Sessions.deps(selected_sessions1, progress = progress) |
456 |
191 |
457 Base_Info(deps1(session1), sessions_structure = full_sessions1, |
192 Base_Info(deps1(session1), sessions_structure = full_sessions1, |
458 errors = deps1.errors, infos = infos1) |
193 errors = deps1.errors, infos = infos1) |
|
194 } |
|
195 |
|
196 |
|
197 /* source dependencies */ |
|
198 |
|
199 sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) { |
|
200 def base_info(session: String): Base_Info = |
|
201 Base_Info(base = apply(session), sessions_structure = sessions_structure, errors = errors) |
|
202 |
|
203 def is_empty: Boolean = session_bases.keysIterator.forall(_.isEmpty) |
|
204 def apply(name: String): Base = session_bases(name) |
|
205 def get(name: String): Option[Base] = session_bases.get(name) |
|
206 |
|
207 def imported_sources(name: String): List[SHA1.Digest] = |
|
208 session_bases(name).imported_sources.map(_._2) |
|
209 |
|
210 def session_sources(name: String): List[SHA1.Digest] = |
|
211 session_bases(name).session_sources.map(_._2) |
|
212 |
|
213 def errors: List[String] = |
|
214 (for { |
|
215 (name, base) <- session_bases.iterator |
|
216 if base.errors.nonEmpty |
|
217 } yield cat_lines(base.errors) + |
|
218 "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.session_pos) |
|
219 ).toList |
|
220 |
|
221 def check_errors: Deps = |
|
222 errors match { |
|
223 case Nil => this |
|
224 case errs => error(cat_lines(errs)) |
|
225 } |
|
226 |
|
227 override def toString: String = "Sessions.Deps(" + sessions_structure + ")" |
|
228 } |
|
229 |
|
230 def deps(sessions_structure: Structure, |
|
231 progress: Progress = new Progress, |
|
232 inlined_files: Boolean = false, |
|
233 verbose: Boolean = false, |
|
234 list_files: Boolean = false, |
|
235 check_keywords: Set[String] = Set.empty |
|
236 ): Deps = { |
|
237 var cache_sources = Map.empty[JFile, SHA1.Digest] |
|
238 def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = { |
|
239 for { |
|
240 path <- paths |
|
241 file = path.file |
|
242 if cache_sources.isDefinedAt(file) || file.isFile |
|
243 } |
|
244 yield { |
|
245 cache_sources.get(file) match { |
|
246 case Some(digest) => (path, digest) |
|
247 case None => |
|
248 val digest = SHA1.digest(file) |
|
249 cache_sources = cache_sources + (file -> digest) |
|
250 (path, digest) |
|
251 } |
|
252 } |
|
253 } |
|
254 |
|
255 val session_bases = |
|
256 sessions_structure.imports_topological_order.foldLeft( |
|
257 Map(Sessions.bootstrap_base.session_entry)) { |
|
258 case (session_bases, session_name) => |
|
259 progress.expose_interrupt() |
|
260 |
|
261 val info = sessions_structure(session_name) |
|
262 try { |
|
263 val deps_base = info.deps_base(session_bases) |
|
264 val resources = new Resources(sessions_structure, deps_base) |
|
265 |
|
266 if (verbose || list_files) { |
|
267 val groups = |
|
268 if (info.groups.isEmpty) "" |
|
269 else info.groups.mkString(" (", " ", ")") |
|
270 progress.echo("Session " + info.chapter + "/" + session_name + groups) |
|
271 } |
|
272 |
|
273 val dependencies = resources.session_dependencies(info) |
|
274 |
|
275 val overall_syntax = dependencies.overall_syntax |
|
276 |
|
277 val proper_session_theories = |
|
278 dependencies.theories.filter(name => |
|
279 sessions_structure.theory_qualifier(name) == session_name) |
|
280 |
|
281 val theory_files = dependencies.theories.map(_.path) |
|
282 |
|
283 val (load_commands, load_commands_errors) = |
|
284 try { if (inlined_files) (dependencies.load_commands, Nil) else (Nil, Nil) } |
|
285 catch { case ERROR(msg) => (Nil, List(msg)) } |
|
286 |
|
287 val loaded_files = |
|
288 load_commands.map({ case (name, spans) => dependencies.loaded_files(name, spans) }) |
|
289 |
|
290 val session_files = |
|
291 (theory_files ::: loaded_files.flatMap(_._2) ::: |
|
292 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) |
|
293 |
|
294 val imported_files = if (inlined_files) dependencies.imported_files else Nil |
|
295 |
|
296 if (list_files) { |
|
297 progress.echo(cat_lines(session_files.map(_.implode).sorted.map(" " + _))) |
|
298 } |
|
299 |
|
300 if (check_keywords.nonEmpty) { |
|
301 Check_Keywords.check_keywords( |
|
302 progress, overall_syntax.keywords, check_keywords, theory_files) |
|
303 } |
|
304 |
|
305 val session_graph_display: Graph_Display.Graph = { |
|
306 def session_node(name: String): Graph_Display.Node = |
|
307 Graph_Display.Node("[" + name + "]", "session." + name) |
|
308 |
|
309 def node(name: Document.Node.Name): Graph_Display.Node = { |
|
310 val qualifier = sessions_structure.theory_qualifier(name) |
|
311 if (qualifier == info.name) { |
|
312 Graph_Display.Node(name.theory_base_name, "theory." + name.theory) |
|
313 } |
|
314 else session_node(qualifier) |
|
315 } |
|
316 |
|
317 val required_sessions = |
|
318 dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory)) |
|
319 .map(theory => sessions_structure.theory_qualifier(theory)) |
|
320 .filter(name => name != info.name && sessions_structure.defined(name)) |
|
321 |
|
322 val required_subgraph = |
|
323 sessions_structure.imports_graph |
|
324 .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet) |
|
325 .transitive_closure |
|
326 .restrict(required_sessions.toSet) |
|
327 .transitive_reduction_acyclic |
|
328 |
|
329 val graph0 = |
|
330 required_subgraph.topological_order.foldLeft(Graph_Display.empty_graph) { |
|
331 case (g, session) => |
|
332 val a = session_node(session) |
|
333 val bs = required_subgraph.imm_preds(session).toList.map(session_node) |
|
334 bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a)) |
|
335 } |
|
336 |
|
337 dependencies.entries.foldLeft(graph0) { |
|
338 case (g, entry) => |
|
339 val a = node(entry.name) |
|
340 val bs = entry.header.imports.map(node).filterNot(_ == a) |
|
341 bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a)) |
|
342 } |
|
343 } |
|
344 |
|
345 val known_theories = |
|
346 dependencies.entries.iterator.map(entry => entry.name.theory -> entry). |
|
347 foldLeft(deps_base.known_theories)(_ + _) |
|
348 |
|
349 val known_loaded_files = deps_base.known_loaded_files ++ loaded_files |
|
350 |
|
351 val import_errors = { |
|
352 val known_sessions = |
|
353 sessions_structure.imports_requirements(List(session_name)).toSet |
|
354 for { |
|
355 name <- dependencies.theories |
|
356 qualifier = sessions_structure.theory_qualifier(name) |
|
357 if !known_sessions(qualifier) |
|
358 } yield "Bad import of theory " + quote(name.toString) + |
|
359 ": need to include sessions " + quote(qualifier) + " in ROOT" |
|
360 } |
|
361 |
|
362 val document_errors = |
|
363 info.document_theories.flatMap( |
|
364 { |
|
365 case (thy, pos) => |
|
366 val build_hierarchy = |
|
367 if (sessions_structure.build_graph.defined(session_name)) { |
|
368 sessions_structure.build_hierarchy(session_name) |
|
369 } |
|
370 else Nil |
|
371 |
|
372 def err(msg: String): Option[String] = |
|
373 Some(msg + " " + quote(thy) + Position.here(pos)) |
|
374 |
|
375 known_theories.get(thy).map(_.name) match { |
|
376 case None => err("Unknown document theory") |
|
377 case Some(name) => |
|
378 val qualifier = sessions_structure.theory_qualifier(name) |
|
379 if (proper_session_theories.contains(name)) { |
|
380 err("Redundant document theory from this session:") |
|
381 } |
|
382 else if (build_hierarchy.contains(qualifier)) None |
|
383 else if (dependencies.theories.contains(name)) None |
|
384 else err("Document theory from other session not imported properly:") |
|
385 } |
|
386 }) |
|
387 val document_theories = |
|
388 info.document_theories.map({ case (thy, _) => known_theories(thy).name }) |
|
389 |
|
390 val dir_errors = { |
|
391 val ok = info.dirs.map(_.canonical_file).toSet |
|
392 val bad = |
|
393 (for { |
|
394 name <- proper_session_theories.iterator |
|
395 path = name.master_dir_path |
|
396 if !ok(path.canonical_file) |
|
397 path1 = File.relative_path(info.dir.canonical, path).getOrElse(path) |
|
398 } yield (path1, name)).toList |
|
399 val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted |
|
400 |
|
401 val errs1 = |
|
402 for { (path1, name) <- bad } |
|
403 yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString) |
|
404 val errs2 = |
|
405 if (bad_dirs.isEmpty) Nil |
|
406 else List("Implicit use of session directories: " + commas(bad_dirs)) |
|
407 val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p |
|
408 val errs4 = |
|
409 (for { |
|
410 name <- proper_session_theories.iterator |
|
411 name1 <- resources.find_theory_node(name.theory) |
|
412 if name.node != name1.node |
|
413 } yield "Incoherent theory file import:\n " + name.path + " vs. \n " + name1.path) |
|
414 .toList |
|
415 |
|
416 errs1 ::: errs2 ::: errs3 ::: errs4 |
|
417 } |
|
418 |
|
419 val sources_errors = |
|
420 for (p <- session_files if !p.is_file) yield "No such file: " + p |
|
421 |
|
422 val path_errors = |
|
423 try { Path.check_case_insensitive(session_files ::: imported_files); Nil } |
|
424 catch { case ERROR(msg) => List(msg) } |
|
425 |
|
426 val bibtex_errors = |
|
427 try { info.bibtex_entries; Nil } |
|
428 catch { case ERROR(msg) => List(msg) } |
|
429 |
|
430 val base = |
|
431 Base( |
|
432 session_name = info.name, |
|
433 session_pos = info.pos, |
|
434 proper_session_theories = proper_session_theories, |
|
435 document_theories = document_theories, |
|
436 loaded_theories = dependencies.loaded_theories, |
|
437 used_theories = dependencies.theories_adjunct, |
|
438 load_commands = load_commands.toMap, |
|
439 known_theories = known_theories, |
|
440 known_loaded_files = known_loaded_files, |
|
441 overall_syntax = overall_syntax, |
|
442 imported_sources = check_sources(imported_files), |
|
443 session_sources = check_sources(session_files), |
|
444 session_graph_display = session_graph_display, |
|
445 errors = dependencies.errors ::: load_commands_errors ::: import_errors ::: |
|
446 document_errors ::: dir_errors ::: sources_errors ::: path_errors ::: |
|
447 bibtex_errors) |
|
448 |
|
449 session_bases + base.session_entry |
|
450 } |
|
451 catch { |
|
452 case ERROR(msg) => |
|
453 cat_error(msg, "The error(s) above occurred in session " + |
|
454 quote(info.name) + Position.here(info.pos)) |
|
455 } |
|
456 } |
|
457 |
|
458 Deps(sessions_structure, session_bases) |
459 } |
459 } |
460 |
460 |
461 |
461 |
462 /* cumulative session info */ |
462 /* cumulative session info */ |
463 |
463 |