466 |
466 |
467 local |
467 local |
468 |
468 |
469 val spaces_quote = space_implode " " o map quote; |
469 val spaces_quote = space_implode " " o map quote; |
470 |
470 |
471 (* FIXME: investigate why dependencies at the moment include themselves! *) |
|
472 fun thm_deps_message (thms, deps) = |
471 fun thm_deps_message (thms, deps) = |
473 if pgip() then |
472 if pgip() then |
474 issue_pgips |
473 issue_pgips |
475 [XML.element |
474 [XML.element |
476 "metainforesponse" (* FIXME: get thy name from info here? *) |
475 "metainforesponse" (* FIXME: get thy name from info here? *) |
477 [("infotype", "isabelle_theorem_dependencies")] |
476 [("infotype", "isabelle_theorem_dependencies")] |
478 [XML.element "value" [("name", "thms")] [XML.text thms], |
477 [XML.element "value" [("name", "thms")] [XML.text thms], |
479 XML.element "value" [("name", "deps")] [XML.text deps]]] |
478 XML.element "value" [("name", "deps")] [XML.text deps]]] |
480 else emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps); |
479 else emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps); |
481 |
480 |
|
481 (* FIXME: check this uses non-transitive closure function here *) |
482 fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () => |
482 fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () => |
483 let |
483 let |
484 val names = filter_out (equal "") (map Thm.name_of_thm ths); |
484 val names = filter_out (equal "") (map Thm.name_of_thm ths); |
485 val deps = filter_out (equal "") |
485 val deps = filter_out (equal "") |
486 (Symtab.keys (fold Proofterm.thms_of_proof |
486 (Symtab.keys (fold Proofterm.thms_of_proof |
1195 val thyname_attro = xmlattro "thyname" |
1195 val thyname_attro = xmlattro "thyname" |
1196 val thyname_attr = xmlattr "thyname" |
1196 val thyname_attr = xmlattr "thyname" |
1197 val objtype_attro = xmlattro "objtype" |
1197 val objtype_attro = xmlattro "objtype" |
1198 val objtype_attr = xmlattr "objtype" |
1198 val objtype_attr = xmlattr "objtype" |
1199 val name_attr = xmlattr "name" |
1199 val name_attr = xmlattr "name" |
1200 val dirname_attr = xmlattr "dir" |
|
1201 fun comment x = "(* " ^ x ^ " *)" |
|
1202 |
1200 |
1203 fun localfile_of_url url = (* only handle file:/// or file://localhost/ *) |
1201 fun localfile_of_url url = (* only handle file:/// or file://localhost/ *) |
1204 case Url.unpack url of |
1202 case Url.unpack url of |
1205 (Url.File path) => File.platform_path path |
1203 (Url.File path) => File.platform_path path |
1206 | _ => error ("Cannot access non-local URL " ^ url) |
1204 | _ => error ("Cannot access non-local URL " ^ url) |
1213 val currently_open_file = ref (NONE : string option) |
1211 val currently_open_file = ref (NONE : string option) |
1214 |
1212 |
1215 (* Path management: we allow theory files to have dependencies |
1213 (* Path management: we allow theory files to have dependencies |
1216 in their own directory, but when we change directory for a new |
1214 in their own directory, but when we change directory for a new |
1217 file we remove the path. Leaving it there can cause confusion |
1215 file we remove the path. Leaving it there can cause confusion |
1218 with difference in batch mode.a NB: PGIP does not assume |
1216 with difference in batch mode. NB: PGIP does not currently assume |
1219 that the prover has a load path. *) |
1217 that the prover has a load path. *) |
1220 local |
1218 local |
1221 val current_working_dir = ref (NONE : string option) |
1219 val current_working_dir = ref (NONE : string option) |
1222 in |
1220 in |
1223 fun changecwd dir = |
1221 fun changecwd dir = |