author wenzelm Mon Feb 27 20:33:18 2012 +0100 (2012-02-27) changeset 46718 dfaf51de90ad parent 46717 b09afce1e54f child 46719 61cd0ad6cd42
tuned;
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Feb 27 20:23:57 2012 +0100
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Feb 27 20:33:18 2012 +0100
1.3 @@ -1,5 +1,6 @@
1.4  (*  Title:      Pure/Tools/find_theorems.ML
1.5      Author:     Rafal Kolanski and Gerwin Klein, NICTA
1.6 +    Author:     Lars Noschinski and Alexander Krauss, TU Muenchen
1.7
1.8  Retrieve theorems from proof context.
1.9  *)
1.10 @@ -108,7 +109,7 @@
1.11  };
1.12
1.13  fun map_criteria f {goal, limit, rem_dups, criteria} =
1.14 -  {goal=goal, limit=limit, rem_dups=rem_dups, criteria=f criteria};
1.15 +  {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria};
1.16
1.17  fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), [])
1.18    | xml_of_criterion Intro = XML.Elem (("Intro", []) , [])
1.19 @@ -127,7 +128,7 @@
1.20    | criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
1.21    | criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
1.22
1.23 -fun xml_of_query {goal=NONE, limit, rem_dups, criteria} =
1.24 +fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
1.25        let
1.26          val properties = []
1.27            |> (if rem_dups then cons ("rem_dups", "") else I)
1.28 @@ -146,7 +147,7 @@
1.29            XML.Decode.list (XML.Decode.pair XML.Decode.bool
1.30              (criterion_of_xml o the_single)) body;
1.31        in
1.32 -        {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
1.33 +        {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
1.34        end
1.35    | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
1.36
1.37 @@ -172,8 +173,9 @@
1.38        let
1.39          val name = the (Properties.get properties "name");
1.40          val pos = Position.of_properties properties;
1.41 -        val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
1.42 -          (Properties.get properties "index");
1.43 +        val intvs_opt =
1.44 +          Option.map (single o Facts.Single o Markup.parse_int)
1.45 +            (Properties.get properties "index");
1.46        in
1.47          External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
1.48        end
1.49 @@ -310,7 +312,7 @@
1.50          andalso not (null successful)
1.51        then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
1.52      end
1.53 -  else NONE
1.54 +  else NONE;
1.55
1.56  val tac_limit = Unsynchronized.ref 5;
1.57
1.58 @@ -423,7 +425,6 @@
1.59  fun lazy_filter filters =
1.60    let
1.61      fun lazy_match thms = Seq.make (fn () => first_match thms)
1.62 -
1.63      and first_match [] = NONE
1.64        | first_match (thm :: thms) =
1.65            (case app_filters thm (SOME (0, 0), NONE, filters) of
1.66 @@ -464,7 +465,7 @@
1.67
1.68  fun nicer_shortest ctxt =
1.69    let
1.70 -    (* FIXME global name space!? *)
1.71 +    (* FIXME Why global name space!?? *)
1.72      val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt));
1.73
1.74      val shorten =
1.75 @@ -507,7 +508,7 @@
1.76
1.77  fun filter_theorems ctxt theorems query =
1.78    let
1.79 -    val {goal=opt_goal, limit=opt_limit, rem_dups, criteria} = query
1.80 +    val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query;
1.81      val filters = map (filter_criterion ctxt opt_goal) criteria;
1.82
1.83      fun find_all theorems =
1.84 @@ -530,8 +531,8 @@
1.85
1.86    in find theorems end;
1.87
1.88 -fun filter_theorems_cmd ctxt theorems raw_query =
1.89 -  filter_theorems ctxt theorems (map_criteria
1.90 +fun filter_theorems_cmd ctxt theorems raw_query =
1.91 +  filter_theorems ctxt theorems (map_criteria
1.92      (map (apsnd (read_criterion ctxt))) raw_query);
1.93
1.94  fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
1.95 @@ -542,8 +543,8 @@
1.96      val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
1.97      val opt_goal' = Option.map add_prems opt_goal;
1.98    in
1.99 -    filter ctxt (map Internal (all_facts_of ctxt))
1.100 -      {goal=opt_goal', limit=opt_limit, rem_dups=rem_dups, criteria=raw_criteria}
1.101 +    filter ctxt (map Internal (all_facts_of ctxt))
1.102 +      {goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria}
1.103      |> apsnd (map (fn Internal f => f))
1.104    end;
1.105
1.106 @@ -563,7 +564,7 @@
1.107    let
1.108      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
1.109      val (foundo, theorems) = find
1.110 -      {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria};
1.111 +      {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
1.112      val returned = length theorems;
1.113
1.114      val tally_msg =
1.115 @@ -587,6 +588,7 @@
1.116    gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;
1.117
1.118
1.119 +
1.120  (** command syntax **)
1.121
1.122  local
```