equal
deleted
inserted
replaced
22 |
22 |
23 /* document node names */ |
23 /* document node names */ |
24 |
24 |
25 def node_name(qualifier: String, raw_path: Path): Document.Node.Name = |
25 def node_name(qualifier: String, raw_path: Path): Document.Node.Name = |
26 { |
26 { |
27 val no_qualifier = "" // FIXME |
|
28 val path = raw_path.expand |
27 val path = raw_path.expand |
29 val node = path.implode |
28 val node = path.implode |
30 val theory = Long_Name.qualify(no_qualifier, Thy_Header.thy_name(node).getOrElse("")) |
29 val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse("")) |
31 val master_dir = if (theory == "") "" else path.dir.implode |
30 val master_dir = if (theory == "") "" else path.dir.implode |
32 Document.Node.Name(node, master_dir, theory) |
31 Document.Node.Name(node, master_dir, theory) |
33 } |
32 } |
34 |
33 |
35 |
34 |
77 } |
76 } |
78 else Nil |
77 else Nil |
79 |
78 |
80 def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name = |
79 def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name = |
81 { |
80 { |
82 val no_qualifier = "" // FIXME |
|
83 val thy1 = Thy_Header.base_name(s) |
81 val thy1 = Thy_Header.base_name(s) |
84 val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1) |
82 val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1) |
85 (base.known_theories.get(thy1) orElse |
83 (base.known_theories.get(thy1) orElse |
86 base.known_theories.get(thy2) orElse |
84 base.known_theories.get(thy2) orElse |
87 base.known_theories.get(Long_Name.base_name(thy1))) match { |
85 base.known_theories.get(Long_Name.base_name(thy1))) match { |
88 case Some(name) if base.loaded_theory(name) => Document.Node.Name.theory(name.theory) |
86 case Some(name) if base.loaded_theory(name) => Document.Node.Name.theory(name.theory) |
89 case Some(name) => name |
87 case Some(name) => name |
92 val theory = path.base.implode |
90 val theory = path.base.implode |
93 if (Long_Name.is_qualified(theory)) Document.Node.Name.theory(theory) |
91 if (Long_Name.is_qualified(theory)) Document.Node.Name.theory(theory) |
94 else { |
92 else { |
95 val node = append(master.master_dir, thy_path(path)) |
93 val node = append(master.master_dir, thy_path(path)) |
96 val master_dir = append(master.master_dir, path.dir) |
94 val master_dir = append(master.master_dir, path.dir) |
97 Document.Node.Name(node, master_dir, Long_Name.qualify(no_qualifier, theory)) |
95 Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory)) |
98 } |
96 } |
99 } |
97 } |
100 } |
98 } |
101 |
99 |
102 def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
100 def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |