equal
deleted
inserted
replaced
37 type pretty_ops = |
37 type pretty_ops = |
38 {trf: string -> Proof.context -> Ast.ast list -> Ast.ast, |
38 {trf: string -> Proof.context -> Ast.ast list -> Ast.ast, |
39 constrain_block: Ast.ast -> Markup.output Pretty.block, |
39 constrain_block: Ast.ast -> Markup.output Pretty.block, |
40 constrain_trans: Ast.ast -> Ast.ast -> Pretty.T option, |
40 constrain_trans: Ast.ast -> Ast.ast -> Pretty.T option, |
41 markup_trans: string -> Ast.ast list -> Pretty.T option, |
41 markup_trans: string -> Ast.ast list -> Pretty.T option, |
42 markup: string -> Markup.T list, |
42 markup_syntax: string -> Markup.T list, |
43 extern: string -> xstring} |
43 pretty_entity: string -> Pretty.T} |
44 val pretty: {type_mode: bool, curried: bool} -> Proof.context -> prtab list -> |
44 val pretty: {type_mode: bool, curried: bool} -> Proof.context -> prtab list -> |
45 pretty_ops -> Ast.ast -> Pretty.T list |
45 pretty_ops -> Ast.ast -> Pretty.T list |
46 val type_mode_flags: {type_mode: bool, curried: bool} |
46 val type_mode_flags: {type_mode: bool, curried: bool} |
47 end; |
47 end; |
48 |
48 |
229 type pretty_ops = |
229 type pretty_ops = |
230 {trf: string -> Proof.context -> Ast.ast list -> Ast.ast, |
230 {trf: string -> Proof.context -> Ast.ast list -> Ast.ast, |
231 constrain_block: Ast.ast -> Markup.output Pretty.block, |
231 constrain_block: Ast.ast -> Markup.output Pretty.block, |
232 constrain_trans: Ast.ast -> Ast.ast -> Pretty.T option, |
232 constrain_trans: Ast.ast -> Ast.ast -> Pretty.T option, |
233 markup_trans: string -> Ast.ast list -> Pretty.T option, |
233 markup_trans: string -> Ast.ast list -> Pretty.T option, |
234 markup: string -> Markup.T list, |
234 markup_syntax: string -> Markup.T list, |
235 extern: string -> xstring}; |
235 pretty_entity: string -> Pretty.T}; |
236 |
236 |
237 fun pretty {type_mode, curried} ctxt prtabs (ops: pretty_ops) = |
237 fun pretty {type_mode, curried} ctxt prtabs (ops: pretty_ops) = |
238 let |
238 let |
239 val show_brackets = Config.get ctxt show_brackets; |
239 val show_brackets = Config.get ctxt show_brackets; |
240 |
240 |
281 (case entry of |
281 (case entry of |
282 NONE => |
282 NONE => |
283 if nargs = 0 then |
283 if nargs = 0 then |
284 (case Option.mapPartial constrain_trans constraint of |
284 (case Option.mapPartial constrain_trans constraint of |
285 SOME prt => [prt] |
285 SOME prt => [prt] |
286 | NONE => [Pretty.marks_str (#markup ops a, #extern ops a)]) |
286 | NONE => [#pretty_entity ops a]) |
287 else main p (application (cc, args)) |
287 else main p (application (cc, args)) |
288 | SOME (symbs, n, q) => |
288 | SOME (symbs, n, q) => |
289 if nargs = n then parens p q a (symbs, args) constraint |
289 if nargs = n then parens p q a (symbs, args) constraint |
290 else main p (application (split_args n [cc] args))) |
290 else main p (application (split_args n [cc] args))) |
291 end) |
291 end) |
303 val output = |
303 val output = |
304 (case constraint of |
304 (case constraint of |
305 SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) => |
305 SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) => |
306 Pretty.make_block (#constrain_block ops ty) o single |
306 Pretty.make_block (#constrain_block ops ty) o single |
307 | _ => I); |
307 | _ => I); |
308 in #1 (syntax (#markup ops a, output) (symbs', args)) end |
308 in #1 (syntax (#markup_syntax ops a, output) (symbs', args)) end |
309 |
309 |
310 and syntax _ ([], args) = ([], args) |
310 and syntax _ ([], args) = ([], args) |
311 | syntax m (Arg p :: symbs, arg :: args) = |
311 | syntax m (Arg p :: symbs, arg :: args) = |
312 let val (prts, args') = syntax m (symbs, args); |
312 let val (prts, args') = syntax m (symbs, args); |
313 in (main p arg @ prts, args') end |
313 in (main p arg @ prts, args') end |