equal
deleted
inserted
replaced
55 Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
55 Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
56 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); |
56 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); |
57 in Pretty.writeln p end; |
57 in Pretty.writeln p end; |
58 |
58 |
59 val opt_modes = |
59 val opt_modes = |
60 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) []; |
60 Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []; |
61 |
61 |
62 val opt_evaluator = |
62 val opt_evaluator = |
63 Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]") |
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 "value" "evaluate and print term" Keyword.diag |
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 |