Theory Alternative_Headings

(*  Title:      Pure/ex/Alternative_Headings.thy
    Author:     Makarius
*)

chapter ‹Alternative document headings›

theory Alternative_Headings
  imports Pure
  keywords
    "chapter*" "section*" "subsection*" "subsubsection*" :: document_heading
begin

ML ‹
local

fun alternative_heading name body =
  [XML.Elem (Markup.latex_heading (unsuffix "*" name) |> Markup.optional_argument "*", body)];

fun document_heading (name, pos) =
  Outer_Syntax.command (name, pos) (name ^ " heading")
    (Parse.opt_target -- Parse.document_source --| Scan.option (Parse.$$$ ";") >>
      Document_Output.document_output
        {markdown = false, markup = alternative_heading name});

val _ =
  List.app document_heading
   [\<^command_keyword>‹chapter*›,
    \<^command_keyword>‹section*›,
    \<^command_keyword>‹subsection*›,
    \<^command_keyword>‹subsubsection*›];

in end›

end