src/Tools/Code/code_runtime.ML
changeset 63174 57c0d60e491c
parent 63164 72aaf69328fc
child 63184 dd6cd88cebd9
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sun May 29 14:10:48 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sun May 29 14:43:17 2016 +0200
     1.3 @@ -375,20 +375,21 @@
     1.4  
     1.5  fun check_datatype thy tyco some_consts =
     1.6    let
     1.7 -    val constrs = (map fst o snd o fst o Code.get_type thy) tyco;
     1.8 -    val _ = case some_consts
     1.9 -     of SOME consts =>
    1.10 +    val declared_constrs = (map fst o snd o fst o Code.get_type thy) tyco;
    1.11 +    val constrs = case some_consts
    1.12 +     of SOME [] => []
    1.13 +      | SOME consts =>
    1.14            let
    1.15 -            val missing_constrs = subtract (op =) consts constrs;
    1.16 +            val missing_constrs = subtract (op =) consts declared_constrs;
    1.17              val _ = if null missing_constrs then []
    1.18                else error ("Missing constructor(s) " ^ commas_quote missing_constrs
    1.19                  ^ " for datatype " ^ quote tyco);
    1.20 -            val false_constrs = subtract (op =) constrs consts;
    1.21 +            val false_constrs = subtract (op =) declared_constrs consts;
    1.22              val _ = if null false_constrs then []
    1.23                else error ("Non-constructor(s) " ^ commas_quote false_constrs
    1.24                  ^ " for datatype " ^ quote tyco)
    1.25 -          in () end
    1.26 -      | NONE => ();
    1.27 +          in consts end
    1.28 +      | NONE => declared_constrs;
    1.29    in (tyco, constrs) end;
    1.30  
    1.31  fun add_eval_tyco (tyco, tyco') thy =
    1.32 @@ -465,16 +466,16 @@
    1.33  local
    1.34  
    1.35  val parse_datatype =
    1.36 -  Parse.name --| @{keyword "="} --
    1.37 +  Parse.name -- Scan.optional (@{keyword "="} |--
    1.38      (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
    1.39 -    || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME));
    1.40 +    || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME))) (SOME []);
    1.41  
    1.42  in
    1.43  
    1.44  val _ =
    1.45    Outer_Syntax.command @{command_keyword code_reflect}
    1.46      "enrich runtime environment with generated code"
    1.47 -    (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!!  (parse_datatype
    1.48 +    (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype
    1.49        ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
    1.50      -- Scan.optional (@{keyword "functions"} |-- Parse.!!!  (Scan.repeat1 Parse.name)) []
    1.51      -- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name)