example: alternative document headings, based on more general document output markup;

--- a/src/Pure/PIDE/markup.ML	Tue Nov 23 20:46:40 2021 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Nov 23 21:02:13 2021 +0100
@@ -159,6 +159,7 @@
   val latex_index_entryN: string val latex_index_entry: string -> T
   val latex_delimN: string val latex_delim: string -> T
   val latex_tagN: string val latex_tag: string -> T
+  val optional_argumentN: string val optional_argument: string -> T -> T
   val markdown_paragraphN: string val markdown_paragraph: T
   val markdown_itemN: string val markdown_item: T
   val markdown_bulletN: string val markdown_bullet: int -> T
@@ -595,6 +596,9 @@
 val (latex_delimN, latex_delim) = markup_string "latex_delim" nameN;
 val (latex_tagN, latex_tag) = markup_string "latex_tag" nameN;
 
+val optional_argumentN = "optional_argument";
+fun optional_argument arg = properties [(optional_argumentN, arg)];
+
 
 (* Markdown document structure *)
 

--- a/src/Pure/PIDE/markup.scala	Tue Nov 23 20:46:40 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Nov 23 21:02:13 2021 +0100
@@ -383,6 +383,8 @@
   val Latex_Index_Item = new Markup_Elem("latex_index_item")
   val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND)
 
+  val Optional_Argument = new Properties.String("optional_argument")
+
 
   /* Markdown document structure */
 

--- a/src/Pure/ROOT	Tue Nov 23 20:46:40 2021 +0100
+++ b/src/Pure/ROOT	Tue Nov 23 21:02:13 2021 +0100
@@ -26,11 +26,16 @@
   description "
     Miscellaneous examples and experiments for Isabelle/Pure.
   "
+  options [document_heading_prefix = ""]
   sessions
     "Pure-Examples"
-  theories
+  theories [document = false]
     Def
     Def_Examples
     Guess
     Guess_Examples
-
+  theories
+    Alternative_Headings
+    Alternative_Headings_Examples
+  document_files
+    "root.tex"

--- a/src/Pure/Thy/latex.scala	Tue Nov 23 20:46:40 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Tue Nov 23 21:02:13 2021 +0100
@@ -116,10 +116,15 @@
     def latex_environment(name: String, body: Text): Text =
       XML.enclose("%\n\\begin{" + name + "}%\n", "%\n\\end{" + name + "}", body)
 
-    def latex_heading(kind: String, pos: Position.T, body: Text): Text =
-      XML.enclose("%\n\\" + options.string("document_heading_prefix") + kind + "{", "%\n}\n", body)
+    def latex_heading(kind: String, props: Properties.T, body: Text): Text =
+    {
+      val prefix =
+        "%\n\\" + options.string("document_heading_prefix") + kind +
+        Markup.Optional_Argument.get(props)
+      XML.enclose(prefix + "{", "%\n}\n", body)
+    }
 
-    def latex_body(kind: String, pos: Position.T, body: Text): Text =
+    def latex_body(kind: String, props: Properties.T, body: Text): Text =
       latex_environment("isamarkup" + kind, body)
 
     def latex_delim(name: String, body: Text): Text =
@@ -178,9 +183,9 @@
           case XML.Elem(Markup.Latex_Environment(name), body) =>
             traverse(latex_environment(name, body))
           case XML.Elem(markup @ Markup.Latex_Heading(kind), body) =>
-            traverse(latex_heading(kind, markup.position_properties, body))
+            traverse(latex_heading(kind, markup.properties, body))
           case XML.Elem(markup @ Markup.Latex_Body(kind), body) =>
-            traverse(latex_body(kind, markup.position_properties, body))
+            traverse(latex_body(kind, markup.properties, body))
           case XML.Elem(Markup.Latex_Delim(name), body) =>
             traverse(latex_delim(name, body))
           case XML.Elem(Markup.Latex_Tag(name), body) =>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ex/Alternative_Headings.thy	Tue Nov 23 21:02:13 2021 +0100
@@ -0,0 +1,35 @@
+(*  Title:      Pure/ex/Alternative_Headings.thy
+    Author:     Makarius
+*)
+
+chapter \<open>Alternative document headings\<close>
+
+theory Alternative_Headings
+  imports Pure
+  keywords
+    "chapter*" "section*" "subsection*" "subsubsection*" :: document_heading
+begin
+
+ML \<open>
+local
+
+fun alternative_heading name pos body =
+  let val markup = Markup.latex_heading (unsuffix "*" name) |> Markup.optional_argument "*";
+  in [XML.Elem (markup |> Position.markup pos, body)] end;
+
+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>\<open>chapter*\<close>,
+    \<^command_keyword>\<open>section*\<close>,
+    \<^command_keyword>\<open>subsection*\<close>,
+    \<^command_keyword>\<open>subsubsection*\<close>];
+
+in end\<close>
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ex/Alternative_Headings_Examples.thy	Tue Nov 23 21:02:13 2021 +0100
@@ -0,0 +1,23 @@
+(*  Title:      Pure/ex/Alternative_Headings_Examples.thy
+    Author:     Makarius
+*)
+
+chapter \<open>Some examples of alternative document headings\<close>
+
+theory Alternative_Headings_Examples
+  imports Alternative_Headings
+begin
+
+section \<open>Regular section\<close>
+
+subsection \<open>Regular subsection\<close>
+
+subsubsection \<open>Regular subsubsection\<close>
+
+subsubsection* \<open>Alternative subsubsection\<close>
+
+subsection* \<open>Alternative subsection\<close>
+
+section* \<open>Alternative section\<close>
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ex/document/root.tex	Tue Nov 23 21:02:13 2021 +0100
@@ -0,0 +1,20 @@
+\documentclass[10pt,a4paper]{report}
+\usepackage[T1]{fontenc}
+\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
+
+\isabellestyle{sltt}
+\usepackage{pdfsetup}\urlstyle{rm}
+
+
+\hyphenation{Isabelle}
+
+\begin{document}
+
+\title{Miscellaneous examples and experiments for Isabelle/Pure}
+\maketitle
+
+\parindent 0pt \parskip 0.5ex
+
+\input{session}
+
+\end{document}