src/Pure/Syntax/printer.ML
changeset 81552 4717d3bf5752
parent 81200 0123c6c8f38a
child 81743 fac2045e61d5
equal deleted inserted replaced
81551:a296642fa0a5 81552:4717d3bf5752
    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