54 } |
54 } |
55 |
55 |
56 |
56 |
57 /* theory files */ |
57 /* theory files */ |
58 |
58 |
59 private def import_name(dir: String, s: String): Document.Node.Name = |
|
60 { |
|
61 val theory = Thy_Header.base_name(s) |
|
62 if (loaded_theories(theory)) Document.Node.Name(theory, "", theory) |
|
63 else { |
|
64 val path = Path.explode(s) |
|
65 val node = append(dir, Thy_Load.thy_path(path)) |
|
66 val dir1 = append(dir, path.dir) |
|
67 Document.Node.Name(node, dir1, theory) |
|
68 } |
|
69 } |
|
70 |
|
71 private def find_file(tokens: List[Token]): Option[String] = |
59 private def find_file(tokens: List[Token]): Option[String] = |
72 { |
60 { |
73 def clean(toks: List[Token]): List[Token] = |
61 def clean(toks: List[Token]): List[Token] = |
74 toks match { |
62 toks match { |
75 case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts) |
63 case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts) |
101 } |
89 } |
102 case _ => Nil |
90 case _ => Nil |
103 }).flatten.toList |
91 }).flatten.toList |
104 } |
92 } |
105 |
93 |
|
94 def import_name(master: Document.Node.Name, s: String): Document.Node.Name = |
|
95 { |
|
96 val theory = Thy_Header.base_name(s) |
|
97 if (loaded_theories(theory)) Document.Node.Name(theory, "", theory) |
|
98 else { |
|
99 val path = Path.explode(s) |
|
100 val node = append(master.dir, Thy_Load.thy_path(path)) |
|
101 val dir = append(master.dir, path.dir) |
|
102 Document.Node.Name(node, dir, theory) |
|
103 } |
|
104 } |
|
105 |
106 def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = |
106 def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = |
107 { |
107 { |
108 try { |
108 try { |
109 val header = Thy_Header.read(text) |
109 val header = Thy_Header.read(text) |
110 |
110 |
111 val name1 = header.name |
111 val name1 = header.name |
112 if (name.theory != name1) |
112 if (name.theory != name1) |
113 error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
113 error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
114 " for theory " + quote(name1)) |
114 " for theory " + quote(name1)) |
115 |
115 |
116 val imports = header.imports.map(import_name(name.dir, _)) |
116 val imports = header.imports.map(import_name(name, _)) |
117 Document.Node.Header(imports, header.keywords, Nil) |
117 Document.Node.Header(imports, header.keywords, Nil) |
118 } |
118 } |
119 catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
119 catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
120 } |
120 } |
121 |
121 |