src/Pure/Isar/theory_target.ML
changeset 25542 ced4104f6c1f
parent 25519 8570745cb40b
child 25597 34860182b250
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Dec 05 14:16:13 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Dec 05 14:16:14 2007 +0100
     1.3 @@ -2,18 +2,18 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Common theory/locale/class/instantiation targets.
     1.8 +Common theory/locale/class/instantiation/overloading targets.
     1.9  *)
    1.10  
    1.11  signature THEORY_TARGET =
    1.12  sig
    1.13    val peek: local_theory -> {target: string, is_locale: bool,
    1.14 -    is_class: bool, instantiation: arity list,
    1.15 +    is_class: bool, instantiation: string list * sort list * sort,
    1.16      overloading: ((string * typ) * (string * bool)) list}
    1.17    val init: string option -> theory -> local_theory
    1.18    val begin: string -> Proof.context -> local_theory
    1.19    val context: xstring -> theory -> local_theory
    1.20 -  val instantiation: arity list -> theory -> local_theory
    1.21 +  val instantiation: string list * sort list * sort -> theory -> local_theory
    1.22    val overloading: ((string * typ) * (string * bool)) list -> theory -> local_theory
    1.23    val overloading_cmd: (((xstring * xstring) * string) * bool) list -> theory -> local_theory
    1.24  end;
    1.25 @@ -24,13 +24,14 @@
    1.26  (* context data *)
    1.27  
    1.28  datatype target = Target of {target: string, is_locale: bool,
    1.29 -  is_class: bool, instantiation: arity list, overloading: ((string * typ) * (string * bool)) list};
    1.30 +  is_class: bool, instantiation: string list * sort list * sort,
    1.31 +  overloading: ((string * typ) * (string * bool)) list};
    1.32  
    1.33  fun make_target target is_locale is_class instantiation overloading =
    1.34    Target {target = target, is_locale = is_locale,
    1.35      is_class = is_class, instantiation = instantiation, overloading = overloading};
    1.36  
    1.37 -val global_target = make_target "" false false [] [];
    1.38 +val global_target = make_target "" false false ([], [], []) [];
    1.39  
    1.40  structure Data = ProofDataFun
    1.41  (
    1.42 @@ -43,7 +44,7 @@
    1.43  
    1.44  (* pretty *)
    1.45  
    1.46 -fun pretty (Target {target, is_locale, is_class, instantiation, overloading}) ctxt =
    1.47 +fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
    1.48    let
    1.49      val thy = ProofContext.theory_of ctxt;
    1.50      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    1.51 @@ -321,20 +322,21 @@
    1.52  local
    1.53  
    1.54  fun init_target _ NONE = global_target
    1.55 -  | init_target thy (SOME target) = make_target target true (Class.is_class thy target) [] [];
    1.56 +  | init_target thy (SOME target) = make_target target true (Class.is_class thy target)
    1.57 +      ([], [], []) [];
    1.58  
    1.59  fun init_instantiation arities = make_target "" false false arities [];
    1.60  
    1.61 -fun init_overloading operations = make_target "" false false [] operations;
    1.62 +fun init_overloading operations = make_target "" false false ([], [], []) operations;
    1.63  
    1.64  fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
    1.65 -  if not (null instantiation) then Class.init_instantiation instantiation
    1.66 +  if (not o null o #1) instantiation then Class.init_instantiation instantiation
    1.67    else if not (null overloading) then Overloading.init overloading
    1.68    else if not is_locale then ProofContext.init
    1.69    else if not is_class then Locale.init target
    1.70    else Class.init target;
    1.71  
    1.72 -fun init_lthy (ta as Target {target, instantiation, ...}) =
    1.73 +fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
    1.74    Data.put ta #>
    1.75    LocalTheory.init (NameSpace.base target)
    1.76     {pretty = pretty ta,
    1.77 @@ -346,8 +348,9 @@
    1.78      term_syntax = term_syntax ta,
    1.79      declaration = declaration ta,
    1.80      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
    1.81 -    exit = if null instantiation then LocalTheory.target_of
    1.82 -      else Class.conclude_instantiation #> LocalTheory.target_of}
    1.83 +    exit = (if (not o null o #1) instantiation then Class.conclude_instantiation
    1.84 +      else if not (null overloading) then Overloading.conclude
    1.85 +      else I) #> LocalTheory.target_of}
    1.86  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
    1.87  
    1.88  in