# HG changeset patch
# User wenzelm
# Date 1637784279 -3600
# Node ID 3bf746911da10a8940533ff5ca818839c54ab445
# Parent  4c8d9479f916b7b3e3549c24d1dbb92a4167b381
more explicit type Latex.Tags;
generate isabelletags.sty from Isabelle/Scala, including comment.sty setup;

diff -r 4c8d9479f916 -r 3bf746911da1 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Wed Nov 24 15:33:43 2021 +0100
+++ b/lib/texinputs/isabelle.sty	Wed Nov 24 21:04:39 2021 +0100
@@ -275,29 +275,8 @@
 \newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
 
 
-% tagged regions
-
-%plain TeX version of comment package -- much faster!
-\let\isafmtname\fmtname\def\fmtname{plain}
-\usepackage{comment}
-\let\fmtname\isafmtname
+% tags
 
 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
 
-\newcommand{\isakeeptag}[1]%
-{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
-\newcommand{\isadroptag}[1]%
-{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
-\newcommand{\isafoldtag}[1]%
-{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
-
-\isakeeptag{document}
-\isakeeptag{theory}
-\isakeeptag{proof}
-\isakeeptag{ML}
-\isakeeptag{visible}
-\isadroptag{invisible}
-\isakeeptag{important}
-\isakeeptag{unimportant}
-
 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
diff -r 4c8d9479f916 -r 3bf746911da1 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Wed Nov 24 15:33:43 2021 +0100
+++ b/src/Pure/Thy/document_build.scala	Wed Nov 24 21:04:39 2021 +0100
@@ -21,36 +21,17 @@
 
   object Document_Variant
   {
-    def parse(name: String, tags: String): Document_Variant =
-      Document_Variant(name, Library.space_explode(',', tags))
-
     def parse(opt: String): Document_Variant =
       Library.space_explode('=', opt) match {
-        case List(name) => Document_Variant(name, Nil)
-        case List(name, tags) => parse(name, tags)
+        case List(name) => Document_Variant(name, Latex.Tags.empty)
+        case List(name, tags) => Document_Variant(name, Latex.Tags(tags))
         case _ => error("Malformed document variant: " + quote(opt))
       }
   }
 
-  sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name
+  sealed case class Document_Variant(name: String, tags: Latex.Tags) extends Document_Name
   {
-    def print_tags: String = tags.mkString(",")
-    def print: String = if (tags.isEmpty) name else name + "=" + print_tags
-
-    def isabelletags: File.Content =
-    {
-      val path = Path.explode("isabelletags.sty")
-      val content =
-        Library.terminate_lines(
-          tags.map(tag =>
-            tag.toList match {
-              case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
-              case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
-              case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
-              case cs => "\\isakeeptag{" + cs.mkString + "}"
-            }))
-      File.Content(path, content)
-    }
+    def print: String = if (tags.toString.isEmpty) name else name + "=" + tags.toString
   }
 
   sealed case class Document_Input(name: String, sources: SHA1.Digest)
@@ -240,7 +221,7 @@
       /* actual sources: with SHA1 digest */
 
       isabelle_styles.foreach(Isabelle_System.copy_file(_, doc_dir))
-      doc.isabelletags.write(doc_dir)
+      doc.tags.sty.write(doc_dir)
 
       for ((base_dir, src) <- info.document_files) {
         Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir)
diff -r 4c8d9479f916 -r 3bf746911da1 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Wed Nov 24 15:33:43 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Wed Nov 24 21:04:39 2021 +0100
@@ -11,6 +11,7 @@
 
 import scala.annotation.tailrec
 import scala.collection.mutable
+import scala.collection.immutable.TreeMap
 import scala.util.matching.Regex
 
 
@@ -93,6 +94,65 @@
   }
 
 
+  /* tags */
+
+  object Tags
+  {
+    object Op extends Enumeration
+    {
+      val fold, drop, keep = Value
+    }
+
+    val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
+
+    private def explode(spec: String): List[String] =
+      Library.space_explode(',', spec)
+
+    def apply(spec: String): Tags =
+      new Tags(spec,
+        (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op.Value]) {
+          case (m, tag) =>
+            tag.toList match {
+              case '/' :: cs => m + (cs.mkString -> Op.fold)
+              case '-' :: cs => m + (cs.mkString -> Op.drop)
+              case '+' :: cs => m + (cs.mkString -> Op.keep)
+              case cs => m + (cs.mkString -> Op.keep)
+            }
+        })
+
+    val empty: Tags = apply("")
+  }
+
+  class Tags private(spec: String, map: TreeMap[String, Tags.Op.Value])
+  {
+    override def toString: String = spec
+
+    def get(name: String): Option[Tags.Op.Value] = map.get(name)
+
+    def sty: File.Content =
+    {
+      val path = Path.explode("isabelletags.sty")
+      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
+
+\newcommand{\isakeeptag}[1]%
+{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isadroptag}[1]%
+{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isafoldtag}[1]%
+{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
+
+""" + Library.terminate_lines(tags))
+    }
+  }
+
+
   /* output text and positions */
 
   type Text = XML.Body