equal
deleted
inserted
replaced
61 |
61 |
62 val opt_evaluator = |
62 val opt_evaluator = |
63 Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"}) |
63 Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"}) |
64 |
64 |
65 val _ = |
65 val _ = |
66 Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag |
66 Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term" |
67 (opt_evaluator -- opt_modes -- Parse.term |
67 (opt_evaluator -- opt_modes -- Parse.term |
68 >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep |
68 >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep |
69 (value_cmd some_name modes t))); |
69 (value_cmd some_name modes t))); |
70 |
70 |
71 val antiq_setup = |
71 val antiq_setup = |