# HG changeset patch
# User wenzelm
# Date 770478586 -7200
# Node ID 9dca566d6d96011c51029d50646af1593b20e248
# Parent  2a1554524ad5943f2c66cc4011d9ff7fda7c3160
added signature constraint;
replaced 'also' by '|>';
added  'sigclass' section;
removed pure_syntax;

diff -r 2a1554524ad5 -r 9dca566d6d96 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Wed Jun 01 15:47:27 1994 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Wed Jun 01 15:49:46 1994 +0200
@@ -57,10 +57,9 @@
   val pure_keywords: string list
   val pure_sections:
     (string * (token list -> (string * string) * token list)) list
-  val pure_syntax: syntax
 end;
 
-functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN)(*: THY_PARSE *) = (* FIXME *)
+functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE =
 struct
 
 open ThyScan;
@@ -230,8 +229,8 @@
       [(pars (commas [t, mk_list xs, rhs, syn]), true)];
 
 fun mk_type_decls tys =
-  "also add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
-  \also add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
+  "|> add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
+  \|> add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
 
 
 val old_type_decl = names -- nat -- opt_infix >> mk_old_type_decl;
@@ -309,6 +308,14 @@
 val axclass_decl = subclass -- repeat (ident -- !! string) >> mk_axclass_decl;
 
 
+(* sigclass *)
+
+fun mk_sigclass_decl ((c, cs), consts) = 
+  (mk_pair (c, cs) ^ "\n" ^ consts, [strip_quotes c ^ "I"]);
+
+val sigclass_decl = subclass -- optional const_decls "[]" >> mk_sigclass_decl;
+
+
 (* instance *)
 
 fun mk_instance_decl ((((t, ss), c), axths), opt_tac) =
@@ -385,12 +392,12 @@
       ^ mltxt ^ "\n\
       \\n\
       \val thy = " ^ old_thys ^ "\n\n\
-      \also add_trfuns\n"
+      \|> add_trfuns\n"
       ^ trfun_args ^ "\n\
       \\n"
       ^ extxt ^ "\n\
       \\n\
-      \also add_thyname " ^ quote thy_name ^ ";\n\
+      \|> add_thyname " ^ quote thy_name ^ ";\n\
       \\n\
       \\n"
       ^ postxt ^ "\n\
@@ -430,27 +437,26 @@
 val pure_keywords =
  ["classes", "default", "types", "arities", "consts", "syntax",
   "translations", "MLtrans", "MLtext", "rules", "defns", "axclass",
-  "instance", "end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+",
-  ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
+  "sigclass", "instance", "end", "ML", "mixfix", "infixr", "infixl",
+  "binder", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]", "::",
+  "==", "=>", "<="];
 
 val pure_sections =
- [section "classes" "also add_classes" class_decls,
-  section "default" "also add_defsort" sort,
+ [section "classes" "|> add_classes" class_decls,
+  section "default" "|> add_defsort" sort,
   ("types", type_decls),
-  section "arities" "also add_arities" arity_decls,
-  section "consts" "also add_consts" const_decls,
-  section "syntax" "also add_syntax" const_decls,
-  section "translations" "also add_trrules" trans_decls,
-  section "MLtrans" "also add_trfuns" mltrans,
+  section "arities" "|> add_arities" arity_decls,
+  section "consts" "|> add_consts" const_decls,
+  section "syntax" "|> add_syntax" const_decls,
+  section "translations" "|> add_trrules" trans_decls,
+  section "MLtrans" "|> add_trfuns" mltrans,
   ("MLtext", verbatim >> rpair ""),
-  axm_section "rules" "also add_axioms" axiom_decls,
-  axm_section "defns" "also add_defns" axiom_decls,
-  axm_section "axclass" "also add_axclass" axclass_decl,
-  section "instance" "also add_instance" instance_decl];
+  axm_section "rules" "|> add_axioms" axiom_decls,
+  axm_section "defns" "|> add_defns" axiom_decls,
+  axm_section "axclass" "|> add_axclass" axclass_decl,
+  axm_section "sigclass" "|> add_sigclass" sigclass_decl,
+  section "instance" "|> add_instance" instance_decl];
 
 
-(* FIXME -> thy_read.ML *)
-val pure_syntax = make_syntax pure_keywords pure_sections;
-
 end;