type object = exn (enhance readability);
authorwenzelm
Tue Nov 04 16:17:04 1997 +0100 (1997-11-04)
changeset 41241af16493c57f
parent 4123 9600dd68d35b
child 4125 dc1cf9db1e17
type object = exn (enhance readability);
src/Provers/classical.ML
src/Provers/simplifier.ML
src/Pure/data.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/Pure/thm.ML
     1.1 --- a/src/Provers/classical.ML	Tue Nov 04 15:16:23 1997 +0100
     1.2 +++ b/src/Provers/classical.ML	Tue Nov 04 16:17:04 1997 +0100
     1.3 @@ -26,9 +26,11 @@
     1.4  signature CLASET_THY_DATA =
     1.5  sig
     1.6    val clasetK: string
     1.7 -  exception ClasetData of exn ref
     1.8 -  val thy_data: string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))
     1.9 -  val fix_methods: exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit) -> unit
    1.10 +  exception ClasetData of object ref
    1.11 +  val thy_data: string * (object * (object -> object) *
    1.12 +    (object * object -> object) * (object -> unit))
    1.13 +  val fix_methods: object * (object -> object) *
    1.14 +    (object * object -> object) * (object -> unit) -> unit
    1.15  end;
    1.16  
    1.17  signature CLASSICAL_DATA =
    1.18 @@ -137,15 +139,15 @@
    1.19  (* data kind claset -- forward declaration *)
    1.20  
    1.21  val clasetK = "claset";
    1.22 -exception ClasetData of exn ref;
    1.23 +exception ClasetData of object ref;
    1.24  
    1.25  local
    1.26    fun undef _ = raise Match;
    1.27  
    1.28    val empty_ref = ref ERROR;
    1.29 -  val prep_ext_fn = ref (undef: exn -> exn);
    1.30 -  val merge_fn = ref (undef: exn * exn -> exn);
    1.31 -  val print_fn = ref (undef: exn -> unit);
    1.32 +  val prep_ext_fn = ref (undef: object -> object);
    1.33 +  val merge_fn = ref (undef: object * object -> object);
    1.34 +  val print_fn = ref (undef: object -> unit);
    1.35  
    1.36    val empty = ClasetData empty_ref;
    1.37    fun prep_ext exn = ! prep_ext_fn exn;
     2.1 --- a/src/Provers/simplifier.ML	Tue Nov 04 15:16:23 1997 +0100
     2.2 +++ b/src/Provers/simplifier.ML	Tue Nov 04 16:17:04 1997 +0100
     2.3 @@ -46,7 +46,8 @@
     2.4    val merge_ss:     simpset * simpset -> simpset
     2.5    val prems_of_ss:  simpset -> thm list
     2.6  
     2.7 -  val simpset_thy_data: string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))
     2.8 +  val simpset_thy_data: string * (object * (object -> object) *
     2.9 +    (object * object -> object) * (object -> unit))
    2.10    val simpset_ref_of_sg: Sign.sg -> simpset ref
    2.11    val simpset_ref_of: theory -> simpset ref
    2.12    val simpset_of_sg: Sign.sg -> simpset
     3.1 --- a/src/Pure/data.ML	Tue Nov 04 15:16:23 1997 +0100
     3.2 +++ b/src/Pure/data.ML	Tue Nov 04 16:17:04 1997 +0100
     3.3 @@ -6,6 +6,8 @@
     3.4  constructors.
     3.5  *)
     3.6  
     3.7 +type object = exn;
     3.8 +
     3.9  signature DATA =
    3.10  sig
    3.11    type T
    3.12 @@ -13,9 +15,10 @@
    3.13    val merge: T * T -> T
    3.14    val prep_ext: T -> T
    3.15    val kinds: T -> string list
    3.16 -  val init: T -> string -> exn -> (exn -> exn) -> (exn * exn -> exn) -> (exn -> unit) -> T
    3.17 -  val get: T -> string -> exn
    3.18 -  val put: T -> string -> exn -> T
    3.19 +  val init: T -> string -> object ->
    3.20 +    (object -> object) -> (object * object -> object) -> (object -> unit) -> T
    3.21 +  val get: T -> string -> object
    3.22 +  val put: T -> string -> object -> T
    3.23    val print: T -> string -> unit
    3.24  end;
    3.25  
    3.26 @@ -27,10 +30,10 @@
    3.27  (* datatype T *)
    3.28  
    3.29  datatype T = Data of
    3.30 -  (exn *				(*value*)
    3.31 -   ((exn -> exn) *			(*prepare extend method*)
    3.32 -    (exn * exn -> exn) *		(*merge and prepare extend method*)
    3.33 -    (exn -> unit)))			(*print method*)
    3.34 +  (object *                             (*value*)
    3.35 +   ((object -> object) *                (*prepare extend method*)
    3.36 +    (object * object -> object) *       (*merge and prepare extend method*)
    3.37 +    (object -> unit)))                  (*print method*)
    3.38    Symtab.table;
    3.39  
    3.40  val empty = Data Symtab.null;
    3.41 @@ -65,9 +68,9 @@
    3.42       | Some x => [(kind, x)]);
    3.43  
    3.44      fun merge_entries [(kind, (e, mths as (ext, _, _)))] =
    3.45 -          (kind, (ext e handle exn => err_method "prep_ext" kind, mths))
    3.46 +          (kind, (ext e handle _ => err_method "prep_ext" kind, mths))
    3.47        | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] =
    3.48 -          (kind, (mrg (e1, e2) handle exn => (err_method "merge" kind; raise exn), mths))
    3.49 +          (kind, (mrg (e1, e2) handle _ => err_method "merge" kind, mths))
    3.50        | merge_entries _ = sys_error "merge_entries";
    3.51  
    3.52      val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
    3.53 @@ -95,7 +98,7 @@
    3.54  
    3.55  fun print (Data tab) kind =
    3.56    let val (e, (_, _, prt)) = lookup tab kind
    3.57 -  in prt e handle exn => err_method "print" kind end;
    3.58 +  in prt e handle _ => err_method "print" kind end;
    3.59  
    3.60  
    3.61  end;
     4.1 --- a/src/Pure/pure_thy.ML	Tue Nov 04 15:16:23 1997 +0100
     4.2 +++ b/src/Pure/pure_thy.ML	Tue Nov 04 16:17:04 1997 +0100
     4.3 @@ -69,8 +69,8 @@
     4.4  
     4.5  in
     4.6  
     4.7 -val theorems_data:
     4.8 -  string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit)) =
     4.9 +val theorems_data: string * (object * (object -> object) *
    4.10 +  (object * object -> object) * (object -> unit)) =
    4.11      (theoremsK, (mk_empty (), mk_empty, mk_empty, print));
    4.12  
    4.13  end;
     5.1 --- a/src/Pure/sign.ML	Tue Nov 04 15:16:23 1997 +0100
     5.2 +++ b/src/Pure/sign.ML	Tue Nov 04 16:17:04 1997 +0100
     5.3 @@ -110,10 +110,10 @@
     5.4    val add_path: string -> sg -> sg
     5.5    val add_space: string * string list -> sg -> sg
     5.6    val add_name: string -> sg -> sg
     5.7 -  val init_data: string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))
     5.8 -    -> sg -> sg
     5.9 -  val get_data: sg -> string -> exn
    5.10 -  val put_data: string * exn -> sg -> sg
    5.11 +  val init_data: string * (object * (object -> object) *
    5.12 +    (object * object -> object) * (object -> unit)) -> sg -> sg
    5.13 +  val get_data: sg -> string -> object
    5.14 +  val put_data: string * object -> sg -> sg
    5.15    val print_data: sg -> string -> unit
    5.16    val merge_refs: sg_ref * sg_ref -> sg_ref
    5.17    val prep_ext: sg -> sg
     6.1 --- a/src/Pure/theory.ML	Tue Nov 04 15:16:23 1997 +0100
     6.2 +++ b/src/Pure/theory.ML	Tue Nov 04 16:17:04 1997 +0100
     6.3 @@ -14,7 +14,7 @@
     6.4    val rep_theory: theory ->
     6.5      {sign: Sign.sg,
     6.6        axioms: term Symtab.table,
     6.7 -      oracles: ((Sign.sg * exn -> term) * stamp) Symtab.table,
     6.8 +      oracles: ((Sign.sg * object -> term) * stamp) Symtab.table,
     6.9        parents: theory list,
    6.10        ancestors: theory list}
    6.11    val sign_of: theory -> Sign.sg
    6.12 @@ -67,16 +67,16 @@
    6.13    val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory
    6.14    val add_axioms: (bstring * string) list -> theory -> theory
    6.15    val add_axioms_i: (bstring * term) list -> theory -> theory
    6.16 -  val add_oracle: bstring * (Sign.sg * exn -> term) -> theory -> theory
    6.17 +  val add_oracle: bstring * (Sign.sg * object -> term) -> theory -> theory
    6.18    val add_defs: (bstring * string) list -> theory -> theory
    6.19    val add_defs_i: (bstring * term) list -> theory -> theory
    6.20    val add_path: string -> theory -> theory
    6.21    val add_space: string * string list -> theory -> theory
    6.22    val add_name: string -> theory -> theory
    6.23 -  val init_data: (string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))) list
    6.24 -    -> theory -> theory
    6.25 -  val get_data: theory -> string -> exn
    6.26 -  val put_data: string * exn -> theory -> theory
    6.27 +  val init_data: (string * (object * (object -> object) *
    6.28 +    (object * object -> object) * (object -> unit))) list -> theory -> theory
    6.29 +  val get_data: theory -> string -> object
    6.30 +  val put_data: string * object -> theory -> theory
    6.31    val prep_ext: theory -> theory
    6.32    val prep_ext_merge: theory list -> theory
    6.33    val pre_pure: theory
    6.34 @@ -93,7 +93,7 @@
    6.35    Theory of {
    6.36      sign: Sign.sg,
    6.37      axioms: term Symtab.table,
    6.38 -    oracles: ((Sign.sg * exn -> term) * stamp) Symtab.table,
    6.39 +    oracles: ((Sign.sg * object -> term) * stamp) Symtab.table,
    6.40      parents: theory list,
    6.41      ancestors: theory list};
    6.42  
     7.1 --- a/src/Pure/thm.ML	Tue Nov 04 15:16:23 1997 +0100
     7.2 +++ b/src/Pure/thm.ML	Tue Nov 04 16:17:04 1997 +0100
     7.3 @@ -41,7 +41,7 @@
     7.4    val keep_derivs       : deriv_kind ref
     7.5    datatype rule = 
     7.6        MinProof                          
     7.7 -    | Oracle of theory * string * Sign.sg * exn
     7.8 +    | Oracle of theory * string * Sign.sg * object
     7.9      | Axiom               of theory * string
    7.10      | Theorem             of string       
    7.11      | Assume              of cterm
    7.12 @@ -166,7 +166,7 @@
    7.13    val rewrite_cterm     : bool * bool -> meta_simpset ->
    7.14                            (meta_simpset -> thm -> thm option) -> cterm -> thm
    7.15  
    7.16 -  val invoke_oracle     : theory -> xstring -> Sign.sg * exn -> thm
    7.17 +  val invoke_oracle     : theory -> xstring -> Sign.sg * object -> thm
    7.18  end;
    7.19  
    7.20  structure Thm: THM =
    7.21 @@ -303,7 +303,7 @@
    7.22    executed in ML.*)
    7.23  datatype rule = 
    7.24      MinProof                            (*for building minimal proof terms*)
    7.25 -  | Oracle              of theory * string * Sign.sg * exn       (*oracles*)
    7.26 +  | Oracle              of theory * string * Sign.sg * object       (*oracles*)
    7.27  (*Axioms/theorems*)
    7.28    | Axiom               of theory * string
    7.29    | Theorem             of string