src/Pure/codegen.ML
changeset 24867 e5b55d7be9bb
parent 24805 34cbfb87dfe8
child 24908 c74ad8782eeb
     1.1 --- a/src/Pure/codegen.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -1100,6 +1100,8 @@
     1.4  
     1.5  structure P = OuterParse and K = OuterKeyword;
     1.6  
     1.7 +val _ = OuterSyntax.keywords ["attach", "file", "contains"];
     1.8 +
     1.9  fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
    1.10    (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
    1.11  
    1.12 @@ -1107,7 +1109,7 @@
    1.13    Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
    1.14      (P.verbatim >> strip_whitespace));
    1.15  
    1.16 -val assoc_typeP =
    1.17 +val _ =
    1.18    OuterSyntax.command "types_code"
    1.19    "associate types with target language types" K.thy_decl
    1.20      (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
    1.21 @@ -1115,7 +1117,7 @@
    1.22         (fn ((name, mfx), aux) => (name, (parse_mixfix
    1.23           (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
    1.24  
    1.25 -val assoc_constP =
    1.26 +val _ =
    1.27    OuterSyntax.command "consts_code"
    1.28    "associate constants with target language code" K.thy_decl
    1.29      (Scan.repeat1
    1.30 @@ -1152,12 +1154,12 @@
    1.31             else map_modules (Symtab.update (module, gr)) thy)
    1.32       end));
    1.33  
    1.34 -val code_libraryP =
    1.35 +val _ =
    1.36    OuterSyntax.command "code_library"
    1.37      "generates code for terms (one structure for each theory)" K.thy_decl
    1.38      (parse_code true);
    1.39  
    1.40 -val code_moduleP =
    1.41 +val _ =
    1.42    OuterSyntax.command "code_module"
    1.43      "generates code for terms (single structure, incremental)" K.thy_decl
    1.44      (parse_code false);
    1.45 @@ -1174,13 +1176,13 @@
    1.46    (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
    1.47      fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
    1.48  
    1.49 -val test_paramsP =
    1.50 +val _ =
    1.51    OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
    1.52      (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
    1.53        (fn fs => Toplevel.theory (fn thy =>
    1.54           map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
    1.55  
    1.56 -val testP =
    1.57 +val _ =
    1.58    OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
    1.59    (Scan.option (P.$$$ "[" |-- P.list1
    1.60      (   parse_test_params >> (fn f => fn thy => apfst (f thy))
    1.61 @@ -1191,15 +1193,10 @@
    1.62          (get_test_params (Toplevel.theory_of st), [])) g [] |>
    1.63        pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
    1.64  
    1.65 -val valueP =
    1.66 +val _ =
    1.67    OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
    1.68      (P.term >> (Toplevel.no_timing oo print_evaluated_term));
    1.69  
    1.70 -val _ = OuterSyntax.add_keywords ["attach", "file", "contains"];
    1.71 -
    1.72 -val _ = OuterSyntax.add_parsers
    1.73 -  [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP];
    1.74 -
    1.75  end;
    1.76  
    1.77  val auto_quickcheck = Codegen.auto_quickcheck;