58 known_loaded_files: Map[String, List[Path]] = Map.empty, |
58 known_loaded_files: Map[String, List[Path]] = Map.empty, |
59 overall_syntax: Outer_Syntax = Outer_Syntax.empty, |
59 overall_syntax: Outer_Syntax = Outer_Syntax.empty, |
60 imported_sources: List[(Path, SHA1.Digest)] = Nil, |
60 imported_sources: List[(Path, SHA1.Digest)] = Nil, |
61 sources: List[(Path, SHA1.Digest)] = Nil, |
61 sources: List[(Path, SHA1.Digest)] = Nil, |
62 session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph, |
62 session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph, |
63 errors: List[String] = Nil, |
63 errors: List[String] = Nil) |
64 imports: Option[Base] = None) |
|
65 { |
64 { |
66 override def toString: String = |
65 override def toString: String = |
67 "Sessions.Base(loaded_theories = " + loaded_theories.size + |
66 "Sessions.Base(loaded_theories = " + loaded_theories.size + |
68 ", used_theories = " + used_theories.length + ")" |
67 ", used_theories = " + used_theories.length + ")" |
69 |
68 |
79 def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] = |
78 def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] = |
80 loaded_theory_syntax(name.theory) |
79 loaded_theory_syntax(name.theory) |
81 |
80 |
82 def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax = |
81 def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax = |
83 nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax |
82 nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax |
84 |
|
85 def get_imports: Base = |
|
86 imports getOrElse Base.bootstrap(session_directories, global_theories) |
|
87 } |
83 } |
88 |
84 |
89 sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) |
85 sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) |
90 { |
86 { |
91 override def toString: String = "Sessions.Deps(" + sessions_structure + ")" |
87 override def toString: String = "Sessions.Deps(" + sessions_structure + ")" |
306 overall_syntax = overall_syntax, |
302 overall_syntax = overall_syntax, |
307 imported_sources = check_sources(imported_files), |
303 imported_sources = check_sources(imported_files), |
308 sources = check_sources(session_files), |
304 sources = check_sources(session_files), |
309 session_graph_display = session_graph_display, |
305 session_graph_display = session_graph_display, |
310 errors = dependencies.errors ::: dir_errors ::: sources_errors ::: |
306 errors = dependencies.errors ::: dir_errors ::: sources_errors ::: |
311 path_errors ::: bibtex_errors, |
307 path_errors ::: bibtex_errors) |
312 imports = Some(imports_base)) |
|
313 |
308 |
314 session_bases + (info.name -> base) |
309 session_bases + (info.name -> base) |
315 } |
310 } |
316 catch { |
311 catch { |
317 case ERROR(msg) => |
312 case ERROR(msg) => |