# HG changeset patch
# User haftmann
# Date 1279116170 -7200
# Node ID adc1143bc1a8aa7f62d80a705ce548ed72fa2476
# Parent  365e37fe93f37ba76cb1c4e8605afbeaf2027d9a
explicit optional checking

diff -r 365e37fe93f3 -r adc1143bc1a8 src/HOL/Codegenerator_Test/Generate.thy
--- a/src/HOL/Codegenerator_Test/Generate.thy	Wed Jul 14 15:49:29 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Wed Jul 14 16:02:50 2010 +0200
@@ -14,6 +14,6 @@
   by a corresponding @{text export_code} command.
 *}
 
-export_code "*" checking SML OCaml Haskell Scala
+export_code "*" checking SML OCaml? Haskell? Scala?
 
 end
diff -r 365e37fe93f3 -r adc1143bc1a8 src/HOL/Codegenerator_Test/Generate_Pretty.thy
--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed Jul 14 15:49:29 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed Jul 14 16:02:50 2010 +0200
@@ -19,6 +19,6 @@
   by a corresponding @{text export_code} command.
 *}
 
-export_code "*" checking SML OCaml Haskell Scala
+export_code "*" checking SML OCaml? Haskell? Scala?
 
 end
diff -r 365e37fe93f3 -r adc1143bc1a8 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Jul 14 15:49:29 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Wed Jul 14 16:02:50 2010 +0200
@@ -321,7 +321,7 @@
 
 fun serialize thy = mount_serializer thy NONE;
 
-fun check thy names_cs naming program target args =
+fun check thy names_cs naming program target strict args =
   let
     val module_name = "Code_Test";
     val { env_var, make_destination, make_command } =
@@ -338,7 +338,9 @@
         else ()
       end;
   in if env_param = ""
-    then warning (env_var ^ " not set; skipped code check for " ^ target)
+    then if strict
+      then error (env_var ^ " not set; cannot check code for " ^ target)
+      else warning (env_var ^ " not set; skipped checking code for " ^ target)
     else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
   end;
 
@@ -391,7 +393,8 @@
 fun check_code thy cs seris =
   let
     val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
-    val _ = map (fn (target, args) => check thy names_cs naming program target args) seris;
+    val _ = map (fn ((target, strict), args) => check thy names_cs naming program
+      target strict args) seris;
   in () end;
 
 fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
@@ -535,7 +538,8 @@
 
 val code_exprP =
   Scan.repeat1 Parse.term_group :|-- (fn raw_cs =>
-    ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name -- code_expr_argsP))
+    ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name
+      -- ((Parse.$$$ "?" |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
       >> (fn seris => check_code_cmd raw_cs seris)
     || Scan.repeat (Parse.$$$ inK |-- Parse.name
        -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)