src/Pure/Isar/theory_target.ML
changeset 25607 779c79c36c5e
parent 25597 34860182b250
child 25684 2b3cce7d22b8
     1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Dec 11 10:23:13 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Dec 11 10:23:14 2007 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4  
     1.5  (* pretty *)
     1.6  
     1.7 -fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
     1.8 +fun pretty_thy ctxt target is_locale is_class =
     1.9    let
    1.10      val thy = ProofContext.theory_of ctxt;
    1.11      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    1.12 @@ -53,14 +53,19 @@
    1.13      val elems =
    1.14        (if null fixes then [] else [Element.Fixes fixes]) @
    1.15        (if null assumes then [] else [Element.Assumes assumes]);
    1.16 -  in
    1.17 -    Pretty.block [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy)] ::
    1.18 -     (if target = "" then []
    1.19 -      else if null elems then [Pretty.str target_name]
    1.20 -      else [Pretty.big_list (target_name ^ " =")
    1.21 -        (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)])
    1.22 +  in if target = "" then []
    1.23 +    else if null elems then [Pretty.str target_name]
    1.24 +    else [Pretty.big_list (target_name ^ " =")
    1.25 +      (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
    1.26    end;
    1.27  
    1.28 +fun pretty (Target {target, is_locale, is_class, instantiation, overloading}) ctxt =
    1.29 +  Pretty.block [Pretty.str "theory", Pretty.brk 1,
    1.30 +      Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
    1.31 +    (if not (null overloading) then [Overloading.pretty ctxt]
    1.32 +    else if not (null (#1 instantiation)) then [Class.pretty_instantiation ctxt]
    1.33 +    else pretty_thy ctxt target is_locale is_class);
    1.34 +
    1.35  
    1.36  (* target declarations *)
    1.37  
    1.38 @@ -215,7 +220,7 @@
    1.39    in
    1.40      lthy'
    1.41      |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default pos ((c, mx2), t))
    1.42 -    |> is_class ? class_target ta (Class.logical_const target pos ((c, mx1), t))
    1.43 +    |> is_class ? class_target ta (Class.declare target pos ((c, mx1), t))
    1.44      |> LocalDefs.add_def ((c, NoSyn), t)
    1.45    end;
    1.46  
    1.47 @@ -241,7 +246,7 @@
    1.48          #-> (fn (lhs, _) =>
    1.49            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.50              term_syntax ta (locale_const ta prmode pos ((c, mx2), lhs')) #>
    1.51 -            is_class ? class_target ta (Class.syntactic_const target prmode pos ((c, mx1), t'))
    1.52 +            is_class ? class_target ta (Class.abbrev target prmode pos ((c, mx1), t'))
    1.53            end)
    1.54        else
    1.55          LocalTheory.theory
    1.56 @@ -363,9 +368,16 @@
    1.57  
    1.58  val instantiation = init_lthy_ctxt o init_instantiation;
    1.59  
    1.60 -fun gen_overloading prep_operation operations thy =
    1.61 -  thy
    1.62 -  |> init_lthy_ctxt (init_overloading (map (prep_operation thy) operations));
    1.63 +fun gen_overloading prep_operation raw_operations thy =
    1.64 +  let
    1.65 +    val check_const = dest_Const o Syntax.check_term (ProofContext.init thy) o Const;
    1.66 +    val operations = raw_operations
    1.67 +      |> map (prep_operation thy)
    1.68 +      |> (map o apfst) check_const;
    1.69 +  in
    1.70 +    thy
    1.71 +    |> init_lthy_ctxt (init_overloading operations)
    1.72 +  end;
    1.73  
    1.74  val overloading = gen_overloading (K I);
    1.75  val overloading_cmd = gen_overloading (fn thy => fn (((raw_c, rawT), v), checked) =>