equal
deleted
inserted
replaced
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 body_files_test(syntax: Outer_Syntax, text: String): Boolean = |
54 syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) |
54 syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) |
55 |
55 |
56 def body_files(syntax: Outer_Syntax, text: String): List[String] = |
56 def body_files(syntax: Outer_Syntax, text: String): List[String] = |
57 { |
57 { |
58 val spans = Thy_Syntax.parse_spans(syntax.scan(text)) |
58 val spans = Thy_Syntax.parse_spans(syntax.scan(text)) |
59 spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList |
59 spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList |