src/Pure/codegen.ML

--- a/src/Pure/codegen.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/codegen.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -1100,6 +1100,8 @@
 
 structure P = OuterParse and K = OuterKeyword;
 
+val _ = OuterSyntax.keywords ["attach", "file", "contains"];
+
 fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
   (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
 
@@ -1107,7 +1109,7 @@
   Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
     (P.verbatim >> strip_whitespace));
 
-val assoc_typeP =
+val _ =
   OuterSyntax.command "types_code"
   "associate types with target language types" K.thy_decl
     (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
@@ -1115,7 +1117,7 @@
        (fn ((name, mfx), aux) => (name, (parse_mixfix
          (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
 
-val assoc_constP =
+val _ =
   OuterSyntax.command "consts_code"
   "associate constants with target language code" K.thy_decl
     (Scan.repeat1
@@ -1152,12 +1154,12 @@
            else map_modules (Symtab.update (module, gr)) thy)
      end));
 
-val code_libraryP =
+val _ =
   OuterSyntax.command "code_library"
     "generates code for terms (one structure for each theory)" K.thy_decl
     (parse_code true);
 
-val code_moduleP =
+val _ =
   OuterSyntax.command "code_module"
     "generates code for terms (single structure, incremental)" K.thy_decl
     (parse_code false);
@@ -1174,13 +1176,13 @@
   (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
     fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
 
-val test_paramsP =
+val _ =
   OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
     (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
       (fn fs => Toplevel.theory (fn thy =>
          map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
 
-val testP =
+val _ =
   OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
   (Scan.option (P.$$$ "[" |-- P.list1
     (   parse_test_params >> (fn f => fn thy => apfst (f thy))
@@ -1191,15 +1193,10 @@
         (get_test_params (Toplevel.theory_of st), [])) g [] |>
       pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
 
-val valueP =
+val _ =
   OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
     (P.term >> (Toplevel.no_timing oo print_evaluated_term));
 
-val _ = OuterSyntax.add_keywords ["attach", "file", "contains"];
-
-val _ = OuterSyntax.add_parsers
-  [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP];
-
 end;
 
 val auto_quickcheck = Codegen.auto_quickcheck;