# HG changeset patch
# User wenzelm
# Date 1637791053 -3600
# Node ID 4faf0ec33cbf1160dd270637e66e27d7764712b7
# Parent  3bf746911da10a8940533ff5ca818839c54ab445
option document_comment_latex supports e.g. Dagstuhl LIPIcs;

diff -r 3bf746911da1 -r 4faf0ec33cbf NEWS
--- a/NEWS	Wed Nov 24 21:04:39 2021 +0100
+++ b/NEWS	Wed Nov 24 22:57:33 2021 +0100
@@ -111,6 +111,10 @@
 explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
 adjust session ROOT options.
 
+* Option "document_comment_latex" enables regular LaTeX comment.sty,
+instead of the historic version for plain TeX (default). The latter is
+much faster, but in conflict with LaTeX classes like Dagstuhl LIPIcs.
+
 * Option "document_echo" informs about document file names during
 session presentation.
 
diff -r 3bf746911da1 -r 4faf0ec33cbf etc/options
--- a/etc/options	Wed Nov 24 21:04:39 2021 +0100
+++ b/etc/options	Wed Nov 24 22:57:33 2021 +0100
@@ -23,6 +23,8 @@
   -- "generate named instance of Isabelle logo (underscore means unnamed variant)"
 option document_heading_prefix : string = "isamarkup" (standard)
   -- "prefix for LaTeX macros generated from 'chapter', 'section' etc."
+option document_comment_latex : bool = false
+  -- "use regular LaTeX version of comment.sty, instead of historic plain TeX version"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"
diff -r 3bf746911da1 -r 4faf0ec33cbf src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Wed Nov 24 21:04:39 2021 +0100
+++ b/src/Pure/Thy/document_build.scala	Wed Nov 24 22:57:33 2021 +0100
@@ -118,9 +118,11 @@
 
   /* context */
 
+  val texinputs: Path = Path.explode("~~/lib/texinputs")
+
   val isabelle_styles: List[Path] =
-    List("comment.sty", "isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
-      map(name => Path.explode("~~/lib/texinputs") + Path.basic(name))
+    List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
+      map(name => texinputs + Path.basic(name))
 
   def context(
     session: String,
@@ -221,7 +223,12 @@
       /* actual sources: with SHA1 digest */
 
       isabelle_styles.foreach(Isabelle_System.copy_file(_, doc_dir))
-      doc.tags.sty.write(doc_dir)
+
+      val comment_latex = options.bool("document_comment_latex")
+      if (!comment_latex) {
+        Isabelle_System.copy_file(texinputs + Path.basic("comment.sty"), doc_dir)
+      }
+      doc.tags.sty(comment_latex).write(doc_dir)
 
       for ((base_dir, src) <- info.document_files) {
         Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir)
diff -r 3bf746911da1 -r 4faf0ec33cbf src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Wed Nov 24 21:04:39 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Wed Nov 24 22:57:33 2021 +0100
@@ -129,17 +129,19 @@
 
     def get(name: String): Option[Tags.Op.Value] = map.get(name)
 
-    def sty: File.Content =
+    def sty(comment_latex: Boolean): File.Content =
     {
       val path = Path.explode("isabelletags.sty")
+      val comment =
+        if (comment_latex) """\usepackage{comment}"""
+        else """%plain TeX version of comment package -- much faster!
+\let\isafmtname\fmtname\def\fmtname{plain}
+\usepackage{comment}
+\let\fmtname\isafmtname"""
       val tags =
         (for ((name, op) <- map.iterator)
           yield "\\isa" + op + "tag{" + name + "}").toList
-      File.Content(path, """
-%plain TeX version of comment package -- much faster!
-\let\isafmtname\fmtname\def\fmtname{plain}
-\usepackage{comment}
-\let\fmtname\isafmtname
+      File.Content(path, comment + """
 
 \newcommand{\isakeeptag}[1]%
 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
@@ -186,16 +188,21 @@
     def latex_body(kind: String, body: Text, optional_argument: String = ""): Text =
       latex_environment("isamarkup" + kind, body, optional_argument)
 
-    def latex_delim(name: String, body: Text): Text =
+    def latex_tag(name: String, body: Text, delim: Boolean = false): Text =
     {
       val s = output_name(name)
-      XML.enclose("%\n\\isadelim" + s + "\n", "%\n\\endisadelim" + s + "\n", body)
-    }
-
-    def latex_tag(name: String, body: Text): Text =
-    {
-      val s = output_name(name)
-      XML.enclose("%\n\\isatag" + s + "\n", "%\n\\endisatag" + s + "\n{\\isafold" + s + "}%\n", body)
+      val kind = if (delim) "delim" else "tag"
+      val end = if (delim) "" else "{\\isafold" + s + "}%\n"
+      if (options.bool("document_comment_latex")) {
+        XML.enclose(
+          "%\n\\begin{isa" + kind + s + "}\n",
+          "%\n\\end{isa" + kind + s + "}\n" + end, body)
+      }
+      else {
+        XML.enclose(
+          "%\n\\isa" + kind + s + "\n",
+          "%\n\\endisa" + kind + s + "\n" + end, body)
+      }
     }
 
     def index_item(item: Index_Item.Value): String =
@@ -249,7 +256,7 @@
                 case Markup.Latex_Environment(name) => latex_environment(name, body, a)
                 case Markup.Latex_Heading(kind) => latex_heading(kind, body, a)
                 case Markup.Latex_Body(kind) => latex_body(kind, body, a)
-                case Markup.Latex_Delim(name) => latex_delim(name, body)
+                case Markup.Latex_Delim(name) => latex_tag(name, body, delim = true)
                 case Markup.Latex_Tag(name) => latex_tag(name, body)
                 case Markup.Latex_Index_Entry(_) =>
                   elem match {