src/Pure/Thy/thy_parse.ML
changeset 414 9dca566d6d96
parent 389 85105a7fb668
child 425 c42f384c89de
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Jun 01 15:47:27 1994 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Jun 01 15:49:46 1994 +0200
     1.3 @@ -57,10 +57,9 @@
     1.4    val pure_keywords: string list
     1.5    val pure_sections:
     1.6      (string * (token list -> (string * string) * token list)) list
     1.7 -  val pure_syntax: syntax
     1.8  end;
     1.9  
    1.10 -functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN)(*: THY_PARSE *) = (* FIXME *)
    1.11 +functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE =
    1.12  struct
    1.13  
    1.14  open ThyScan;
    1.15 @@ -230,8 +229,8 @@
    1.16        [(pars (commas [t, mk_list xs, rhs, syn]), true)];
    1.17  
    1.18  fun mk_type_decls tys =
    1.19 -  "also add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
    1.20 -  \also add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
    1.21 +  "|> add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
    1.22 +  \|> add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
    1.23  
    1.24  
    1.25  val old_type_decl = names -- nat -- opt_infix >> mk_old_type_decl;
    1.26 @@ -309,6 +308,14 @@
    1.27  val axclass_decl = subclass -- repeat (ident -- !! string) >> mk_axclass_decl;
    1.28  
    1.29  
    1.30 +(* sigclass *)
    1.31 +
    1.32 +fun mk_sigclass_decl ((c, cs), consts) = 
    1.33 +  (mk_pair (c, cs) ^ "\n" ^ consts, [strip_quotes c ^ "I"]);
    1.34 +
    1.35 +val sigclass_decl = subclass -- optional const_decls "[]" >> mk_sigclass_decl;
    1.36 +
    1.37 +
    1.38  (* instance *)
    1.39  
    1.40  fun mk_instance_decl ((((t, ss), c), axths), opt_tac) =
    1.41 @@ -385,12 +392,12 @@
    1.42        ^ mltxt ^ "\n\
    1.43        \\n\
    1.44        \val thy = " ^ old_thys ^ "\n\n\
    1.45 -      \also add_trfuns\n"
    1.46 +      \|> add_trfuns\n"
    1.47        ^ trfun_args ^ "\n\
    1.48        \\n"
    1.49        ^ extxt ^ "\n\
    1.50        \\n\
    1.51 -      \also add_thyname " ^ quote thy_name ^ ";\n\
    1.52 +      \|> add_thyname " ^ quote thy_name ^ ";\n\
    1.53        \\n\
    1.54        \\n"
    1.55        ^ postxt ^ "\n\
    1.56 @@ -430,27 +437,26 @@
    1.57  val pure_keywords =
    1.58   ["classes", "default", "types", "arities", "consts", "syntax",
    1.59    "translations", "MLtrans", "MLtext", "rules", "defns", "axclass",
    1.60 -  "instance", "end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+",
    1.61 -  ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
    1.62 +  "sigclass", "instance", "end", "ML", "mixfix", "infixr", "infixl",
    1.63 +  "binder", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]", "::",
    1.64 +  "==", "=>", "<="];
    1.65  
    1.66  val pure_sections =
    1.67 - [section "classes" "also add_classes" class_decls,
    1.68 -  section "default" "also add_defsort" sort,
    1.69 + [section "classes" "|> add_classes" class_decls,
    1.70 +  section "default" "|> add_defsort" sort,
    1.71    ("types", type_decls),
    1.72 -  section "arities" "also add_arities" arity_decls,
    1.73 -  section "consts" "also add_consts" const_decls,
    1.74 -  section "syntax" "also add_syntax" const_decls,
    1.75 -  section "translations" "also add_trrules" trans_decls,
    1.76 -  section "MLtrans" "also add_trfuns" mltrans,
    1.77 +  section "arities" "|> add_arities" arity_decls,
    1.78 +  section "consts" "|> add_consts" const_decls,
    1.79 +  section "syntax" "|> add_syntax" const_decls,
    1.80 +  section "translations" "|> add_trrules" trans_decls,
    1.81 +  section "MLtrans" "|> add_trfuns" mltrans,
    1.82    ("MLtext", verbatim >> rpair ""),
    1.83 -  axm_section "rules" "also add_axioms" axiom_decls,
    1.84 -  axm_section "defns" "also add_defns" axiom_decls,
    1.85 -  axm_section "axclass" "also add_axclass" axclass_decl,
    1.86 -  section "instance" "also add_instance" instance_decl];
    1.87 +  axm_section "rules" "|> add_axioms" axiom_decls,
    1.88 +  axm_section "defns" "|> add_defns" axiom_decls,
    1.89 +  axm_section "axclass" "|> add_axclass" axclass_decl,
    1.90 +  axm_section "sigclass" "|> add_sigclass" sigclass_decl,
    1.91 +  section "instance" "|> add_instance" instance_decl];
    1.92  
    1.93  
    1.94 -(* FIXME -> thy_read.ML *)
    1.95 -val pure_syntax = make_syntax pure_keywords pure_sections;
    1.96 -
    1.97  end;
    1.98