let naming transform binding beforehand -- covering only the "conceal" flag for now;
authorwenzelm
Wed Oct 28 17:36:34 2009 +0100 (2009-10-28 ago)
changeset 33281223ef9bc399a
parent 33280 e3eaeba6ae28
child 33282 c6364889fea5
let naming transform binding beforehand -- covering only the "conceal" flag for now;
export LocalTheory.standard_morphism;
src/Pure/General/name_space.ML
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/General/name_space.ML	Wed Oct 28 16:28:12 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Oct 28 17:36:34 2009 +0100
     1.3 @@ -40,6 +40,7 @@
     1.4    val root_path: naming -> naming
     1.5    val parent_path: naming -> naming
     1.6    val mandatory_path: string -> naming -> naming
     1.7 +  val transform_binding: naming -> binding -> binding
     1.8    val full_name: naming -> binding -> string
     1.9    val external_names: naming -> string -> string list
    1.10    val declare: bool -> naming -> binding -> T -> string * T
    1.11 @@ -254,14 +255,17 @@
    1.12  
    1.13  (* full name *)
    1.14  
    1.15 +fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
    1.16 +  | transform_binding _ = I;
    1.17 +
    1.18  fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
    1.19  
    1.20 -fun name_spec (Naming {conceal = conceal1, path, ...}) binding =
    1.21 +fun name_spec (naming as Naming {path, ...}) raw_binding =
    1.22    let
    1.23 -    val (conceal2, prefix, name) = Binding.dest binding;
    1.24 +    val binding = transform_binding naming raw_binding;
    1.25 +    val (concealed, prefix, name) = Binding.dest binding;
    1.26      val _ = Long_Name.is_qualified name andalso err_bad binding;
    1.27  
    1.28 -    val concealed = conceal1 orelse conceal2;
    1.29      val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
    1.30      val spec2 = if name = "" then [] else [(name, true)];
    1.31      val spec = spec1 @ spec2;
     2.1 --- a/src/Pure/Isar/local_theory.ML	Wed Oct 28 16:28:12 2009 +0100
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Oct 28 17:36:34 2009 +0100
     2.3 @@ -25,6 +25,8 @@
     2.4    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
     2.5    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
     2.6    val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
     2.7 +  val standard_morphism: local_theory -> Proof.context -> morphism
     2.8 +  val target_morphism: local_theory -> morphism
     2.9    val pretty: local_theory -> Pretty.T list
    2.10    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    2.11      (term * term) * local_theory
    2.12 @@ -37,7 +39,6 @@
    2.13    val term_syntax: declaration -> local_theory -> local_theory
    2.14    val declaration: declaration -> local_theory -> local_theory
    2.15    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    2.16 -  val target_morphism: local_theory -> morphism
    2.17    val init: string -> operations -> Proof.context -> local_theory
    2.18    val restore: local_theory -> local_theory
    2.19    val reinit: local_theory -> local_theory
    2.20 @@ -166,6 +167,15 @@
    2.21    Context.proof_map f;
    2.22  
    2.23  
    2.24 +(* morphisms *)
    2.25 +
    2.26 +fun standard_morphism lthy ctxt =
    2.27 +  ProofContext.norm_export_morphism lthy ctxt $>
    2.28 +  Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
    2.29 +
    2.30 +fun target_morphism lthy = standard_morphism lthy (target_of lthy);
    2.31 +
    2.32 +
    2.33  (* basic operations *)
    2.34  
    2.35  fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
    2.36 @@ -182,9 +192,6 @@
    2.37  
    2.38  fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
    2.39  
    2.40 -fun target_morphism lthy =
    2.41 -  ProofContext.norm_export_morphism lthy (target_of lthy);
    2.42 -
    2.43  fun notation add mode raw_args lthy =
    2.44    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
    2.45    in term_syntax (ProofContext.target_notation add mode args) lthy end;
    2.46 @@ -218,14 +225,14 @@
    2.47  fun exit_result f (x, lthy) =
    2.48    let
    2.49      val ctxt = exit lthy;
    2.50 -    val phi = ProofContext.norm_export_morphism lthy ctxt;
    2.51 +    val phi = standard_morphism lthy ctxt;
    2.52    in (f phi x, ctxt) end;
    2.53  
    2.54  fun exit_result_global f (x, lthy) =
    2.55    let
    2.56      val thy = exit_global lthy;
    2.57      val thy_ctxt = ProofContext.init thy;
    2.58 -    val phi = ProofContext.norm_export_morphism lthy thy_ctxt;
    2.59 +    val phi = standard_morphism lthy thy_ctxt;
    2.60    in (f phi x, thy) end;
    2.61  
    2.62  end;