44 def append(dir: String, source_path: Path): String = |
45 def append(dir: String, source_path: Path): String = |
45 (Path.explode(dir) + source_path).expand.implode |
46 (Path.explode(dir) + source_path).expand.implode |
46 |
47 |
47 def append(node_name: Document.Node.Name, source_path: Path): String = |
48 def append(node_name: Document.Node.Name, source_path: Path): String = |
48 append(node_name.master_dir, source_path) |
49 append(node_name.master_dir, source_path) |
|
50 |
|
51 def make_theory_node(dir: String, file: Path, theory: String): Document.Node.Name = |
|
52 { |
|
53 val node = append(dir, file) |
|
54 val master_dir = append(dir, file.dir) |
|
55 Document.Node.Name(node, master_dir, theory) |
|
56 } |
49 |
57 |
50 |
58 |
51 /* source files of Isabelle/ML bootstrap */ |
59 /* source files of Isabelle/ML bootstrap */ |
52 |
60 |
53 def source_file(raw_name: String): Option[String] = |
61 def source_file(raw_name: String): Option[String] = |
107 def theory_name(qualifier: String, theory: String): String = |
115 def theory_name(qualifier: String, theory: String): String = |
108 if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory)) |
116 if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory)) |
109 theory |
117 theory |
110 else Long_Name.qualify(qualifier, theory) |
118 else Long_Name.qualify(qualifier, theory) |
111 |
119 |
|
120 def find_theory_node(theory: String): Option[Document.Node.Name] = |
|
121 session_base.known.theories.get(theory).map(_.name) orElse { |
|
122 val thy_file = thy_path(Path.basic(Long_Name.base_name(theory))) |
|
123 val session = session_base.theory_qualifier(theory) |
|
124 val dirs = |
|
125 sessions_structure.get(session) match { |
|
126 case Some(info) => info.dirs |
|
127 case None => Nil |
|
128 } |
|
129 dirs.collectFirst({ |
|
130 case dir if (dir + thy_file).is_file => make_theory_node("", dir + thy_file, theory) }) |
|
131 } |
|
132 |
112 def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = |
133 def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = |
113 { |
134 { |
114 val theory = theory_name(qualifier, Thy_Header.import_name(s)) |
135 val theory = theory_name(qualifier, Thy_Header.import_name(s)) |
115 if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory) |
136 if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory) |
116 else { |
137 else { |
117 session_base.known_theory(theory) match { |
138 find_theory_node(theory) match { |
118 case Some(node_name) => node_name |
139 case Some(node_name) => node_name |
119 case None => |
140 case None => |
120 if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)) |
141 if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)) |
121 Document.Node.Name.loaded_theory(theory) |
142 Document.Node.Name.loaded_theory(theory) |
122 else { |
143 else make_theory_node(dir, thy_path(Path.explode(s)), theory) |
123 val path = Path.explode(s) |
|
124 val node = append(dir, thy_path(path)) |
|
125 val master_dir = append(dir, path.dir) |
|
126 Document.Node.Name(node, master_dir, theory) |
|
127 } |
|
128 } |
144 } |
129 } |
145 } |
130 } |
146 } |
131 |
147 |
132 def import_name(name: Document.Node.Name, s: String): Document.Node.Name = |
148 def import_name(name: Document.Node.Name, s: String): Document.Node.Name = |