src/Pure/Isar/local_theory.ML
changeset 26131 91024979b9eb
parent 25984 da0399c9ffcb
child 28017 4919bd124a58
     1.1 --- a/src/Pure/Isar/local_theory.ML	Mon Feb 25 16:31:18 2008 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Mon Feb 25 16:31:19 2008 +0100
     1.3 @@ -10,6 +10,10 @@
     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 -> Markup.property list
     1.9 +  val group_position_of: local_theory -> Markup.property list
    1.10 +  val set_group: string -> local_theory -> local_theory
    1.11    val target_of: local_theory -> Proof.context
    1.12    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    1.13    val raw_theory: (theory -> theory) -> local_theory -> local_theory
    1.14 @@ -24,26 +28,14 @@
    1.15    val axioms: string ->
    1.16      ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    1.17      -> (term list * (bstring * thm list) list) * local_theory
    1.18 -  val axioms_grouped: string -> string ->
    1.19 -    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    1.20 -    -> (term list * (bstring * thm list) list) * local_theory
    1.21    val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
    1.22      (term * term) * local_theory
    1.23    val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.24      (term * (bstring * thm)) * local_theory
    1.25 -  val define_grouped: string -> string ->
    1.26 -    (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.27 -    (term * (bstring * thm)) * local_theory
    1.28    val note: string -> (bstring * Attrib.src list) * thm list ->
    1.29      local_theory -> (bstring * thm list) * local_theory
    1.30    val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.31      local_theory -> (bstring * thm list) list * local_theory
    1.32 -  val note_grouped: string -> string ->
    1.33 -    (bstring * Attrib.src list) * thm list ->
    1.34 -    local_theory -> (bstring * thm list) * local_theory
    1.35 -  val notes_grouped: string -> string ->
    1.36 -    ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.37 -    local_theory -> (bstring * thm list) list * local_theory
    1.38    val type_syntax: declaration -> local_theory -> local_theory
    1.39    val term_syntax: declaration -> local_theory -> local_theory
    1.40    val declaration: declaration -> local_theory -> local_theory
    1.41 @@ -64,14 +56,14 @@
    1.42  
    1.43  type operations =
    1.44   {pretty: local_theory -> Pretty.T list,
    1.45 -  axioms: string -> string ->
    1.46 +  axioms: string ->
    1.47      ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    1.48      -> (term list * (bstring * thm list) list) * local_theory,
    1.49    abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
    1.50 -  define: string -> string ->
    1.51 +  define: string ->
    1.52      (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.53      (term * (bstring * thm)) * local_theory,
    1.54 -  notes: string -> string ->
    1.55 +  notes: string ->
    1.56      ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.57      local_theory -> (bstring * thm list) list * local_theory,
    1.58    type_syntax: declaration -> local_theory -> local_theory,
    1.59 @@ -81,12 +73,13 @@
    1.60    exit: local_theory -> Proof.context};
    1.61  
    1.62  datatype lthy = LThy of
    1.63 - {theory_prefix: string,
    1.64 + {group: string,
    1.65 +  theory_prefix: string,
    1.66    operations: operations,
    1.67    target: Proof.context};
    1.68  
    1.69 -fun make_lthy (theory_prefix, operations, target) =
    1.70 -  LThy {theory_prefix = theory_prefix, operations = operations, target = target};
    1.71 +fun make_lthy (group, theory_prefix, operations, target) =
    1.72 +  LThy {group = group, theory_prefix = theory_prefix, operations = operations, target = target};
    1.73  
    1.74  
    1.75  (* context data *)
    1.76 @@ -103,14 +96,33 @@
    1.77    | SOME (LThy data) => data);
    1.78  
    1.79  fun map_lthy f lthy =
    1.80 -  let val {theory_prefix, operations, target} = get_lthy lthy
    1.81 -  in Data.put (SOME (make_lthy (f (theory_prefix, operations, target)))) lthy end;
    1.82 +  let val {group, theory_prefix, operations, target} = get_lthy lthy
    1.83 +  in Data.put (SOME (make_lthy (f (group, theory_prefix, operations, target)))) lthy end;
    1.84 +
    1.85 +
    1.86 +(* group *)
    1.87 +
    1.88 +val group_of = #group o get_lthy;
    1.89 +
    1.90 +fun group_properties_of lthy =
    1.91 +  (case group_of lthy of
    1.92 +    "" => []
    1.93 +  | group => [(Markup.groupN, group)]);
    1.94 +
    1.95 +fun group_position_of lthy =
    1.96 +  group_properties_of lthy @ Position.properties_of (Position.thread_data ());
    1.97 +
    1.98 +fun set_group group = map_lthy (fn (_, theory_prefix, operations, target) =>
    1.99 +  (group, theory_prefix, operations, target));
   1.100 +
   1.101 +
   1.102 +(* target *)
   1.103  
   1.104  val target_of = #target o get_lthy;
   1.105  val affirm = tap target_of;
   1.106  
   1.107 -fun map_target f = map_lthy (fn (theory_prefix, operations, target) =>
   1.108 -  (theory_prefix, operations, f target));
   1.109 +fun map_target f = map_lthy (fn (group, theory_prefix, operations, target) =>
   1.110 +  (group, theory_prefix, operations, f target));
   1.111  
   1.112  
   1.113  (* substructure mappings *)
   1.114 @@ -142,7 +154,7 @@
   1.115  
   1.116  fun target_result f lthy =
   1.117    let
   1.118 -    val (res, ctxt') = f (#target (get_lthy lthy));
   1.119 +    val (res, ctxt') = f (target_of lthy);
   1.120      val thy' = ProofContext.theory_of ctxt';
   1.121      val lthy' = lthy
   1.122        |> map_target (K ctxt')
   1.123 @@ -156,25 +168,18 @@
   1.124  
   1.125  fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
   1.126  fun operation1 f x = operation (fn ops => f ops x);
   1.127 -fun operation2 f x y = operation (fn ops => f ops x y);
   1.128 -fun operation3 f x y z = operation (fn ops => f ops x y z);
   1.129 +fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
   1.130  
   1.131  val pretty = operation #pretty;
   1.132 -val axioms_grouped = operation3 #axioms;
   1.133 +val axioms = operation2 #axioms;
   1.134  val abbrev = operation2 #abbrev;
   1.135 -val define_grouped = operation3 #define;
   1.136 -val notes_grouped = operation3 #notes;
   1.137 +val define = operation2 #define;
   1.138 +val notes = operation2 #notes;
   1.139  val type_syntax = operation1 #type_syntax;
   1.140  val term_syntax = operation1 #term_syntax;
   1.141  val declaration = operation1 #declaration;
   1.142  
   1.143 -fun note_grouped kind group (a, ths) lthy = lthy
   1.144 -  |> notes_grouped kind group [(a, [(ths, [])])] |>> the_single;
   1.145 -
   1.146 -fun axioms kind = axioms_grouped kind "";
   1.147 -fun define kind = define_grouped kind "";
   1.148 -fun notes kind = notes_grouped kind "";
   1.149 -fun note kind = note_grouped kind "";
   1.150 +fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
   1.151  
   1.152  fun target_morphism lthy =
   1.153    ProofContext.export_morphism lthy (target_of lthy) $>
   1.154 @@ -188,11 +193,11 @@
   1.155  (* init -- exit *)
   1.156  
   1.157  fun init theory_prefix operations target = target |> Data.map
   1.158 -  (fn NONE => SOME (make_lthy (theory_prefix, operations, target))
   1.159 +  (fn NONE => SOME (make_lthy ("", theory_prefix, operations, target))
   1.160      | SOME _ => error "Local theory already initialized");
   1.161  
   1.162  fun restore lthy =
   1.163 -  let val {theory_prefix, operations, target} = get_lthy lthy
   1.164 +  let val {group = _, theory_prefix, operations, target} = get_lthy lthy
   1.165    in init theory_prefix operations target end;
   1.166  
   1.167  val reinit = operation #reinit;