added new_thms_deps (operates on global facts, some name_hint approximation);
authorwenzelm
Tue Sep 02 22:20:27 2008 +0200 (2008-09-02)
changeset 28097003dff7410c1
parent 28096 046418f64474
child 28098 c92850d2d16c
added new_thms_deps (operates on global facts, some name_hint approximation);
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 02 22:20:25 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 02 22:20:27 2008 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  signature PROOF_GENERAL_PGIP =
     1.6  sig
     1.7 +  val new_thms_deps: Toplevel.state -> Toplevel.state -> string list * string list
     1.8    val init_pgip: bool -> unit             (* main PGIP loop with true; fail with false *)
     1.9  
    1.10    (* These two are just to support the semi-PGIP Emacs mode *)
    1.11 @@ -245,7 +246,38 @@
    1.12       welcome ());
    1.13  
    1.14  
    1.15 -(* theorem dependency output *)
    1.16 +(* theorem dependencies *)
    1.17 +
    1.18 +local
    1.19 +
    1.20 +fun thm_deps th =
    1.21 +  (case Thm.proof_of th of
    1.22 +    PThm (name, prf, _, _) =>
    1.23 +      if Thm.has_name_hint th andalso Thm.get_name_hint th = name then
    1.24 +        Proofterm.thms_of_proof' prf
    1.25 +      else I
    1.26 +  | prf => Proofterm.thms_of_proof' prf);
    1.27 +
    1.28 +fun thms_deps ths =
    1.29 +  let
    1.30 +    (* FIXME proper derivation names!? *)
    1.31 +    val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
    1.32 +    val deps = Symtab.keys (fold thm_deps ths Symtab.empty);
    1.33 +  in (names, deps) end;
    1.34 +
    1.35 +in
    1.36 +
    1.37 +fun new_thms_deps state state' =
    1.38 +  let
    1.39 +    val prev_facts =
    1.40 +      (case try Toplevel.theory_of state of NONE => [] | SOME thy => [PureThy.facts_of thy]);
    1.41 +    val facts = PureThy.facts_of (Toplevel.theory_of state');
    1.42 +  in thms_deps (maps #2 (Facts.dest_static prev_facts facts)) end;
    1.43 +
    1.44 +end;
    1.45 +
    1.46 +
    1.47 +(* theorem dependeny output *)
    1.48  
    1.49  val show_theorem_dependencies = ref false;
    1.50  
    1.51 @@ -254,33 +286,28 @@
    1.52  val spaces_quote = space_implode " " o map quote;
    1.53  
    1.54  fun thm_deps_message (thms, deps) =
    1.55 -    let
    1.56 -        val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms])
    1.57 -        val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps])
    1.58 -    in
    1.59 -        issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")],
    1.60 -                                      content=[valuethms,valuedeps]})
    1.61 -    end
    1.62 -
    1.63 -fun tell_thm_deps ths =
    1.64 -  if !show_theorem_dependencies then
    1.65 -      let
    1.66 -        val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
    1.67 -        val deps = (Symtab.keys (fold Proofterm.thms_of_proof'
    1.68 -                                        (map Thm.proof_of ths) Symtab.empty))
    1.69 -      in
    1.70 -          if null names orelse null deps then ()
    1.71 -          else thm_deps_message (spaces_quote names, spaces_quote deps)
    1.72 -      end
    1.73 -  else ()
    1.74 +  let
    1.75 +    val valuethms = XML.Elem ("value", [("name", "thms")], [XML.Text thms]);
    1.76 +    val valuedeps = XML.Elem ("value", [("name", "deps")], [XML.Text deps]);
    1.77 +  in
    1.78 +    issue_pgip (Metainforesponse
    1.79 +      {attrs = [("infotype", "isabelle_theorem_dependencies")],
    1.80 +       content = [valuethms, valuedeps]})
    1.81 +  end;
    1.82  
    1.83  in
    1.84  
    1.85 -fun setup_present_hook () =
    1.86 -  ProofDisplay.add_hook (fn res => tell_thm_deps (maps #2 res));
    1.87 +fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
    1.88 +  if ! show_theorem_dependencies andalso Toplevel.is_theory state' andalso is_none opt_err then
    1.89 +    let val (names, deps) = new_thms_deps state state' in
    1.90 +      if null names orelse null deps then ()
    1.91 +      else thm_deps_message (spaces_quote names, spaces_quote deps)
    1.92 +    end
    1.93 +  else ());
    1.94  
    1.95  end;
    1.96  
    1.97 +
    1.98  (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
    1.99  
   1.100  fun lexicalstructure_keywords () =
   1.101 @@ -1041,4 +1068,3 @@
   1.102  end
   1.103  
   1.104  end;
   1.105 -