equal
deleted
inserted
replaced
520 |> (fn (r, state) => Output.urgent_message (Pretty.string_of |
520 |> (fn (r, state) => Output.urgent_message (Pretty.string_of |
521 (pretty_counterex (Proof.context_of state) false r))); |
521 (pretty_counterex (Proof.context_of state) false r))); |
522 |
522 |
523 val parse_arg = |
523 val parse_arg = |
524 Parse.name -- |
524 Parse.name -- |
525 (Scan.optional (Parse.$$$ "=" |-- |
525 (Scan.optional (@{keyword "="} |-- |
526 (((Parse.name || Parse.float_number) >> single) || |
526 (((Parse.name || Parse.float_number) >> single) || |
527 (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]); |
527 (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}))) ["true"]); |
528 |
528 |
529 val parse_args = |
529 val parse_args = |
530 Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]" || Scan.succeed []; |
530 @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed []; |
531 |
531 |
532 val _ = |
532 val _ = |
533 Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl |
533 Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl |
534 (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args))); |
534 (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args))); |
535 |
535 |