equal
deleted
inserted
replaced
67 |
67 |
68 (* find_consts *) |
68 (* find_consts *) |
69 |
69 |
70 fun find_consts ctxt raw_criteria = |
70 fun find_consts ctxt raw_criteria = |
71 let |
71 let |
72 val start = Timing.start (); |
|
73 |
|
74 val thy = Proof_Context.theory_of ctxt; |
72 val thy = Proof_Context.theory_of ctxt; |
75 val low_ranking = 10000; |
73 val low_ranking = 10000; |
76 |
74 |
77 fun user_visible consts (nm, _) = |
75 fun user_visible consts (nm, _) = |
78 if Consts.is_concealed consts nm then NONE else SOME low_ranking; |
76 if Consts.is_concealed consts nm then NONE else SOME low_ranking; |
111 val matches = |
109 val matches = |
112 Symtab.fold (cons o eval_entry) consts_tab [] |
110 Symtab.fold (cons o eval_entry) consts_tab [] |
113 |> map_filter I |
111 |> map_filter I |
114 |> sort (rev_order o int_ord o pairself snd) |
112 |> sort (rev_order o int_ord o pairself snd) |
115 |> map (apsnd fst o fst); |
113 |> map (apsnd fst o fst); |
116 |
|
117 val end_msg = " in " ^ Timing.message (Timing.result start); |
|
118 in |
114 in |
119 Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) :: |
115 Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) :: |
120 Pretty.str "" :: |
116 Pretty.str "" :: |
121 Pretty.str |
117 Pretty.str |
122 (if null matches |
118 (if null matches |
123 then "nothing found" ^ end_msg |
119 then "nothing found" |
124 else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") :: |
120 else "found " ^ string_of_int (length matches) ^ " constant(s):") :: |
125 Pretty.str "" :: |
121 Pretty.str "" :: |
126 map (pretty_const ctxt) matches |
122 map (pretty_const ctxt) matches |
127 end |> Pretty.chunks |> Pretty.writeln; |
123 end |> Pretty.chunks |> Pretty.writeln; |
128 |
124 |
129 |
125 |