equal
deleted
inserted
replaced
33 in Pretty.writeln p end; |
33 in Pretty.writeln p end; |
34 |
34 |
35 val opt_modes = |
35 val opt_modes = |
36 Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []; |
36 Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []; |
37 |
37 |
38 val opt_evaluator = |
|
39 Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"}) |
|
40 |
|
41 val _ = |
38 val _ = |
42 Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term" |
39 Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term" |
43 (opt_modes -- Parse.term |
40 (opt_modes -- Parse.term |
44 >> (fn (modes, t) => Toplevel.keep (value_cmd modes t))); |
41 >> (fn (modes, t) => Toplevel.keep (value_cmd modes t))); |
45 |
42 |