reactivate time measurement (partly reverting c27b0b37041a);
authorkrauss
Fri Feb 25 16:57:44 2011 +0100 (2011-02-25)
changeset 418456611b9cef38b
parent 41844 b933142e02d0
child 41846 b368a7aee46a
reactivate time measurement (partly reverting c27b0b37041a);
export pretty_theorem, to display both internal or external facts
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Feb 25 16:57:43 2011 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Feb 25 16:57:44 2011 +0100
     1.3 @@ -11,8 +11,7 @@
     1.4      Pattern of 'term
     1.5  
     1.6    datatype theorem =
     1.7 -    Internal of Facts.ref * thm |
     1.8 -    External of Facts.ref * term
     1.9 +    Internal of Facts.ref * thm | External of Facts.ref * term
    1.10  
    1.11    val tac_limit: int Unsynchronized.ref
    1.12    val limit: int Unsynchronized.ref
    1.13 @@ -22,7 +21,9 @@
    1.14      int option -> bool -> (bool * string criterion) list ->
    1.15      int option * theorem list
    1.16  
    1.17 +  val pretty_theorem: Proof.context -> theorem -> Pretty.T
    1.18    val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
    1.19 +
    1.20  end;
    1.21  
    1.22  structure Find_Theorems: FIND_THEOREMS =
    1.23 @@ -80,7 +81,7 @@
    1.24    end;
    1.25  
    1.26  
    1.27 -(** theorems, either internal or external (without proof) *)
    1.28 +(** theorems, either internal or external (without proof) **)
    1.29  
    1.30  datatype theorem =
    1.31    Internal of Facts.ref * thm |
    1.32 @@ -452,16 +453,23 @@
    1.33       rem_dups raw_criteria
    1.34    |> apsnd (map (fn Internal f => f));
    1.35  
    1.36 -fun pretty_thm ctxt (thmref, thm) = Pretty.block
    1.37 -  [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    1.38 -    Display.pretty_thm ctxt thm];
    1.39 +fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
    1.40 +      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    1.41 +        Display.pretty_thm ctxt thm]
    1.42 +  | pretty_theorem ctxt (External (thmref, prop)) = Pretty.block
    1.43 +      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    1.44 +        Syntax.unparse_term ctxt prop];
    1.45  
    1.46 -fun print_theorems ctxt (foundo, thms) raw_criteria =
    1.47 +fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
    1.48 +
    1.49 +fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.50    let
    1.51      val start = start_timing ();
    1.52  
    1.53      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.54 -    val returned = length thms;
    1.55 +    val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
    1.56 +      opt_goal opt_limit rem_dups raw_criteria;
    1.57 +    val returned = length theorems;
    1.58  
    1.59      val tally_msg =
    1.60        (case foundo of
    1.61 @@ -476,10 +484,10 @@
    1.62    in
    1.63      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
    1.64      Pretty.str "" ::
    1.65 -    (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
    1.66 +    (if null theorems then [Pretty.str ("nothing found" ^ end_msg)]
    1.67       else
    1.68        [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
    1.69 -        map (pretty_thm ctxt) thms)
    1.70 +        map (pretty_theorem ctxt) theorems)
    1.71    end |> Pretty.chunks |> Pretty.writeln;
    1.72  
    1.73  
    1.74 @@ -515,8 +523,7 @@
    1.75            let
    1.76              val ctxt = Toplevel.context_of state;
    1.77              val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
    1.78 -            val found = find_theorems ctxt opt_goal opt_lim rem_dups spec;
    1.79 -          in print_theorems ctxt found spec end)));
    1.80 +          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
    1.81  
    1.82  end;
    1.83