equal
deleted
inserted
replaced
59 |
59 |
60 def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] = |
60 def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] = |
61 { |
61 { |
62 val raw_text = with_thy_reader(name, reader => reader.source.toString) |
62 val raw_text = with_thy_reader(name, reader => reader.source.toString) |
63 () => { |
63 () => { |
64 val text = Symbol.decode(raw_text) |
64 if (syntax.load_commands_in(raw_text)) { |
65 if (syntax.load_commands_in(text)) { |
65 val text = Symbol.decode(raw_text) |
66 val spans = syntax.parse_spans(text) |
66 val spans = syntax.parse_spans(text) |
67 val dir = Path.explode(name.master_dir) |
67 val dir = Path.explode(name.master_dir) |
68 spans.iterator.map(Command.span_files(syntax, _)._1).flatten. |
68 spans.iterator.map(Command.span_files(syntax, _)._1).flatten. |
69 map(a => (dir + Path.explode(a)).expand).toList |
69 map(a => (dir + Path.explode(a)).expand).toList |
70 } |
70 } |