101 fun check_file dir file = File.check_file (File.full_path dir file); |
101 fun check_file dir file = File.check_file (File.full_path dir file); |
102 |
102 |
103 fun check_thy dir thy_name = |
103 fun check_thy dir thy_name = |
104 let |
104 let |
105 val thy_base_name = Long_Name.base_name thy_name; |
105 val thy_base_name = Long_Name.base_name thy_name; |
106 val thy_path = thy_path (Path.basic thy_base_name); |
|
107 val master_file = |
106 val master_file = |
108 (case known_theory thy_name of |
107 (case known_theory thy_name of |
109 NONE => check_file dir thy_path |
108 SOME known_path => check_file Path.current known_path |
110 | SOME known_path => check_file Path.current known_path); |
109 | NONE => check_file dir (thy_path (Path.basic thy_base_name))); |
111 val text = File.read master_file; |
110 val text = File.read master_file; |
112 |
111 |
113 val {name = (name, pos), imports, keywords} = |
112 val {name = (name, pos), imports, keywords} = |
114 Thy_Header.read (Path.position master_file) text; |
113 Thy_Header.read (Path.position master_file) text; |
115 val _ = |
114 val _ = |
116 thy_base_name <> name andalso |
115 thy_base_name <> name andalso |
117 error ("Bad theory name " ^ quote name ^ |
116 error ("Bad theory name " ^ quote name ^ |
118 " for file " ^ Path.print thy_path ^ Position.here pos); |
117 " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); |
119 in |
118 in |
120 {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, |
119 {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, |
121 imports = imports, keywords = keywords} |
120 imports = imports, keywords = keywords} |
122 end; |
121 end; |
123 |
122 |