tuned: less formal noise in Named_Target, more coherence in Class
authorhaftmann
Fri Aug 20 08:52:01 2010 +0200 (2010-08-20 ago)
changeset 3861925e401d53900
parent 38561 d2a8087effc6
child 38620 b40524b74f77
tuned: less formal noise in Named_Target, more coherence in Class
src/Pure/Isar/class.ML
src/Pure/Isar/named_target.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Aug 19 18:44:26 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Aug 20 08:52:01 2010 +0200
     1.3 @@ -17,9 +17,8 @@
     1.4    val print_classes: theory -> unit
     1.5    val init: class -> theory -> Proof.context
     1.6    val begin: class list -> sort -> Proof.context -> Proof.context
     1.7 -  val const: class -> (binding * mixfix) * (term list * term) -> theory -> theory
     1.8 -  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
     1.9 -  val refresh_syntax: class -> Proof.context -> Proof.context
    1.10 +  val const: class -> (binding * mixfix) * (term list * term) -> local_theory -> local_theory
    1.11 +  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
    1.12    val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    1.13    val class_prefix: string -> string
    1.14    val register: class -> class list -> ((string * typ) * (string * typ)) list
    1.15 @@ -286,12 +285,6 @@
    1.16      |> Overloading.set_primary_constraints
    1.17    end;
    1.18  
    1.19 -fun refresh_syntax class ctxt =
    1.20 -  let
    1.21 -    val thy = ProofContext.theory_of ctxt;
    1.22 -    val base_sort = base_sort thy class;
    1.23 -  in synchronize_class_syntax [class] base_sort ctxt end;
    1.24 -
    1.25  fun redeclare_operations thy sort =
    1.26    fold (redeclare_const thy o fst) (these_operations thy sort);
    1.27  
    1.28 @@ -312,7 +305,15 @@
    1.29  
    1.30  val class_prefix = Logic.const_of_class o Long_Name.base_name;
    1.31  
    1.32 -fun const class ((c, mx), (type_params, dict)) thy =
    1.33 +fun target_extension f class lthy =
    1.34 +  lthy
    1.35 +  |> Local_Theory.raw_theory f
    1.36 +  |> Local_Theory.target (synchronize_class_syntax [class]
    1.37 +      (base_sort (ProofContext.theory_of lthy) class));
    1.38 +
    1.39 +local
    1.40 +
    1.41 +fun target_const class ((c, mx), (type_params, dict)) thy =
    1.42    let
    1.43      val morph = morphism thy class;
    1.44      val b = Morphism.binding morph c;
    1.45 @@ -334,7 +335,7 @@
    1.46      |> Sign.add_const_constraint (c', SOME ty')
    1.47    end;
    1.48  
    1.49 -fun abbrev class prmode ((c, mx), rhs) thy =
    1.50 +fun target_abbrev class prmode ((c, mx), rhs) thy =
    1.51    let
    1.52      val morph = morphism thy class;
    1.53      val unchecks = these_unchecks thy [class];
    1.54 @@ -352,6 +353,13 @@
    1.55      |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
    1.56    end;
    1.57  
    1.58 +in
    1.59 +
    1.60 +fun const class arg = target_extension (target_const class arg) class;
    1.61 +fun abbrev class prmode arg = target_extension (target_abbrev class prmode arg) class;
    1.62 +
    1.63 +end;
    1.64 +
    1.65  
    1.66  (* simple subclasses *)
    1.67  
     2.1 --- a/src/Pure/Isar/named_target.ML	Thu Aug 19 18:44:26 2010 +0200
     2.2 +++ b/src/Pure/Isar/named_target.ML	Fri Aug 20 08:52:01 2010 +0200
     2.3 @@ -88,10 +88,6 @@
     2.4  fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
     2.5    locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
     2.6  
     2.7 -fun class_target (Target {target, ...}) f =
     2.8 -  Local_Theory.raw_theory f #>
     2.9 -  Local_Theory.target (Class.refresh_syntax target);
    2.10 -
    2.11  
    2.12  (* define *)
    2.13  
    2.14 @@ -104,7 +100,7 @@
    2.15      (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    2.16    Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    2.17    #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
    2.18 -    #> class_target ta (Class.const target ((b, mx), (type_params, lhs)))
    2.19 +    #> Class.const target ((b, mx), (type_params, lhs))
    2.20      #> pair (lhs, def))
    2.21  
    2.22  fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
    2.23 @@ -143,7 +139,7 @@
    2.24    if is_locale
    2.25      then lthy
    2.26        |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
    2.27 -      |> is_class ? class_target ta (Class.abbrev target prmode ((b, mx), t'))
    2.28 +      |> is_class ? Class.abbrev target prmode ((b, mx), t')
    2.29      else lthy
    2.30        |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
    2.31