# HG changeset patch
# User haftmann
# Date 1372014966 -7200
# Node ID cbb94074682b8bbce06a410eff341ea4e286c9c9
# Parent  ec3a22e62b54e22083b82c0ae044de1e6d31eaf6
more appropriate cutting of input syntax

diff -r ec3a22e62b54 -r cbb94074682b src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sun Jun 23 21:16:06 2013 +0200
+++ b/src/Tools/Code/code_runtime.ML	Sun Jun 23 21:16:06 2013 +0200
@@ -357,10 +357,10 @@
 val _ =
   Outer_Syntax.command @{command_spec "code_reflect"}
     "enrich runtime environment with generated code"
-    (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype
+    (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!!  (parse_datatype
       ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
-    -- Scan.optional (@{keyword "functions"} |-- Scan.repeat1 Parse.name) []
-    -- Scan.option (@{keyword "file"} |-- Parse.name)
+    -- Scan.optional (@{keyword "functions"} |-- Parse.!!!  (Scan.repeat1 Parse.name)) []
+    -- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name)
     >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
       (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
 
diff -r ec3a22e62b54 -r cbb94074682b src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Jun 23 21:16:06 2013 +0200
+++ b/src/Tools/Code/code_target.ML	Sun Jun 23 21:16:06 2013 +0200
@@ -742,8 +742,8 @@
 (** Isar setup **)
 
 fun parse_single_symbol_pragma parse_keyword parse_isa parse_target =
-  parse_keyword |-- Parse.!!! parse_isa --| (@{keyword "\<rightharpoonup>"} || @{keyword "=>"})
-    -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target));
+  parse_keyword |-- Parse.!!! (parse_isa --| (@{keyword "\<rightharpoonup>"} || @{keyword "=>"})
+    -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target)));
 
 fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
   parse_single_symbol_pragma @{keyword "constant"} Parse.term_group parse_const
@@ -765,15 +765,21 @@
 
 val code_expr_argsP = Scan.optional (@{keyword "("} |-- Args.parse --| @{keyword ")"}) [];
 
-val code_exprP =
-  Scan.repeat1 Parse.term_group :|-- (fn raw_cs =>
-    ((@{keyword "checking"} |-- Scan.repeat (Parse.name
-      -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
-      >> (fn seris => check_code_cmd raw_cs seris)
-    || Scan.repeat (@{keyword "in"} |-- Parse.name
-       -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
-       -- Scan.optional (@{keyword "file"} |-- Parse.name) ""
-       -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
+fun code_expr_inP raw_cs =
+  Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name
+    -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
+    -- Scan.optional (@{keyword "file"} |-- Parse.name) ""
+    -- code_expr_argsP))
+      >> (fn seri_args => export_code_cmd raw_cs seri_args);
+
+fun code_expr_checkingP raw_cs =
+  (@{keyword "checking"} |-- Parse.!!!
+    (Scan.repeat (Parse.name -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true)
+    -- code_expr_argsP)))
+      >> (fn seri_args => check_code_cmd raw_cs seri_args);
+
+val code_exprP = Scan.repeat1 Parse.term_group
+  :|-- (fn raw_cs => (code_expr_checkingP raw_cs || code_expr_inP raw_cs));
 
 val _ =
   Outer_Syntax.command @{command_spec "code_reserved"}