# HG changeset patch
# User wenzelm
# Date 1637431103 -3600
# Node ID 6424f74fd9d4cec9202a34d7e078baf69f0e01a6
# Parent  d6ce4ce20422308e6f5523c91923c5e96577a1ff
Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.;

diff -r d6ce4ce20422 -r 6424f74fd9d4 NEWS
--- a/NEWS	Sat Nov 20 18:15:09 2021 +0100
+++ b/NEWS	Sat Nov 20 18:58:23 2021 +0100
@@ -114,6 +114,11 @@
 * Option "document_echo" informs about document file names during
 session presentation.
 
+* Option "document_heading_prefix" specifies a prefix for the LaTeX
+macro names generated from document heading commands like 'chapter',
+'section' etc. The default is "isamarkup", so 'section' becomes
+"\isamarkupsection" for example.
+
 * The command-line tool "isabelle latex" has been discontinued,
 INCOMPATIBILITY for old document build scripts.
 
diff -r d6ce4ce20422 -r 6424f74fd9d4 etc/options
--- a/etc/options	Sat Nov 20 18:15:09 2021 +0100
+++ b/etc/options	Sat Nov 20 18:58:23 2021 +0100
@@ -21,6 +21,8 @@
   -- "document build engine (e.g. lualatex, pdflatex, build)"
 option document_logo : string = ""
   -- "generate named instance of Isabelle logo (underscore means unnamed variant)"
+option document_heading_prefix : string = "isamarkup"
+  -- "prefix for LaTeX macros generated from 'chapter', 'section' etc."
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"
diff -r d6ce4ce20422 -r 6424f74fd9d4 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Sat Nov 20 18:15:09 2021 +0100
+++ b/src/Pure/Thy/document_build.scala	Sat Nov 20 18:58:23 2021 +0100
@@ -335,7 +335,7 @@
   abstract class Bash_Engine(name: String) extends Engine(name)
   {
     def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory =
-      context.prepare_directory(dir, doc, new Latex.Output)
+      context.prepare_directory(dir, doc, new Latex.Output(context.options))
 
     def use_pdflatex: Boolean = false
     def latex_script(context: Context, directory: Directory): String =
diff -r d6ce4ce20422 -r 6424f74fd9d4 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Sat Nov 20 18:15:09 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Sat Nov 20 18:58:23 2021 +0100
@@ -73,7 +73,7 @@
     if (file_pos.isEmpty) Nil
     else List("\\endinput\n", position(Markup.FILE, file_pos))
 
-  class Output
+  class Output(options: Options)
   {
     def latex_output(latex_text: Text): String = apply(latex_text)
 
@@ -87,7 +87,7 @@
       XML.enclose("%\n\\begin{" + name + "}%\n", "%\n\\end{" + name + "}", body)
 
     def latex_heading(kind: String, body: Text): Text =
-      XML.enclose("%\n\\isamarkup" + kind + "{", "%\n}\n", body)
+      XML.enclose("%\n\\" + options.string("document_heading_prefix") + kind + "{", "%\n}\n", body)
 
     def latex_body(kind: String, body: Text): Text =
       latex_environment("isamarkup" + kind, body)