PRIVATE sig parts;
authorwenzelm
Tue Oct 13 14:24:35 1998 +0200 (1998-10-13)
changeset 56421b3e48bdbb93
parent 5641 5266f09db46c
child 5643 983ce1421211
PRIVATE sig parts;
src/Pure/sign.ML
src/Pure/theory.ML
src/Pure/theory_data.ML
     1.1 --- a/src/Pure/sign.ML	Tue Oct 13 11:08:28 1998 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Oct 13 14:24:35 1998 +0200
     1.3 @@ -121,11 +121,6 @@
     1.4    val add_space: string * string list -> sg -> sg
     1.5    val add_name: string -> sg -> sg
     1.6    val data_kinds: data -> string list
     1.7 -  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) *
     1.8 -    (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
     1.9 -  val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
    1.10 -  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
    1.11 -  val print_data: Object.kind -> sg -> unit
    1.12    val merge_refs: sg_ref * sg_ref -> sg_ref
    1.13    val merge: sg * sg -> sg
    1.14    val prep_ext: sg -> sg
    1.15 @@ -135,7 +130,17 @@
    1.16    val class_of_const: string -> class
    1.17  end;
    1.18  
    1.19 -structure Sign: SIGN =
    1.20 +signature SIGN_PRIVATE =
    1.21 +sig
    1.22 +  include SIGN
    1.23 +  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) *
    1.24 +    (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
    1.25 +  val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
    1.26 +  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
    1.27 +  val print_data: Object.kind -> sg -> unit
    1.28 +end;
    1.29 +
    1.30 +structure Sign: SIGN_PRIVATE =
    1.31  struct
    1.32  
    1.33  
     2.1 --- a/src/Pure/theory.ML	Tue Oct 13 11:08:28 1998 +0200
     2.2 +++ b/src/Pure/theory.ML	Tue Oct 13 14:24:35 1998 +0200
     2.3 @@ -79,19 +79,24 @@
     2.4    val root_path: theory -> theory
     2.5    val add_space: string * string list -> theory -> theory
     2.6    val add_name: string -> theory -> theory
     2.7 -  val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
     2.8 -    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
     2.9 -  val print_data: Object.kind -> theory -> unit
    2.10 -  val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
    2.11 -  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
    2.12    val prep_ext: theory -> theory
    2.13    val prep_ext_merge: theory list -> theory
    2.14    val requires: theory -> string -> string -> unit
    2.15    val pre_pure: theory
    2.16  end;
    2.17  
    2.18 +signature THEORY_PRIVATE =
    2.19 +sig
    2.20 +  include THEORY
    2.21 +  val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
    2.22 +    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
    2.23 +  val print_data: Object.kind -> theory -> unit
    2.24 +  val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
    2.25 +  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
    2.26 +end;
    2.27  
    2.28 -structure Theory: THEORY =
    2.29 +
    2.30 +structure Theory: THEORY_PRIVATE =
    2.31  struct
    2.32  
    2.33  
     3.1 --- a/src/Pure/theory_data.ML	Tue Oct 13 11:08:28 1998 +0200
     3.2 +++ b/src/Pure/theory_data.ML	Tue Oct 13 14:24:35 1998 +0200
     3.3 @@ -47,3 +47,9 @@
     3.4  val put = Theory.put_data kind Data;
     3.5  
     3.6  end;
     3.7 +
     3.8 +(* FIXME deactivated due to Provers/classical.ML legacy code
     3.9 +(*hide private data access functions*)
    3.10 +structure Sign: SIGN = Sign;
    3.11 +structure Theory: THEORY = Theory;
    3.12 +*)