equal
deleted
inserted
replaced
105 |
105 |
106 ML \<open> |
106 ML \<open> |
107 local |
107 local |
108 val _ = |
108 val _ = |
109 Outer_Syntax.command \<^command_keyword>\<open>external_file\<close> "formal dependency on external file" |
109 Outer_Syntax.command \<^command_keyword>\<open>external_file\<close> "formal dependency on external file" |
110 (Parse.position Parse.path >> (fn path => Toplevel.keep (fn st => |
110 (Resources.provide_parse_files "external_file" >> (fn files => Toplevel.theory (#2 o files))); |
111 let |
|
112 val ctxt = Toplevel.context_of st; |
|
113 val thy = Toplevel.theory_of st; |
|
114 val _ = Resources.check_path ctxt (Resources.master_directory thy) path; |
|
115 in () end))); |
|
116 |
111 |
117 val _ = |
112 val _ = |
118 Outer_Syntax.command \<^command_keyword>\<open>bibtex_file\<close> "check bibtex database file in Prover IDE" |
113 Outer_Syntax.command \<^command_keyword>\<open>bibtex_file\<close> "check bibtex database file in Prover IDE" |
119 (Scan.ahead Parse.not_eof -- Parse.position Parse.path >> (fn (tok, path) => |
114 (Resources.provide_parse_files "bibtex_file" >> (fn files => |
120 Toplevel.keep (fn st => |
115 Toplevel.theory (fn thy => |
121 let |
116 let |
122 val ctxt = Toplevel.context_of st; |
117 val ([{lines, pos, ...}], thy') = files thy; |
123 val thy = Toplevel.theory_of st; |
118 val _ = Bibtex.check_database_output pos (cat_lines lines); |
124 val _ = Resources.check_path ctxt (Resources.master_directory thy) path; |
119 in thy' end))); |
125 val _ = |
|
126 (case Token.get_files tok of |
|
127 [Exn.Res {lines, pos, ...}] => Bibtex.check_database_output pos (cat_lines lines) |
|
128 | _ => ()); |
|
129 in () end))); |
|
130 in end\<close> |
120 in end\<close> |
131 |
121 |
132 |
122 |
133 subsection \<open>Embedded ML text\<close> |
123 subsection \<open>Embedded ML text\<close> |
134 |
124 |