more markup -- avoid old Locale.extern;
authorwenzelm
Fri Aug 16 20:58:15 2013 +0200 (2013-08-16)
changeset 53041d51bac27d4a0
parent 53040 e6edd7abc4ce
child 53042 aa0322a65bea
more markup -- avoid old Locale.extern;
removed obsolete Locale.intern -- prefer Locale.check;
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Aug 16 19:03:31 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Aug 16 20:58:15 2013 +0200
     1.3 @@ -89,6 +89,8 @@
     1.4  
     1.5  fun parameters_of thy strict (expr, fixed) =
     1.6    let
     1.7 +    val ctxt = Proof_Context.init_global thy;
     1.8 +
     1.9      fun reject_dups message xs =
    1.10        (case duplicates (op =) xs of
    1.11          [] => ()
    1.12 @@ -103,16 +105,18 @@
    1.13              val ps = params_loc loc;
    1.14              val d = length ps - length insts;
    1.15              val insts' =
    1.16 -              if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
    1.17 -                quote (Locale.extern thy loc))
    1.18 +              if d < 0 then
    1.19 +                error ("More arguments than parameters in instantiation of locale " ^
    1.20 +                  quote (Locale.markup_name ctxt loc))
    1.21                else insts @ replicate d NONE;
    1.22              val ps' = (ps ~~ insts') |>
    1.23                map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
    1.24            in (ps', (loc, (prfx, Positional insts'))) end
    1.25        | params_inst (loc, (prfx, Named insts)) =
    1.26            let
    1.27 -            val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
    1.28 -              (map fst insts);
    1.29 +            val _ =
    1.30 +              reject_dups "Duplicate instantiation of the following parameter(s): "
    1.31 +                (map fst insts);
    1.32              val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
    1.33                if AList.defined (op =) ps p then AList.delete (op =) p ps
    1.34                else error (quote p ^ " not a parameter of instantiated expression"));
     2.1 --- a/src/Pure/Isar/locale.ML	Fri Aug 16 19:03:31 2013 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Fri Aug 16 20:58:15 2013 +0200
     2.3 @@ -36,9 +36,9 @@
     2.4      declaration list ->
     2.5      (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
     2.6      (string * morphism) list -> theory -> theory
     2.7 -  val intern: theory -> xstring -> string
     2.8    val check: theory -> xstring * Position.T -> string
     2.9    val extern: theory -> string -> xstring
    2.10 +  val markup_name: Proof.context -> string -> string
    2.11    val pretty_name: Proof.context -> string -> Pretty.T
    2.12    val defined: theory -> string -> bool
    2.13    val params_of: theory -> string -> ((string * typ) * mixfix) list
    2.14 @@ -159,13 +159,15 @@
    2.15    val merge = Name_Space.join_tables (K merge_locale);
    2.16  );
    2.17  
    2.18 -val intern = Name_Space.intern o #1 o Locales.get;
    2.19  fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy);
    2.20 +
    2.21  fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
    2.22  
    2.23 -fun pretty_name ctxt name =
    2.24 -  Pretty.mark_str
    2.25 -    (Name_Space.markup_extern ctxt (#1 (Locales.get (Proof_Context.theory_of ctxt))) name);
    2.26 +fun markup_extern ctxt =
    2.27 +  Name_Space.markup_extern ctxt (#1 (Locales.get (Proof_Context.theory_of ctxt)));
    2.28 +
    2.29 +fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup;
    2.30 +fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str;
    2.31  
    2.32  val get_locale = Symtab.lookup o #2 o Locales.get;
    2.33  val defined = Symtab.defined o #2 o Locales.get;
    2.34 @@ -207,7 +209,7 @@
    2.35  fun mixins_of thy name serial = the_locale thy name |>
    2.36    #mixins |> lookup_mixins serial;
    2.37  
    2.38 -(* FIXME unused *)
    2.39 +(* FIXME unused!? *)
    2.40  fun identity_on thy name morph =
    2.41    let val mk_instance = instance_of thy name
    2.42    in ListPair.all Term.aconv_untyped (mk_instance Morphism.identity, mk_instance morph) end;
    2.43 @@ -462,15 +464,18 @@
    2.44  fun amend_registration (name, morph) mixin export context =
    2.45    let
    2.46      val thy = Context.theory_of context;
    2.47 +    val ctxt = Context.proof_of context;
    2.48 +
    2.49      val regs = Registrations.get context |> fst;
    2.50      val base = instance_of thy name (morph $> export);
    2.51 -    val serial' = case Idtab.lookup regs (name, base) of
    2.52 +    val serial' =
    2.53 +      (case Idtab.lookup regs (name, base) of
    2.54          NONE =>
    2.55 -          error ("No interpretation of locale " ^
    2.56 -            quote (extern thy name) ^ " with\nparameter instantiation " ^
    2.57 +          error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
    2.58 +            " with\nparameter instantiation " ^
    2.59              space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
    2.60              " available")
    2.61 -      | SOME (_, serial') => serial';
    2.62 +      | SOME (_, serial') => serial');
    2.63    in
    2.64      add_mixin serial' mixin context
    2.65    end;
    2.66 @@ -502,7 +507,7 @@
    2.67  
    2.68  (*** Dependencies ***)
    2.69  
    2.70 -(*
    2.71 +(* FIXME dead code!?
    2.72  fun amend_dependency loc (name, morph) mixin export thy =
    2.73    let
    2.74      val deps = dependencies_of thy loc;