equal
deleted
inserted
replaced
107 val command_names = map #1 (Name_Space.markup_table ctxt commands); |
107 val command_names = map #1 (Name_Space.markup_table ctxt commands); |
108 val option_names = map #1 (Name_Space.markup_table ctxt options); |
108 val option_names = map #1 (Name_Space.markup_table ctxt options); |
109 in |
109 in |
110 [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names), |
110 [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names), |
111 Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)] |
111 Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)] |
112 |> Pretty.chunks |> Pretty.writeln |
112 |> Pretty.writeln_chunks |
113 end; |
113 end; |
114 |
114 |
115 fun antiquotation name scan body = |
115 fun antiquotation name scan body = |
116 add_command name |
116 add_command name |
117 (fn src => fn state => fn ctxt => |
117 (fn src => fn state => fn ctxt => |