equal
deleted
inserted
replaced
242 Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
242 Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
243 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) () |
243 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) () |
244 end |> Pretty.writeln; |
244 end |> Pretty.writeln; |
245 |
245 |
246 val opt_modes = |
246 val opt_modes = |
247 Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []; |
247 Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []; |
248 |
248 |
249 val _ = |
249 val _ = |
250 Outer_Syntax.command @{command_keyword approximate} "print approximation of term" |
250 Outer_Syntax.command @{command_keyword approximate} "print approximation of term" |
251 (opt_modes -- Parse.term |
251 (opt_modes -- Parse.term |
252 >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t))); |
252 >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t))); |