Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.;
--- 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.
--- 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"
--- 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 =
--- 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)