1040 Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
1040 Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
1041 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) () |
1041 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) () |
1042 end |> Pretty.writeln |
1042 end |> Pretty.writeln |
1043 |
1043 |
1044 |
1044 |
1045 (* renewing the values command for Prolog queries *) |
1045 (* values command for Prolog queries *) |
1046 |
1046 |
1047 val opt_print_modes = |
1047 val opt_print_modes = |
1048 Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [] |
1048 Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [] |
1049 |
1049 |
1050 val _ = |
1050 val _ = |
1051 Outer_Syntax.improper_command @{command_spec "values"} |
1051 Outer_Syntax.improper_command @{command_spec "values_prolog"} |
1052 "enumerate and print comprehensions" |
1052 "enumerate and print comprehensions" |
1053 (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term |
1053 (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term |
1054 >> (fn ((print_modes, soln), t) => Toplevel.keep |
1054 >> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t))) |
1055 (values_cmd print_modes soln t))) (*FIXME does not preserve the previous functionality*) |
|
1056 |
1055 |
1057 |
1056 |
1058 (* quickcheck generator *) |
1057 (* quickcheck generator *) |
1059 |
1058 |
1060 (* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *) |
1059 (* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *) |