src/Pure/Tools/find_consts.ML
author wenzelm
Mon, 06 Apr 2015 16:00:19 +0200
changeset 59934 b65c4370f831
parent 59083 88b0b1f28adc
child 59936 b8ffc3dc9e24
permissions -rw-r--r--
more position information and PIDE markup for command keywords;
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
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
    14
  val read_query: Position.T -> string -> (bool * criterion) list
29884
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
33301
1fe9fc908ec3 less hermetic ML;
wenzelm
parents: 33158
diff changeset
    18
structure Find_Consts : FIND_CONSTS =
29884
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
31684
d5d830979a54 minor tuning according to Isabelle/ML conventions;
wenzelm
parents: 30207
diff changeset
    28
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    29
(* matching types/consts *)
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    30
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    31
fun matches_subtype thy typat =
38335
630f379f2660 misc tuning and simplification;
wenzelm
parents: 38334
diff changeset
    32
  Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    33
38335
630f379f2660 misc tuning and simplification;
wenzelm
parents: 38334
diff changeset
    34
fun check_const pred (nm, (ty, _)) =
630f379f2660 misc tuning and simplification;
wenzelm
parents: 38334
diff changeset
    35
  if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    36
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    37
fun opt_not f (c as (_, (ty, _))) =
38335
630f379f2660 misc tuning and simplification;
wenzelm
parents: 38334
diff changeset
    38
  if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    39
46979
ef4b0d6b2fb6 sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents: 46961
diff changeset
    40
fun filter_const _ _ NONE = NONE
ef4b0d6b2fb6 sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents: 46961
diff changeset
    41
  | filter_const c f (SOME rank) =
31684
d5d830979a54 minor tuning according to Isabelle/ML conventions;
wenzelm
parents: 30207
diff changeset
    42
      (case f c of
d5d830979a54 minor tuning according to Isabelle/ML conventions;
wenzelm
parents: 30207
diff changeset
    43
        NONE => NONE
46979
ef4b0d6b2fb6 sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents: 46961
diff changeset
    44
      | SOME i => SOME (Int.min (rank, i)));
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    45
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    46
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    47
(* pretty results *)
29895
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    48
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    49
fun pretty_criterion (b, c) =
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    50
  let
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    51
    fun prfx s = if b then s else "-" ^ s;
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    52
  in
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    53
    (case c of
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    54
      Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    55
    | Loose pat => Pretty.str (prfx (quote pat))
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    56
    | Name name => Pretty.str (prfx "name: " ^ quote name))
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    57
  end;
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    58
49886
0dc57c05bf4e more formal markup;
wenzelm
parents: 48646
diff changeset
    59
fun pretty_const ctxt (c, ty) =
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    60
  let
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 33301
diff changeset
    61
    val ty' = Logic.unvarifyT_global ty;
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 52703
diff changeset
    62
    val const_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 52703
diff changeset
    63
    val markup = Name_Space.markup const_space c;
29895
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    64
  in
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    65
    Pretty.block
49886
0dc57c05bf4e more formal markup;
wenzelm
parents: 48646
diff changeset
    66
     [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    67
      Pretty.quote (Syntax.pretty_typ ctxt ty')]
29895
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    68
  end;
0e70a29d3e02 find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents: 29884
diff changeset
    69
31684
d5d830979a54 minor tuning according to Isabelle/ML conventions;
wenzelm
parents: 30207
diff changeset
    70
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    71
(* find_consts *)
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    72
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
    73
fun pretty_consts ctxt raw_criteria =
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    74
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42012
diff changeset
    75
    val thy = Proof_Context.theory_of ctxt;
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    76
    val low_ranking = 10000;
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    77
33158
6e3dc0ba2b06 conceal consts via name space, not tags;
wenzelm
parents: 32790
diff changeset
    78
    fun user_visible consts (nm, _) =
6e3dc0ba2b06 conceal consts via name space, not tags;
wenzelm
parents: 32790
diff changeset
    79
      if Consts.is_concealed consts nm then NONE else SOME low_ranking;
30206
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
    80
30207
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    81
    fun make_pattern crit =
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    82
      let
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    83
        val raw_T = Syntax.parse_typ ctxt crit;
31684
d5d830979a54 minor tuning according to Isabelle/ML conventions;
wenzelm
parents: 30207
diff changeset
    84
        val t =
d5d830979a54 minor tuning according to Isabelle/ML conventions;
wenzelm
parents: 30207
diff changeset
    85
          Syntax.check_term
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42012
diff changeset
    86
            (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
31684
d5d830979a54 minor tuning according to Isabelle/ML conventions;
wenzelm
parents: 30207
diff changeset
    87
            (Term.dummy_pattern raw_T);
30207
c56d27155041 Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents: 30206
diff changeset
    88
      in Term.type_of t end;
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    89
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    90
    fun make_match (Strict arg) =
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    91
          let val qty = make_pattern arg; in
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    92
            fn (_, (ty, _)) =>
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
    93
              let
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    94
                val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
31684
d5d830979a54 minor tuning according to Isabelle/ML conventions;
wenzelm
parents: 30207
diff changeset
    95
                val sub_size =
d5d830979a54 minor tuning according to Isabelle/ML conventions;
wenzelm
parents: 30207
diff changeset
    96
                  Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
32790
a7b92f98180b handle Type.TYPE_MATCH, not arbitrary exceptions;
wenzelm
parents: 31687
diff changeset
    97
              in SOME sub_size end handle Type.TYPE_MATCH => NONE
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    98
          end
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
    99
      | make_match (Loose arg) =
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   100
          check_const (matches_subtype thy (make_pattern arg) o snd)
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   101
      | make_match (Name arg) = check_const (match_string arg o fst);
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   102
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   103
    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
   104
    val criteria = map make_criterion raw_criteria;
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   105
30206
48507466d9d2 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents: 30190
diff changeset
   106
    val consts = Sign.consts_of thy;
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 52703
diff changeset
   107
    val {constants, ...} = Consts.dest consts;
31684
d5d830979a54 minor tuning according to Isabelle/ML conventions;
wenzelm
parents: 30207
diff changeset
   108
    fun eval_entry c =
46979
ef4b0d6b2fb6 sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents: 46961
diff changeset
   109
      fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   110
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
   111
    val matches =
56062
8ae2965ddc80 tuned signature;
wenzelm
parents: 56025
diff changeset
   112
      fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58928
diff changeset
   113
      |> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst))
46979
ef4b0d6b2fb6 sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents: 46961
diff changeset
   114
      |> map (apsnd fst o snd);
56912
293cd4dcfebc some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56908
diff changeset
   115
293cd4dcfebc some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56908
diff changeset
   116
    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   117
  in
56891
48899c43b07d tuned message -- more context for detached window etc.;
wenzelm
parents: 56763
diff changeset
   118
    Pretty.block
56912
293cd4dcfebc some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56908
diff changeset
   119
      (Pretty.fbreaks
293cd4dcfebc some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56908
diff changeset
   120
        (Pretty.mark position_markup (Pretty.keyword1 "find_consts") ::
293cd4dcfebc some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents: 56908
diff changeset
   121
          map pretty_criterion raw_criteria)) ::
38335
630f379f2660 misc tuning and simplification;
wenzelm
parents: 38334
diff changeset
   122
    Pretty.str "" ::
56908
734f7e6151c9 tuned message: more compact, imitate actual command line;
wenzelm
parents: 56891
diff changeset
   123
    (if null matches then [Pretty.str "found nothing"]
734f7e6151c9 tuned message: more compact, imitate actual command line;
wenzelm
parents: 56891
diff changeset
   124
     else
734f7e6151c9 tuned message: more compact, imitate actual command line;
wenzelm
parents: 56891
diff changeset
   125
       Pretty.str ("found " ^ string_of_int (length matches) ^ " constant(s):") ::
734f7e6151c9 tuned message: more compact, imitate actual command line;
wenzelm
parents: 56891
diff changeset
   126
       grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches)
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   127
  end |> Pretty.fbreaks |> curry Pretty.blk 0;
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   128
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   129
fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   130
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
   131
30143
98a986b02022 observe basic Isabelle/ML coding conventions;
wenzelm
parents: 30142
diff changeset
   132
(* 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
   133
38334
c677c2c1d333 simplified/unified command setup;
wenzelm
parents: 36953
diff changeset
   134
local
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
   135
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29895
diff changeset
   136
val criterion =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 35845
diff changeset
   137
  Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 35845
diff changeset
   138
  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 35845
diff changeset
   139
  Parse.xname >> Loose;
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
   140
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   141
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   142
59934
b65c4370f831 more position information and PIDE markup for command keywords;
wenzelm
parents: 59083
diff changeset
   143
val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
58905
55160ef37e8f more frugal keywords;
wenzelm
parents: 58903
diff changeset
   144
38334
c677c2c1d333 simplified/unified command setup;
wenzelm
parents: 36953
diff changeset
   145
in
c677c2c1d333 simplified/unified command setup;
wenzelm
parents: 36953
diff changeset
   146
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   147
fun read_query pos str =
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59058
diff changeset
   148
  Token.explode query_keywords pos str
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   149
  |> filter Token.is_proper
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   150
  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   151
  |> #1;
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   152
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
   153
val _ =
58893
9e0ecb66d6a7 eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents: 57918
diff changeset
   154
  Outer_Syntax.command @{command_spec "find_consts"}
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   155
    "find constants by name / type patterns"
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   156
    (query >> (fn spec =>
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   157
      Toplevel.keep (fn st =>
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   158
        Pretty.writeln (pretty_consts (Toplevel.context_of st) spec))));
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
   159
29884
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   160
end;
74c183927054 added ML file for the find_consts command
kleing
parents:
diff changeset
   161
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   162
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   163
(* PIDE query operation *)
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   164
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   165
val _ =
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   166
  Query_Operation.register "find_consts" (fn {state, args, output_result} =>
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   167
    (case try Toplevel.context_of state of
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   168
      SOME ctxt =>
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   169
        let
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   170
          val [query_arg] = args;
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   171
          val query = read_query Position.none query_arg;
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   172
        in output_result (Pretty.string_of (pretty_consts ctxt query)) end
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   173
    | NONE => error "Unknown context"));
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56062
diff changeset
   174
38334
c677c2c1d333 simplified/unified command setup;
wenzelm
parents: 36953
diff changeset
   175
end;
c677c2c1d333 simplified/unified command setup;
wenzelm
parents: 36953
diff changeset
   176