src/Pure/Isar/local_theory.ML
changeset 33166 55f250ef9e31
parent 33157 56f836b9414f
child 33276 f2bc8bc6e73d
     1.1 --- a/src/Pure/Isar/local_theory.ML	Sun Oct 25 19:17:42 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sun Oct 25 19:18:25 2009 +0100
     1.3 @@ -9,22 +9,21 @@
     1.4  signature LOCAL_THEORY =
     1.5  sig
     1.6    type operations
     1.7 -  val group_of: local_theory -> string
     1.8 -  val group_properties_of: local_theory -> Properties.T
     1.9 -  val group_position_of: local_theory -> Properties.T
    1.10 -  val set_group: string -> local_theory -> local_theory
    1.11 +  val affirm: local_theory -> local_theory
    1.12 +  val naming_of: local_theory -> Name_Space.naming
    1.13 +  val full_name: local_theory -> binding -> string
    1.14 +  val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
    1.15 +  val conceal: local_theory -> local_theory
    1.16 +  val set_group: serial -> local_theory -> local_theory
    1.17    val target_of: local_theory -> Proof.context
    1.18    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    1.19    val raw_theory: (theory -> theory) -> local_theory -> local_theory
    1.20    val checkpoint: local_theory -> local_theory
    1.21 -  val full_naming: local_theory -> Name_Space.naming
    1.22 -  val full_name: local_theory -> binding -> string
    1.23    val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    1.24    val theory: (theory -> theory) -> local_theory -> local_theory
    1.25    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
    1.26    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    1.27    val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
    1.28 -  val affirm: local_theory -> local_theory
    1.29    val pretty: local_theory -> Pretty.T list
    1.30    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    1.31      (term * term) * local_theory
    1.32 @@ -71,14 +70,13 @@
    1.33    exit: local_theory -> Proof.context};
    1.34  
    1.35  datatype lthy = LThy of
    1.36 - {group: string,
    1.37 -  conceal: bool,
    1.38 + {naming: Name_Space.naming,
    1.39    theory_prefix: string,
    1.40    operations: operations,
    1.41    target: Proof.context};
    1.42  
    1.43 -fun make_lthy (group, conceal, theory_prefix, operations, target) =
    1.44 -  LThy {group = group, conceal = conceal, theory_prefix = theory_prefix,
    1.45 +fun make_lthy (naming, theory_prefix, operations, target) =
    1.46 +  LThy {naming = naming, theory_prefix = theory_prefix,
    1.47      operations = operations, target = target};
    1.48  
    1.49  
    1.50 @@ -96,33 +94,30 @@
    1.51    | SOME (LThy data) => data);
    1.52  
    1.53  fun map_lthy f lthy =
    1.54 -  let val {group, conceal, theory_prefix, operations, target} = get_lthy lthy
    1.55 -  in Data.put (SOME (make_lthy (f (group, conceal, theory_prefix, operations, target)))) lthy end;
    1.56 +  let val {naming, theory_prefix, operations, target} = get_lthy lthy
    1.57 +  in Data.put (SOME (make_lthy (f (naming, theory_prefix, operations, target)))) lthy end;
    1.58 +
    1.59 +val affirm = tap get_lthy;
    1.60  
    1.61  
    1.62 -(* group *)
    1.63 +(* naming *)
    1.64  
    1.65 -val group_of = #group o get_lthy;
    1.66 +val naming_of = #naming o get_lthy;
    1.67 +val full_name = Name_Space.full_name o naming_of;
    1.68  
    1.69 -fun group_properties_of lthy =
    1.70 -  (case group_of lthy of
    1.71 -    "" => []
    1.72 -  | group => [(Markup.groupN, group)]);
    1.73 +fun map_naming f = map_lthy (fn (naming, theory_prefix, operations, target) =>
    1.74 +  (f naming, theory_prefix, operations, target));
    1.75  
    1.76 -fun group_position_of lthy =
    1.77 -  group_properties_of lthy @ Position.properties_of (Position.thread_data ());
    1.78 -
    1.79 -fun set_group group = map_lthy (fn (_, conceal, theory_prefix, operations, target) =>
    1.80 -  (group, conceal, theory_prefix, operations, target));
    1.81 +val conceal = map_naming Name_Space.conceal;
    1.82 +val set_group = map_naming o Name_Space.set_group;
    1.83  
    1.84  
    1.85  (* target *)
    1.86  
    1.87  val target_of = #target o get_lthy;
    1.88 -val affirm = tap target_of;
    1.89  
    1.90 -fun map_target f = map_lthy (fn (group, conceal, theory_prefix, operations, target) =>
    1.91 -  (group, conceal, theory_prefix, operations, f target));
    1.92 +fun map_target f = map_lthy (fn (naming, theory_prefix, operations, target) =>
    1.93 +  (naming, theory_prefix, operations, f target));
    1.94  
    1.95  
    1.96  (* substructure mappings *)
    1.97 @@ -139,23 +134,12 @@
    1.98  
    1.99  val checkpoint = raw_theory Theory.checkpoint;
   1.100  
   1.101 -fun full_naming lthy =
   1.102 -  let val {conceal, theory_prefix, ...} = get_lthy lthy in
   1.103 -    Sign.naming_of (ProofContext.theory_of lthy)
   1.104 -    |> Name_Space.mandatory_path theory_prefix
   1.105 -    |> conceal ? Name_Space.conceal
   1.106 -  end;
   1.107 -
   1.108 -fun full_name naming = Name_Space.full_name (full_naming naming);
   1.109 -
   1.110 -fun theory_result f lthy = lthy |> raw_theory_result (fn thy =>
   1.111 -  let val {conceal, theory_prefix, ...} = get_lthy lthy in
   1.112 +fun theory_result f lthy =
   1.113 +  lthy |> raw_theory_result (fn thy =>
   1.114      thy
   1.115 -    |> Sign.mandatory_path theory_prefix
   1.116 -    |> conceal ? Sign.conceal
   1.117 +    |> Sign.map_naming (K (naming_of lthy))
   1.118      |> f
   1.119 -    ||> Sign.restore_naming thy
   1.120 -  end);
   1.121 +    ||> Sign.restore_naming thy);
   1.122  
   1.123  fun theory f = #2 o theory_result (f #> pair ());
   1.124  
   1.125 @@ -205,10 +189,16 @@
   1.126  
   1.127  (* init *)
   1.128  
   1.129 -fun init theory_prefix operations target = target |> Data.map
   1.130 -  (fn NONE => SOME (make_lthy ("", false, theory_prefix, operations, target))
   1.131 -    | SOME _ => error "Local theory already initialized")
   1.132 -  |> checkpoint;
   1.133 +fun init theory_prefix operations target =
   1.134 +  let val naming =
   1.135 +    Sign.naming_of (ProofContext.theory_of target)
   1.136 +    |> Name_Space.mandatory_path theory_prefix;
   1.137 +  in
   1.138 +    target |> Data.map
   1.139 +      (fn NONE => SOME (make_lthy (naming, theory_prefix, operations, target))
   1.140 +        | SOME _ => error "Local theory already initialized")
   1.141 +    |> checkpoint
   1.142 +  end;
   1.143  
   1.144  fun restore lthy =
   1.145    let val {theory_prefix, operations, target, ...} = get_lthy lthy