src/Pure/Tools/find_consts.ML
author Timothy Bourke
Tue, 03 Mar 2009 12:14:52 +1100
changeset 30207 c56d27155041
parent 30206 48507466d9d2
child 31684 d5d830979a54
permissions -rw-r--r--
Implement Makarius's suggestion for improved type pattern parsing.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
     1
(*  Title:      Pure/Tools/find_consts.ML
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
     2
    Author:     Timothy Bourke and Gerwin Klein, NICTA
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
     3
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
     4
Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
     5
type over constants, but matching is not fuzzy.
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
     6
*)
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
     7
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
     8
signature FIND_CONSTS =
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
     9
sig
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    10
  datatype criterion =
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    11
      Strict of string
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    12
    | Loose of string
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    13
    | Name of string
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    14
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    15
  val find_consts : Proof.context -> (bool * criterion) list -> unit
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    16
end;
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    17
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    18
structure FindConsts : FIND_CONSTS =
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    19
struct
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    20
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    21
(* search criteria *)
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    22
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    23
datatype criterion =
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    24
    Strict of string
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    25
  | Loose of string
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    26
  | Name of string;
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    27
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    28
(* matching types/consts *)
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    29
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    30
fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    31
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    32
fun matches_subtype thy typat =
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    33
  let
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    34
    val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    35
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    36
    fun fs [] = false
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    37
      | fs (t :: ts) = f t orelse fs ts
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    38
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    39
    and f (t as Type (_, ars)) = p t orelse fs ars
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    40
      | f t = p t;
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    41
  in f end;
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    42
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    43
fun check_const p (nm, (ty, _)) =
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    44
  if p (nm, ty)
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    45
  then SOME (Term.size_of_typ ty)
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    46
  else NONE;
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    47
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    48
fun opt_not f (c as (_, (ty, _))) =
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    49
  if is_some (f c)
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    50
  then NONE else SOME (Term.size_of_typ ty);
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    51
30206
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
    52
fun filter_const _ NONE = NONE
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
    53
  | filter_const f (SOME (c, r)) =
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    54
      Option.map (pair c o (curry Int.min r)) (f c);
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    55
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    56
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    57
(* pretty results *)
29895
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    58
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    59
fun pretty_criterion (b, c) =
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    60
  let
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    61
    fun prfx s = if b then s else "-" ^ s;
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    62
  in
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    63
    (case c of
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    64
      Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    65
    | Loose pat => Pretty.str (prfx (quote pat))
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    66
    | Name name => Pretty.str (prfx "name: " ^ quote name))
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    67
  end;
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    68
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    69
fun pretty_const ctxt (nm, ty) =
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    70
  let
29895
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    71
    val ty' = Logic.unvarifyT ty;
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    72
  in
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    73
    Pretty.block
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    74
     [Pretty.quote (Pretty.str nm), Pretty.fbrk,
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    75
      Pretty.str "::", Pretty.brk 1,
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    76
      Pretty.quote (Syntax.pretty_typ ctxt ty')]
29895
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    77
  end;
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    78
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    79
(* find_consts *)
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    80
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    81
fun find_consts ctxt raw_criteria =
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    82
  let
29895
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    83
    val start = start_timing ();
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    84
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    85
    val thy = ProofContext.theory_of ctxt;
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    86
    val low_ranking = 10000;
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    87
30206
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
    88
    fun not_internal consts (nm, _) = 
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
    89
      if member (op =) (Consts.the_tags consts nm) Markup.property_internal
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
    90
      then NONE else SOME low_ranking;
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
    91
30207
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    92
    fun make_pattern crit =
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    93
      let
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    94
        val raw_T = Syntax.parse_typ ctxt crit;
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    95
        val t = Syntax.check_term
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    96
                  (ProofContext.set_mode ProofContext.mode_pattern ctxt)
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    97
                  (Term.dummy_pattern raw_T);
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    98
      in Term.type_of t end;
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    99
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   100
    fun make_match (Strict arg) =
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   101
          let val qty = make_pattern arg; in
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
   102
            fn (_, (ty, _)) =>
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
   103
              let
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   104
                val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   105
                val sub_size = Vartab.fold add_tye tye 0;
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   106
              in SOME sub_size end handle MATCH => NONE
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   107
          end
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   108
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   109
      | make_match (Loose arg) =
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   110
          check_const (matches_subtype thy (make_pattern arg) o snd)
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   111
      
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   112
      | make_match (Name arg) = check_const (match_string arg o fst);
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   113
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   114
    fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
30206
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
   115
    val criteria = map make_criterion raw_criteria;
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   116
30206
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
   117
    val consts = Sign.consts_of thy;
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
   118
    val (_, consts_tab) = (#constants o Consts.dest) consts;
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
   119
    fun eval_entry c = fold filter_const (not_internal consts::criteria)
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
   120
                                         (SOME (c, low_ranking));
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   121
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
   122
    val matches =
30206
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
   123
      Symtab.fold (cons o eval_entry) consts_tab []
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
   124
      |> map_filter I
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
   125
      |> sort (rev_order o int_ord o pairself snd)
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
   126
      |> map ((apsnd fst) o fst);
29895
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   127
30188
82144a95f9ec avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
wenzelm
parents: 30143
diff changeset
   128
    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   129
  in
29895
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   130
    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   131
      :: Pretty.str ""
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   132
      :: (Pretty.str o concat)
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   133
           (if null matches
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   134
            then ["nothing found", end_msg]
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   135
            else ["found ", (string_of_int o length) matches,
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   136
                  " constants", end_msg, ":"])
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   137
      :: Pretty.str ""
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   138
      :: map (pretty_const ctxt) matches
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
   139
    |> Pretty.chunks
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   140
    |> Pretty.writeln
30206
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
   141
  end;
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   142
30142
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   143
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
   144
(* command syntax *)
30142
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   145
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   146
fun find_consts_cmd spec =
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   147
  Toplevel.unknown_theory o Toplevel.keep (fn state =>
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   148
    find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   149
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   150
local
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   151
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   152
structure P = OuterParse and K = OuterKeyword;
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   153
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   154
val criterion =
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   155
  P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   156
  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   157
  P.xname >> Loose;
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   158
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   159
in
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   160
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   161
val _ =
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   162
  OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   163
    (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   164
      >> (Toplevel.no_timing oo find_consts_cmd));
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   165
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   166
end;
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   167
30142
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   168
end;
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   169