equal
deleted
inserted
replaced
64 (Markup.entity Markup.commandN name); |
64 (Markup.entity Markup.commandN name); |
65 |
65 |
66 fun pretty_command (cmd as (name, Command {comment, ...})) = |
66 fun pretty_command (cmd as (name, Command {comment, ...})) = |
67 Pretty.block |
67 Pretty.block |
68 (Pretty.marks_str |
68 (Pretty.marks_str |
69 ([Sendback.make_markup {implicit = true}, command_markup false cmd], name) :: |
69 ([Sendback.make_markup {implicit = true, properties = [Markup.padding_line]}, |
70 Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); |
70 command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); |
71 |
71 |
72 |
72 |
73 (* parse command *) |
73 (* parse command *) |
74 |
74 |
75 local |
75 local |