65 val spans = syntax.parse_spans(text) |
65 val spans = syntax.parse_spans(text) |
66 spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList |
66 spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList |
67 } |
67 } |
68 else Nil |
68 else Nil |
69 |
69 |
70 def init_name(global: Boolean, raw_path: Path): Document.Node.Name = |
70 def qualify(name: String): String = |
|
71 if (Long_Name.is_qualified(name)) error("Bad qualified theory name " + quote(name)) |
|
72 else if (session_base.global_theories.contains(name)) name |
|
73 else Long_Name.qualify(session_name, name) |
|
74 |
|
75 def init_name(raw_path: Path): Document.Node.Name = |
71 { |
76 { |
72 val path = raw_path.expand |
77 val path = raw_path.expand |
73 val node = path.implode |
78 val node = path.implode |
74 val qualifier = if (global) "" else session_name |
79 val theory = qualify(Thy_Header.thy_name(node).getOrElse("")) |
75 val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse("")) |
|
76 val master_dir = if (theory == "") "" else path.dir.implode |
80 val master_dir = if (theory == "") "" else path.dir.implode |
77 Document.Node.Name(node, master_dir, theory) |
81 Document.Node.Name(node, master_dir, theory) |
78 } |
82 } |
79 |
83 |
80 def import_name(master: Document.Node.Name, s: String): Document.Node.Name = |
84 def import_name(master: Document.Node.Name, s: String): Document.Node.Name = |