# HG changeset patch # User aspinall # Date 1169476455 -3600 # Node ID 0cf0d3912239c3776d71db3a2625546a7cd4c54b # Parent ff4fc4ee9eb0bdd46990beaf9f33c28edb32b712 Comment diff -r ff4fc4ee9eb0 -r 0cf0d3912239 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jan 22 15:33:42 2007 +0100 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jan 22 15:34:15 2007 +0100 @@ -216,7 +216,7 @@ fun tell_thm_deps ths = if Output.has_mode thm_depsN then let - val names = filter_out (equal "") (map PureThy.get_name_hint ths); + val names = filter_out (equal "") (map PureThy.get_name_hint ths); (* da: HAS THIS NOW BECOME "??.unknown"? *) val deps = filter_out (equal "") (Symtab.keys (fold Proofterm.thms_of_proof (map Thm.proof_of ths) Symtab.empty)); diff -r ff4fc4ee9eb0 -r 0cf0d3912239 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jan 22 15:33:42 2007 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jan 22 15:34:15 2007 +0100 @@ -17,6 +17,8 @@ (* Yet more message functions... *) val nonfatal_error : string -> unit (* recoverable error *) val log_msg : string -> unit (* for internal log messages *) + + val error_with_pos : PgipTypes.fatality -> Position.T -> string -> unit end structure ProofGeneralPgip : PROOF_GENERAL_PGIP = @@ -190,12 +192,22 @@ val content = XML.Elem("pgmltext",[],[XML.Rawtext s]) val pgip = Errorresponse {area=NONE,fatality=fatality, content=[content], - (* FIXME: pass in locations *) location=NONE} in queue_or_issue pgip end + (* Error responses with useful locations *) + fun error_with_pos fatality pos s = + let + val content = XML.Elem("pgmltext",[],[XML.Rawtext s]) + val pgip = Errorresponse {area=NONE,fatality=fatality, + content=[content], + location=SOME (PgipIsabelle.location_of_position pos)} + in + queue_or_issue pgip + end + fun start_delay_msgs () = (set delay_msgs; delayed_msgs := []) fun end_delayed_msgs () = (reset delay_msgs; ! delayed_msgs) end; @@ -346,7 +358,7 @@ fun tell_thm_deps ths = if Output.has_mode thm_depsN then let - val names = filter_out (equal "") (map PureThy.get_name_hint ths); + val names = filter_out (equal "") (map PureThy.get_name_hint ths); (* da: HAS THIS NOW BECOME "??.unknown"? *) val deps = filter_out (equal "") (Symtab.keys (fold Proofterm.thms_of_proof (map Thm.proof_of ths) Symtab.empty)); @@ -540,14 +552,11 @@ (*** PGIP identifier tables ***) -fun setids t = issue_pgip (Setids {idtables = [t]}) -fun addids t = issue_pgip (Addids {idtables = [t]}) -fun delids t = issue_pgip (Delids {idtables = [t]}) +(* TODO: these ones should be triggered by hooks after a + declaration addition/removal, to be sent automatically. *) -(* - fun delallids ty = - issue_pgip (Setids {idtables = - [{context=NONE,objtype=ty,ids=[]}]}) *) +fun addids t = issue_pgip (Addids {idtables = [t]}) +fun delids t = issue_pgip (Delids {idtables = [t]}) fun askids (Askids vs) = let @@ -557,6 +566,8 @@ fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} + fun setids t = issue_pgip (Setids {idtables = [t]}) + val thms_of_thy = map fst o PureThy.thms_of o ThyInfo.get_theory in (* case (url_attr,thyname,objtype) of @@ -579,6 +590,63 @@ | (_, SOME ot) => error ("No objects of type "^(PgipTypes.name_of_objtype ot)^" are available here.") end +fun askrefs (Askrefs vs) = + let + val url = #url vs (* ask for references of a file (i.e. immediate pre-requisites) *) + val thyname = #thyname vs (* ask for references of a theory (other theories) *) + val objtype = #objtype vs (* ask for references of a particular type... *) + val name = #name vs (* ... with this name *) + + fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} + + 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 + + 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 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 + | _ => error ("Unimplemented/invalid case of ") + end + + + local (* accumulate printed output in a single PGIP response (inside ) *) fun with_displaywrap pgipfn dispfn = @@ -839,6 +907,7 @@ | Pgip.Restoregoal _ => error " not implemented" | Pgip.Abortgoal _ => abortgoal inp | Pgip.Askids _ => askids inp + | Pgip.Askrefs _ => askrefs inp | Pgip.Showid _ => showid inp | Pgip.Askguise _ => askguise inp | Pgip.Parsescript _ => parsescript inp