equal
deleted
inserted
replaced
48 } |
48 } |
49 |
49 |
50 |
50 |
51 /* theory files */ |
51 /* theory files */ |
52 |
52 |
53 def body_files_test(syntax: Outer_Syntax, text: String): Boolean = |
53 def loaded_files(syntax: Outer_Syntax, text: String): List[String] = |
54 syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) |
|
55 |
|
56 def body_files(syntax: Outer_Syntax, text: String): List[String] = |
|
57 { |
54 { |
58 val spans = Thy_Syntax.parse_spans(syntax.scan(text)) |
55 if (syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) { |
59 spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList |
56 val spans = Thy_Syntax.parse_spans(syntax.scan(text)) |
|
57 spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList |
|
58 } |
|
59 else Nil |
60 } |
60 } |
61 |
61 |
62 def import_name(master: Document.Node.Name, s: String): Document.Node.Name = |
62 def import_name(master: Document.Node.Name, s: String): Document.Node.Name = |
63 { |
63 { |
64 val theory = Thy_Header.base_name(s) |
64 val theory = Thy_Header.base_name(s) |