# HG changeset patch
# User wenzelm
# Date 893841434 -7200
# Node ID 9c072489a9e7ec8085bbe3360a3908576e955e5d
# Parent  fdc7d8949d82600a5b1d8cee718713e474b1c532
renamed setup to apply;
added add_nonterminals: bstring list -> theory -> theory;
added parent_path: theory -> theory;
added root_path: theory -> theory;
added require: theory -> string -> string -> unit (from section_utils.ML);

diff -r fdc7d8949d82 -r 9c072489a9e7 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Apr 29 11:14:34 1998 +0200
+++ b/src/Pure/theory.ML	Wed Apr 29 11:17:14 1998 +0200
@@ -33,6 +33,7 @@
 signature THEORY =
 sig
   include BASIC_THEORY
+  val apply: (theory -> theory) list -> theory -> theory
   val axiomK: string
   val oracleK: string
   (*theory extendsion primitives*)
@@ -43,6 +44,7 @@
   val add_defsort: xsort -> theory -> theory
   val add_defsort_i: sort -> theory -> theory
   val add_types: (bstring * int * mixfix) list -> theory -> theory
+  val add_nonterminals: bstring list -> theory -> theory
   val add_tyabbrs: (bstring * string list * string * mixfix) list
     -> theory -> theory
   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
@@ -72,15 +74,17 @@
   val add_defs: (bstring * string) list -> theory -> theory
   val add_defs_i: (bstring * term) list -> theory -> theory
   val add_path: string -> theory -> theory
+  val parent_path: theory -> theory
+  val root_path: theory -> theory
   val add_space: string * string list -> theory -> theory
   val add_name: string -> theory -> theory
   val init_data: (string * (object * (object -> object) *
     (object * object -> object) * (Sign.sg -> object -> unit))) list -> theory -> theory
   val get_data: theory -> string -> object
   val put_data: string * object -> theory -> theory
-  val setup: (theory -> theory) list -> theory -> theory
   val prep_ext: theory -> theory
   val prep_ext_merge: theory list -> theory
+  val require: theory -> string -> string -> unit
   val pre_pure: theory
 end;
 
@@ -120,10 +124,17 @@
 val subthy = Sign.subsig o pairself sign_of;
 val eq_thy = Sign.eq_sg o pairself sign_of;
 
+(*check for some named theory*)
+fun require thy name what =
+  if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then ()
+  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
 
-(* partial Pure theory *)
+(*partial Pure theory*)
+val pre_pure = make_thy Sign.pre_pure Symtab.empty Symtab.empty [] [];
 
-val pre_pure = make_thy Sign.pre_pure Symtab.empty Symtab.empty [] [];
+(*apply transformers*)
+fun apply [] thy = thy
+  | apply (f :: fs) thy = apply fs (f thy);
 
 
 
@@ -172,6 +183,7 @@
 val add_defsort      = ext_sg Sign.add_defsort;
 val add_defsort_i    = ext_sg Sign.add_defsort_i;
 val add_types        = ext_sg Sign.add_types;
+val add_nonterminals = ext_sg Sign.add_nonterminals;
 val add_tyabbrs      = ext_sg Sign.add_tyabbrs;
 val add_tyabbrs_i    = ext_sg Sign.add_tyabbrs_i;
 val add_arities      = ext_sg Sign.add_arities;
@@ -188,6 +200,8 @@
 val add_trrules      = ext_sg Sign.add_trrules;
 val add_trrules_i    = ext_sg Sign.add_trrules_i;
 val add_path         = ext_sg Sign.add_path;
+val parent_path      = add_path "..";
+val root_path        = add_path "/";
 val add_space        = ext_sg Sign.add_space;
 val add_name         = ext_sg Sign.add_name;
 val prep_ext         = ext_sg (K Sign.prep_ext) ();
@@ -385,10 +399,6 @@
 val get_data = Sign.get_data o sign_of;
 val put_data = ext_sg Sign.put_data;
 
-(*generic setup*)
-fun setup [] thy = thy
-  | setup (f :: fs) thy = setup fs (f thy);
-
 
 
 (** merge theories **)		(*exception ERROR*)