equal
deleted
inserted
replaced
11 begin |
11 begin |
12 |
12 |
13 ML \<open> |
13 ML \<open> |
14 local |
14 local |
15 |
15 |
16 fun alternative_heading name pos body = |
16 fun alternative_heading name body = |
17 let val markup = Markup.latex_heading (unsuffix "*" name) |> Markup.optional_argument "*"; |
17 [XML.Elem (Markup.latex_heading (unsuffix "*" name) |> Markup.optional_argument "*", body)]; |
18 in [XML.Elem (markup |> Position.markup pos, body)] end; |
|
19 |
18 |
20 fun document_heading (name, pos) = |
19 fun document_heading (name, pos) = |
21 Outer_Syntax.command (name, pos) (name ^ " heading") |
20 Outer_Syntax.command (name, pos) (name ^ " heading") |
22 (Parse.opt_target -- Parse.document_source --| Scan.option (Parse.$$$ ";") >> |
21 (Parse.opt_target -- Parse.document_source --| Scan.option (Parse.$$$ ";") >> |
23 Document_Output.document_output |
22 Document_Output.document_output |