src/Tools/Code/code_target.ML
changeset 37825 adc1143bc1a8
parent 37824 365e37fe93f3
child 37840 a3632a0b7d6c
     1.1 --- a/src/Tools/Code/code_target.ML	Wed Jul 14 15:49:29 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Wed Jul 14 16:02:50 2010 +0200
     1.3 @@ -321,7 +321,7 @@
     1.4  
     1.5  fun serialize thy = mount_serializer thy NONE;
     1.6  
     1.7 -fun check thy names_cs naming program target args =
     1.8 +fun check thy names_cs naming program target strict args =
     1.9    let
    1.10      val module_name = "Code_Test";
    1.11      val { env_var, make_destination, make_command } =
    1.12 @@ -338,7 +338,9 @@
    1.13          else ()
    1.14        end;
    1.15    in if env_param = ""
    1.16 -    then warning (env_var ^ " not set; skipped code check for " ^ target)
    1.17 +    then if strict
    1.18 +      then error (env_var ^ " not set; cannot check code for " ^ target)
    1.19 +      else warning (env_var ^ " not set; skipped checking code for " ^ target)
    1.20      else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
    1.21    end;
    1.22  
    1.23 @@ -391,7 +393,8 @@
    1.24  fun check_code thy cs seris =
    1.25    let
    1.26      val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    1.27 -    val _ = map (fn (target, args) => check thy names_cs naming program target args) seris;
    1.28 +    val _ = map (fn ((target, strict), args) => check thy names_cs naming program
    1.29 +      target strict args) seris;
    1.30    in () end;
    1.31  
    1.32  fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
    1.33 @@ -535,7 +538,8 @@
    1.34  
    1.35  val code_exprP =
    1.36    Scan.repeat1 Parse.term_group :|-- (fn raw_cs =>
    1.37 -    ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name -- code_expr_argsP))
    1.38 +    ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name
    1.39 +      -- ((Parse.$$$ "?" |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
    1.40        >> (fn seris => check_code_cmd raw_cs seris)
    1.41      || Scan.repeat (Parse.$$$ inK |-- Parse.name
    1.42         -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)