src/Pure/Tools/find_consts.ML
changeset 30206 48507466d9d2
parent 30190 479806475f3c
child 30207 c56d27155041
     1.1 --- a/src/Pure/Tools/find_consts.ML	Mon Mar 02 20:31:27 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Mar 02 18:11:39 2009 +1100
     1.3 @@ -12,8 +12,6 @@
     1.4      | Loose of string
     1.5      | Name of string
     1.6  
     1.7 -  val default_criteria : (bool * criterion) list ref
     1.8 -
     1.9    val find_consts : Proof.context -> (bool * criterion) list -> unit
    1.10  end;
    1.11  
    1.12 @@ -27,9 +25,6 @@
    1.13    | Loose of string
    1.14    | Name of string;
    1.15  
    1.16 -val default_criteria = ref [(false, Name ".sko_")];
    1.17 -
    1.18 -
    1.19  (* matching types/consts *)
    1.20  
    1.21  fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
    1.22 @@ -54,8 +49,8 @@
    1.23    if is_some (f c)
    1.24    then NONE else SOME (Term.size_of_typ ty);
    1.25  
    1.26 -fun filter_const (_, NONE) = NONE
    1.27 -  | filter_const (f, (SOME (c, r))) =
    1.28 +fun filter_const _ NONE = NONE
    1.29 +  | filter_const f (SOME (c, r)) =
    1.30        Option.map (pair c o (curry Int.min r)) (f c);
    1.31  
    1.32  
    1.33 @@ -81,7 +76,6 @@
    1.34        Pretty.quote (Syntax.pretty_typ ctxt ty')]
    1.35    end;
    1.36  
    1.37 -
    1.38  (* find_consts *)
    1.39  
    1.40  fun find_consts ctxt raw_criteria =
    1.41 @@ -91,7 +85,11 @@
    1.42      val thy = ProofContext.theory_of ctxt;
    1.43      val low_ranking = 10000;
    1.44  
    1.45 -    fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) |> Term.type_of;
    1.46 +    fun not_internal consts (nm, _) = 
    1.47 +      if member (op =) (Consts.the_tags consts nm) Markup.property_internal
    1.48 +      then NONE else SOME low_ranking;
    1.49 +
    1.50 +    fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) |> type_of;
    1.51  
    1.52      fun make_match (Strict arg) =
    1.53            let val qty = make_pattern arg; in
    1.54 @@ -108,13 +106,15 @@
    1.55        | make_match (Name arg) = check_const (match_string arg o fst);
    1.56  
    1.57      fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
    1.58 -    val criteria = map make_criterion (! default_criteria @ raw_criteria);
    1.59 +    val criteria = map make_criterion raw_criteria;
    1.60  
    1.61 -    val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
    1.62 -    fun eval_entry c = List.foldl filter_const (SOME (c, low_ranking)) criteria;
    1.63 +    val consts = Sign.consts_of thy;
    1.64 +    val (_, consts_tab) = (#constants o Consts.dest) consts;
    1.65 +    fun eval_entry c = fold filter_const (not_internal consts::criteria)
    1.66 +                                         (SOME (c, low_ranking));
    1.67  
    1.68      val matches =
    1.69 -      Symtab.fold (cons o eval_entry) consts []
    1.70 +      Symtab.fold (cons o eval_entry) consts_tab []
    1.71        |> map_filter I
    1.72        |> sort (rev_order o int_ord o pairself snd)
    1.73        |> map ((apsnd fst) o fst);
    1.74 @@ -132,7 +132,7 @@
    1.75        :: map (pretty_const ctxt) matches
    1.76      |> Pretty.chunks
    1.77      |> Pretty.writeln
    1.78 -  end handle ERROR s => Output.error_msg s;
    1.79 +  end;
    1.80  
    1.81  
    1.82  (* command syntax *)