31 name: Document.Node.Name, |
31 name: Document.Node.Name, |
32 header: Document.Node.Header) |
32 header: Document.Node.Header) |
33 { |
33 { |
34 def load_files(syntax: Outer_Syntax): List[String] = |
34 def load_files(syntax: Outer_Syntax): List[String] = |
35 { |
35 { |
36 val string = thy_load.with_thy_text(name, _.toString) |
36 val string = resources.with_thy_text(name, _.toString) |
37 if (thy_load.body_files_test(syntax, string)) |
37 if (resources.body_files_test(syntax, string)) |
38 thy_load.body_files(syntax, string) |
38 resources.body_files(syntax, string) |
39 else Nil |
39 else Nil |
40 } |
40 } |
41 } |
41 } |
42 |
42 |
43 object Dependencies |
43 object Dependencies |
69 { |
69 { |
70 val header_errors = deps.flatMap(dep => dep.header.errors) |
70 val header_errors = deps.flatMap(dep => dep.header.errors) |
71 val import_errors = |
71 val import_errors = |
72 (for { |
72 (for { |
73 (theory, names) <- seen_names.iterator_list |
73 (theory, names) <- seen_names.iterator_list |
74 if !thy_load.loaded_theories(theory) |
74 if !resources.loaded_theories(theory) |
75 if names.length > 1 |
75 if names.length > 1 |
76 } yield |
76 } yield |
77 "Incoherent imports for theory " + quote(theory) + ":\n" + |
77 "Incoherent imports for theory " + quote(theory) + ":\n" + |
78 cat_lines(names.flatMap(name => |
78 cat_lines(names.flatMap(name => |
79 seen_positions.get_list(theory).map(pos => |
79 seen_positions.get_list(theory).map(pos => |
80 " " + quote(name.node) + Position.here(pos)))) |
80 " " + quote(name.node) + Position.here(pos)))) |
81 ).toList |
81 ).toList |
82 header_errors ::: import_errors |
82 header_errors ::: import_errors |
83 } |
83 } |
84 |
84 |
85 lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords) |
85 lazy val syntax: Outer_Syntax = resources.base_syntax.add_keywords(keywords) |
86 |
86 |
87 def loaded_theories: Set[String] = |
87 def loaded_theories: Set[String] = |
88 (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory } |
88 (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory } |
89 |
89 |
90 def load_files: List[Path] = |
90 def load_files: List[Path] = |
91 { |
91 { |
92 val dep_files = |
92 val dep_files = |
93 rev_deps.par.map(dep => |
93 rev_deps.par.map(dep => |
113 def message: String = |
113 def message: String = |
114 "The error(s) above occurred for theory " + quote(theory) + |
114 "The error(s) above occurred for theory " + quote(theory) + |
115 required_by(initiators) + Position.here(require_pos) |
115 required_by(initiators) + Position.here(require_pos) |
116 |
116 |
117 val required1 = required + thy |
117 val required1 = required + thy |
118 if (required.seen_names.isDefinedAt(theory) || thy_load.loaded_theories(theory)) |
118 if (required.seen_names.isDefinedAt(theory) || resources.loaded_theories(theory)) |
119 required1 |
119 required1 |
120 else { |
120 else { |
121 try { |
121 try { |
122 if (initiators.contains(name)) error(cycle_msg(initiators)) |
122 if (initiators.contains(name)) error(cycle_msg(initiators)) |
123 val header = |
123 val header = |
124 try { thy_load.check_thy(name).cat_errors(message) } |
124 try { resources.check_thy(name).cat_errors(message) } |
125 catch { case ERROR(msg) => cat_error(msg, message) } |
125 catch { case ERROR(msg) => cat_error(msg, message) } |
126 val imports = header.imports.map((_, Position.File(name.node))) |
126 val imports = header.imports.map((_, Position.File(name.node))) |
127 Dep(name, header) :: require_thys(name :: initiators, required1, imports) |
127 Dep(name, header) :: require_thys(name :: initiators, required1, imports) |
128 } |
128 } |
129 catch { |
129 catch { |