# HG changeset patch # User wenzelm # Date 1170358834 -3600 # Node ID 7c27195a4afc6e1219780af1e96175fd402f1b7c # Parent 7f88a6848fc2e4e47c850633af8939602a61224c proper use of PureThy.has_name_hint instead of hard-wired string''; diff -r 7f88a6848fc2 -r 7c27195a4afc src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Feb 01 20:40:17 2007 +0100 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Feb 01 20:40:34 2007 +0100 @@ -215,8 +215,7 @@ fun tell_thm_deps ths = if Output.has_mode thm_depsN then let - val names = filter_out (equal PureThy.unknown_name_hint) - (map PureThy.get_name_hint ths); + val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths); val deps = Symtab.keys (fold Proofterm.thms_of_proof' (map Thm.proof_of ths) Symtab.empty); in diff -r 7f88a6848fc2 -r 7c27195a4afc src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Feb 01 20:40:17 2007 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Feb 01 20:40:34 2007 +0100 @@ -16,7 +16,7 @@ (* Yet more message functions... *) val nonfatal_error : string -> unit (* recoverable error *) - val log_msg : string -> unit (* for internal log messages *) + val log_msg : string -> unit (* for internal log messages *) val error_with_pos : PgipTypes.fatality -> Position.T -> string -> unit val get_currently_open_file : unit -> Path.T option (* interface focus *) @@ -218,7 +218,7 @@ hand the output functions were tuned some time ago, so it ought to be enough to use Rawtext always above. *) (* NB 2: all of standard functions print strings terminated with new lines, but we don't - add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages + add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages can't be written without newlines. *) fun setup_messages () = @@ -240,15 +240,15 @@ fun tell_clear_goals () = issue_pgip (Cleardisplay {area=Display}) fun tell_clear_response () = issue_pgip (Cleardisplay {area=Message}) -fun tell_file_loaded completed path = +fun tell_file_loaded completed path = issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path, - completed=completed}) -fun tell_file_outdated completed path = + completed=completed}) +fun tell_file_outdated completed path = issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path, - completed=completed}) -fun tell_file_retracted completed path = + completed=completed}) +fun tell_file_retracted completed path = issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path, - completed=completed}) + completed=completed}) @@ -257,7 +257,7 @@ local fun statedisplay prts = - let + let val display = Pretty.output (Pretty.chunks prts) (* TODO: add extra PGML markup for allow proof state navigation *) val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display]) @@ -266,13 +266,13 @@ end fun print_current_goals n m st = - case (Display.pretty_current_goals n m st) of + case (Display.pretty_current_goals n m st) of [] => tell_clear_goals() | prts => statedisplay prts fun print_state b st = - case (Toplevel.pretty_state b st) of - [] => tell_clear_goals() + case (Toplevel.pretty_state b st) of + [] => tell_clear_goals() | prts => statedisplay prts in @@ -287,21 +287,21 @@ (* theory loader actions *) local - (* da: TODO: PGIP has a completed flag so the prover can indicate to the - interface which files are busy performing a particular action. + (* da: TODO: PGIP has a completed flag so the prover can indicate to the + interface which files are busy performing a particular action. To make use of this we need to adjust the hook in thy_info.ML - (may actually be difficult to tell the interface *which* action is in + (may actually be difficult to tell the interface *which* action is in progress, but we could add a generic "Lock" action which uses informfileloaded: the broker/UI should not infer too much from incomplete operations). - *) + *) fun trace_action action name = if action = ThyInfo.Update then - List.app (tell_file_loaded true) (ThyInfo.loaded_files name) + List.app (tell_file_loaded true) (ThyInfo.loaded_files name) else if action = ThyInfo.Outdate then List.app (tell_file_outdated true) (ThyInfo.loaded_files name) else if action = ThyInfo.Remove then - List.app (tell_file_retracted true) (ThyInfo.loaded_files name) + List.app (tell_file_retracted true) (ThyInfo.loaded_files name) else () @@ -356,14 +356,14 @@ end fun tell_thm_deps ths = - if Output.has_mode thm_depsN then - let - val names = filter_out (equal PureThy.unknown_name_hint) (map PureThy.get_name_hint ths) - val deps = (Symtab.keys (fold Proofterm.thms_of_proof' - (map Thm.proof_of ths) Symtab.empty)) - in - if null names orelse null deps then () - else thm_deps_message (spaces_quote names, spaces_quote deps) + if Output.has_mode thm_depsN then + let + val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths); + val deps = (Symtab.keys (fold Proofterm.thms_of_proof' + (map Thm.proof_of ths) Symtab.empty)) + in + if null names orelse null deps then () + else thm_deps_message (spaces_quote names, spaces_quote deps) end else () @@ -439,8 +439,8 @@ preferences := (* PGIP uses markup for distinguishing variable types *) (!preferences |> Preferences.set_default ("show-question-marks","false") - |> Preferences.remove "show-question-marks"); - + |> Preferences.remove "show-question-marks"); + (* Sending commands to Isar *) @@ -561,7 +561,7 @@ (*** PGIP identifier tables ***) -(* TODO: these ones should be triggered by hooks after a +(* TODO: these ones should be triggered by hooks after a declaration addition/removal, to be sent automatically. *) fun addids t = issue_pgip (Addids {idtables = [t]}) @@ -575,48 +575,48 @@ fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} - fun setids t = issue_pgip (Setids {idtables = [t]}) + fun setids t = issue_pgip (Setids {idtables = [t]}) (* fake one-level nested "subtheories" by picking apart names. *) - val thms_of_thy = - map fst o NameSpace.extern_table o PureThy.theorems_of o ThyInfo.get_theory; + val thms_of_thy = + map fst o NameSpace.extern_table o PureThy.theorems_of o ThyInfo.get_theory; val isnested_id = String.isSubstring NameSpace.separator val immed_thms_of_thy = filter_out isnested_id o thms_of_thy fun thy_prefix s = case space_explode NameSpace.separator s of - x::_::_ => SOME x (* String.find? *) - | _ => NONE - fun subthys_of_thy s = - foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) [] - (map thy_prefix (thms_of_thy s)) - fun subthms_of_thy thy = - (case thy_prefix thy of - NONE => immed_thms_of_thy thy - | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy)) - (thms_of_thy prf)) + x::_::_ => SOME x (* String.find? *) + | _ => NONE + fun subthys_of_thy s = + foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) [] + (map thy_prefix (thms_of_thy s)) + fun subthms_of_thy thy = + (case thy_prefix thy of + NONE => immed_thms_of_thy thy + | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy)) + (thms_of_thy prf)) val qualified_thms_of_thy = (* for global query with single response *) - filter_out (equal PureThy.unknown_name_hint) o - (map fst) o PureThy.thms_of o ThyInfo.get_theory; - in + map PureThy.get_name_hint o filter PureThy.has_name_hint o + map snd o PureThy.thms_of o ThyInfo.get_theory; + in case (thyname,objtype) of - (NONE, NONE) => - setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*) - | (NONE, SOME ObjFile) => - setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*) - | (SOME fi, SOME ObjFile) => - setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *) + (NONE, NONE) => + setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*) + | (NONE, SOME ObjFile) => + setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*) + | (SOME fi, SOME ObjFile) => + setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *) | (NONE, SOME ObjTheory) => - setids (idtable ObjTheory NONE (ThyInfo.names())) + setids (idtable ObjTheory NONE (ThyInfo.names())) | (SOME thy, SOME ObjTheory) => - setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy)) - | (SOME thy, SOME ObjTheorem) => - setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)) - | (NONE, SOME ObjTheorem) => - (* A large query, but not unreasonable. ~5000 results for HOL.*) - (* Several setids should be allowed, but Eclipse code is currently broken: + setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy)) + | (SOME thy, SOME ObjTheorem) => + setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)) + | (NONE, SOME ObjTheorem) => + (* A large query, but not unreasonable. ~5000 results for HOL.*) + (* Several setids should be allowed, but Eclipse code is currently broken: Library.seq (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))) - (ThyInfo.names()) *) + (ThyInfo.names()) *) setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *) - (flat (map qualified_thms_of_thy (ThyInfo.names())))) + (maps qualified_thms_of_thy (ThyInfo.names()))) | _ => warning ("askids: ignored argument combination") end @@ -631,47 +631,47 @@ val thms_of_thy = map fst o PureThy.thms_of o ThyInfo.get_theory - val thy_name = Path.implode o #1 o Path.split_ext o Path.base + val thy_name = Path.implode o #1 o Path.split_ext o Path.base - fun filerefs f = - let val thy = thy_name f - val (_,filerefs) = OuterSyntax.deps_thy thy true f (* (Path.unpack f); *) - in - issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, - name=NONE, idtables=[], fileurls=filerefs}) - end + fun filerefs f = + let val thy = thy_name f + val (_,filerefs) = OuterSyntax.deps_thy thy true f (* (Path.unpack f); *) + in + issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, + name=NONE, idtables=[], fileurls=filerefs}) + end - fun thyrefs thy = - let val ml_path = ThyLoad.ml_path thy - val (thyrefs,_) = OuterSyntax.deps_thy thy true ml_path (* (Path.unpack f); *) - in - issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, - name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, - ids=thyrefs}], fileurls=[]}) - end + fun thyrefs thy = + let val ml_path = ThyLoad.ml_path thy + val (thyrefs,_) = OuterSyntax.deps_thy thy true ml_path (* (Path.unpack f); *) + in + issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, + name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, + ids=thyrefs}], fileurls=[]}) + end - fun thmrefs thmname = - let - (* TODO: interim: this is probably not right. - What we want is mapping onto simple PGIP name/context model. *) - val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *) - val thy = Context.theory_of_proof ctx - val ths = [PureThy.get_thm thy (PureThy.Name thmname)] - val deps = filter_out (equal "") - (Symtab.keys (fold Proofterm.thms_of_proof - (map Thm.proof_of ths) Symtab.empty)) - in - if null deps then () - else issue_pgip (Setrefs {url=url, thyname=thyname, name=name, - objtype=SOME PgipTypes.ObjTheorem, - idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem, - ids=deps}], fileurls=[]}) - end + fun thmrefs thmname = + let + (* TODO: interim: this is probably not right. + What we want is mapping onto simple PGIP name/context model. *) + val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *) + val thy = Context.theory_of_proof ctx + val ths = [PureThy.get_thm thy (PureThy.Name thmname)] + val deps = filter_out (equal "") + (Symtab.keys (fold Proofterm.thms_of_proof + (map Thm.proof_of ths) Symtab.empty)) + in + if null deps then () + else issue_pgip (Setrefs {url=url, thyname=thyname, name=name, + objtype=SOME PgipTypes.ObjTheorem, + idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem, + ids=deps}], fileurls=[]}) + end in case (url,thyname,objtype,name) of - (SOME file, NONE, _, _) => filerefs file - | (_,SOME thy,_,_) => thyrefs thy - | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname + (SOME file, NONE, _, _) => filerefs file + | (_,SOME thy,_,_) => thyrefs thy + | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname | _ => error ("Unimplemented/invalid case of ") end @@ -860,17 +860,17 @@ in case !currently_open_file of SOME f => raise PGIP (" when a file is already open!\nCurrently open file: " ^ - PgipTypes.string_of_pgipurl url) + PgipTypes.string_of_pgipurl url) | NONE => (openfile_retract filepath; changecwd_dir filedir; - priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url); + priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url); currently_open_file := SOME url) end fun closefile vs = case !currently_open_file of SOME f => (proper_inform_file_processed f (Isar.state()); - priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f); + priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f); currently_open_file := NONE) | NONE => raise PGIP (" when no file is open!") @@ -883,16 +883,16 @@ e.g. file loaded depends on open file which is not yet saved. *) (* case !currently_open_file of SOME f => raise PGIP (" when a file is open!\nCurrently open file: " ^ - PgipTypes.string_of_pgipurl url) + PgipTypes.string_of_pgipurl url) | NONE => *) - use_thy_or_ml_file (File.platform_path url) + use_thy_or_ml_file (File.platform_path url) end fun abortfile vs = case !currently_open_file of SOME f => (isarcmd "init_toplevel"; - priority ("Aborted working in file: " ^ - PgipTypes.string_of_pgipurl f); + priority ("Aborted working in file: " ^ + PgipTypes.string_of_pgipurl f); currently_open_file := NONE) | NONE => raise PGIP (" when no file is open!") @@ -903,11 +903,11 @@ case !currently_open_file of SOME f => raise PGIP (" when a file is open!") | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url); - (* TODO: next should be in thy loader, here just for testing *) - let - val name = thy_name url - in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end; - inform_file_retracted url) + (* TODO: next should be in thy loader, here just for testing *) + let + val name = thy_name url + in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end; + inform_file_retracted url) end @@ -1092,7 +1092,7 @@ (! initialized orelse (setmp warning_fn (K ()) init_outer_syntax (); PgipParser.init (); - setup_preferences_tweak (); + setup_preferences_tweak (); setup_xsymbols_output (); setup_pgml_output (); setup_messages (); @@ -1129,4 +1129,3 @@ end end; - diff -r 7f88a6848fc2 -r 7c27195a4afc src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Feb 01 20:40:17 2007 +0100 +++ b/src/Pure/pure_thy.ML Thu Feb 01 20:40:34 2007 +0100 @@ -31,7 +31,6 @@ val untag_rule: string -> thm -> thm val tag: tag -> attribute val untag: string -> attribute - val unknown_name_hint: string val has_name_hint: thm -> bool val get_name_hint: thm -> string val put_name_hint: string -> thm -> thm @@ -118,14 +117,12 @@ (* unofficial theorem names *) -val unknown_name_hint = "??.unknown"; - fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) "name"; fun get_name_hint thm = (case AList.lookup (op =) (Thm.get_tags thm) "name" of SOME (k :: _) => k - | _ => unknown_name_hint); + | _ => "??.unknown"); fun put_name_hint name = untag_rule "name" #> tag_rule ("name", [name]);