author wenzelm Fri Aug 02 22:46:54 2013 +0200 (2013-08-02) changeset 52855 fb1f026c48ff parent 52854 92932931bd82 child 52856 46c339daaff2
some actual find_theorems functionality;
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:17:53 2013 +0200
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 02 22:46:54 2013 +0200
1.3 @@ -21,7 +21,7 @@
1.4    }
1.5
1.6    val read_criterion: Proof.context -> string criterion -> term criterion
1.7 -  val query_parser: (bool * string criterion) list parser
1.8 +  val parse_query: string -> (bool * string criterion) list
1.9
1.10    val xml_of_query: term query -> XML.tree
1.11    val query_of_xml: XML.tree -> term query
1.12 @@ -496,7 +496,7 @@
1.13  end;
1.14
1.15
1.16 -(* print_theorems *)
1.17 +(* pretty_theorems *)
1.18
1.19  fun all_facts_of ctxt =
1.20    let
1.21 @@ -572,11 +572,12 @@
1.22
1.23  fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
1.24
1.25 -fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
1.26 +fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
1.27    let
1.28      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
1.29 -    val (foundo, theorems) = find
1.30 -      {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
1.31 +    val (foundo, theorems) =
1.32 +      filter_theorems ctxt (map Internal (all_facts_of ctxt))
1.33 +        {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
1.34      val returned = length theorems;
1.35
1.36      val tally_msg =
1.37 @@ -594,10 +595,13 @@
1.38       else
1.39        [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
1.40          grouped 10 Par_List.map (pretty_theorem ctxt) theorems)
1.41 -  end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
1.42 +  end |> Pretty.fbreaks |> curry Pretty.blk 0;
1.43
1.44 -fun print_theorems ctxt =
1.45 -  gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;
1.46 +fun pretty_theorems_cmd state opt_lim rem_dups spec =
1.47 +  let
1.48 +    val ctxt = Toplevel.context_of state;
1.49 +    val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
1.50 +  in pretty_theorems ctxt opt_goal opt_lim rem_dups spec end;
1.51
1.52
1.53
1.54 @@ -619,20 +623,25 @@
1.55      (Parse.\$\$\$ "(" |--
1.56        Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
1.57          --| Parse.\$\$\$ ")")) (NONE, true);
1.58 +
1.59 +val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
1.60 +
1.61  in
1.62
1.63 -val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
1.64 +(* FIXME proper wrapper for parser combinator *)
1.65 +fun parse_query str =
1.66 +  (str ^ ";")
1.67 +  |> Outer_Syntax.scan Position.start
1.68 +  |> filter Token.is_proper
1.69 +  |> Scan.error query_parser
1.70 +  |> fst;
1.71
1.72  val _ =
1.73    Outer_Syntax.improper_command @{command_spec "find_theorems"}
1.74      "find theorems meeting specified criteria"
1.75 -    (options -- query_parser
1.76 -      >> (fn ((opt_lim, rem_dups), spec) =>
1.77 -        Toplevel.keep (fn state =>
1.78 -          let
1.79 -            val ctxt = Toplevel.context_of state;
1.80 -            val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
1.81 -          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
1.82 +    (options -- query_parser >> (fn ((opt_lim, rem_dups), spec) =>
1.83 +      Toplevel.keep (fn state =>
1.84 +        Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec))));
1.85
1.86  end;
1.87
1.88 @@ -647,8 +656,14 @@
1.89      (case args of
1.90        [instance, query] =>
1.91        SOME {delay = NONE, pri = 0, persistent = false,
1.92 -        print_fn = fn _ => fn st =>
1.93 -          Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] query}
1.94 +        print_fn = fn _ => fn state =>
1.95 +          let
1.96 +            val msg =
1.97 +              Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query))
1.98 +                handle exn =>
1.99 +                  if Exn.is_interrupt exn then reraise exn
1.100 +                  else ML_Compiler.exn_message exn;  (* FIXME error markup!? *)
1.101 +          in Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] msg end}
1.102      | _ => NONE));
1.103
1.104  end;
```
```     2.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Fri Aug 02 22:17:53 2013 +0200
2.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Fri Aug 02 22:46:54 2013 +0200
2.3 @@ -16,12 +16,7 @@
2.4      val args = Symtab.lookup arg_data;
2.5
2.6      val query_str = the_default "" (args "query");
2.7 -    fun get_query () =
2.8 -      (query_str ^ ";")
2.9 -      |> Outer_Syntax.scan Position.start
2.10 -      |> filter Token.is_proper
2.11 -      |> Scan.error Find_Theorems.query_parser
2.12 -      |> fst;
2.13 +    fun get_query () = Find_Theorems.parse_query query_str;
2.14
2.15      val limit = case args "limit" of
2.16          NONE => default_limit
```