conceal consts via name space, not tags;
authorwenzelm
Sun Oct 25 13:18:35 2009 +0100 (2009-10-25)
changeset 331586e3dc0ba2b06
parent 33157 56f836b9414f
child 33161 165a9f490d98
conceal consts via name space, not tags;
src/HOL/Tools/res_axioms.ML
src/Pure/General/markup.ML
src/Pure/Tools/find_consts.ML
src/Pure/consts.ML
src/Pure/display.ML
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Oct 25 12:27:21 2009 +0100
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Oct 25 13:18:35 2009 +0100
     1.3 @@ -85,7 +85,7 @@
     1.4              val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
     1.5                      (*Forms a lambda-abstraction over the formal parameters*)
     1.6              val (c, thy') =
     1.7 -              Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy
     1.8 +              Sign.declare_const [] ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
     1.9              val cdef = cname ^ "_def"
    1.10              val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
    1.11              val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
     2.1 --- a/src/Pure/General/markup.ML	Sun Oct 25 12:27:21 2009 +0100
     2.2 +++ b/src/Pure/General/markup.ML	Sun Oct 25 13:18:35 2009 +0100
     2.3 @@ -17,7 +17,6 @@
     2.4    val theory_nameN: string
     2.5    val kindN: string
     2.6    val internalK: string
     2.7 -  val property_internal: Properties.property
     2.8    val entityN: string val entity: string -> T
     2.9    val defN: string
    2.10    val refN: string
    2.11 @@ -161,7 +160,6 @@
    2.12  val kindN = "kind";
    2.13  
    2.14  val internalK = "internal";
    2.15 -val property_internal = (kindN, internalK);
    2.16  
    2.17  
    2.18  (* formal entities *)
     3.1 --- a/src/Pure/Tools/find_consts.ML	Sun Oct 25 12:27:21 2009 +0100
     3.2 +++ b/src/Pure/Tools/find_consts.ML	Sun Oct 25 13:18:35 2009 +0100
     3.3 @@ -87,9 +87,8 @@
     3.4      val thy = ProofContext.theory_of ctxt;
     3.5      val low_ranking = 10000;
     3.6  
     3.7 -    fun not_internal consts (nm, _) =
     3.8 -      if member (op =) (Consts.the_tags consts nm) Markup.property_internal
     3.9 -      then NONE else SOME low_ranking;
    3.10 +    fun user_visible consts (nm, _) =
    3.11 +      if Consts.is_concealed consts nm then NONE else SOME low_ranking;
    3.12  
    3.13      fun make_pattern crit =
    3.14        let
    3.15 @@ -119,7 +118,7 @@
    3.16      val consts = Sign.consts_of thy;
    3.17      val (_, consts_tab) = #constants (Consts.dest consts);
    3.18      fun eval_entry c =
    3.19 -      fold filter_const (not_internal consts :: criteria)
    3.20 +      fold filter_const (user_visible consts :: criteria)
    3.21          (SOME (c, low_ranking));
    3.22  
    3.23      val matches =
     4.1 --- a/src/Pure/consts.ML	Sun Oct 25 12:27:21 2009 +0100
     4.2 +++ b/src/Pure/consts.ML	Sun Oct 25 13:18:35 2009 +0100
     4.3 @@ -20,6 +20,7 @@
     4.4    val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
     4.5    val the_constraint: T -> string -> typ                       (*exception TYPE*)
     4.6    val space_of: T -> Name_Space.T
     4.7 +  val is_concealed: T -> string -> bool
     4.8    val intern: T -> xstring -> string
     4.9    val extern: T -> string -> xstring
    4.10    val extern_early: T -> string -> xstring
    4.11 @@ -123,6 +124,8 @@
    4.12  
    4.13  fun space_of (Consts {decls = (space, _), ...}) = space;
    4.14  
    4.15 +val is_concealed = Name_Space.is_concealed o space_of;
    4.16 +
    4.17  val intern = Name_Space.intern o space_of;
    4.18  val extern = Name_Space.extern o space_of;
    4.19  
     5.1 --- a/src/Pure/display.ML	Sun Oct 25 12:27:21 2009 +0100
     5.2 +++ b/src/Pure/display.ML	Sun Oct 25 13:18:35 2009 +0100
     5.3 @@ -188,8 +188,7 @@
     5.4      val tdecls = Name_Space.dest_table types;
     5.5      val arties = Name_Space.dest_table (Sign.type_space thy, arities);
     5.6  
     5.7 -    fun prune_const c = not verbose andalso
     5.8 -      member (op =) (Consts.the_tags consts c) Markup.property_internal;
     5.9 +    fun prune_const c = not verbose andalso Consts.is_concealed consts c;
    5.10      val cnsts = Name_Space.extern_table (#1 constants,
    5.11        Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
    5.12