78 } |
78 } |
79 val clean_tokens = clean(tokens.filter(_.is_proper)) |
79 val clean_tokens = clean(tokens.filter(_.is_proper)) |
80 clean_tokens.reverse.find(_.is_name).map(_.content) |
80 clean_tokens.reverse.find(_.is_name).map(_.content) |
81 } |
81 } |
82 |
82 |
83 def find_files(syntax: Outer_Syntax, text: String): List[String] = |
83 def theory_body_files(syntax: Outer_Syntax, text: String): List[String] = |
84 { |
84 { |
85 val thy_load_commands = syntax.thy_load_commands |
85 val thy_load_commands = syntax.thy_load_commands |
86 if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) { |
86 if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) { |
87 val spans = Thy_Syntax.parse_spans(syntax.scan(text)) |
87 val spans = Thy_Syntax.parse_spans(syntax.scan(text)) |
88 spans.iterator.map({ |
88 spans.iterator.map({ |
103 else Nil |
103 else Nil |
104 } |
104 } |
105 |
105 |
106 def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = |
106 def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = |
107 { |
107 { |
108 val header = Thy_Header.read(text) |
108 try { |
|
109 val header = Thy_Header.read(text) |
109 |
110 |
110 val name1 = header.name |
111 val name1 = header.name |
111 if (name.theory != name1) |
112 if (name.theory != name1) |
112 error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
113 error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
113 " for theory " + quote(name1)) |
114 " for theory " + quote(name1)) |
114 |
115 |
115 val imports = header.imports.map(import_name(name.dir, _)) |
116 val imports = header.imports.map(import_name(name.dir, _)) |
116 val uses = header.uses |
117 val uses = header.uses |
117 Document.Node.Header(imports, header.keywords, uses) |
118 Document.Node.Header(imports, header.keywords, uses) |
|
119 } |
|
120 catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) } |
118 } |
121 } |
119 |
122 |
120 def check_thy(name: Document.Node.Name): Document.Node.Header = |
123 def check_thy(name: Document.Node.Name): Document.Node.Header = |
121 with_thy_text(name, check_thy_text(name, _)) |
124 with_thy_text(name, check_thy_text(name, _)) |
122 |
|
123 def check_thy_files(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header = |
|
124 with_thy_text(name, text => |
|
125 { |
|
126 val string = text.toString |
|
127 val header = check_thy_text(name, string) |
|
128 val more_uses = find_files(syntax.add_keywords(header.keywords), string) |
|
129 header.copy(uses = header.uses ::: more_uses.map((_, false))) |
|
130 }) |
|
131 } |
125 } |
132 |
126 |