# HG changeset patch
# User wenzelm
# Date 1693320557 -7200
# Node ID 604a7377725c93bacd9cb9e16796583d1f9de93e
# Parent  afb83ba8d24c0f95b7549cfe9ff43ff756427e9d
clarified signature: prefer enum types;

diff -r afb83ba8d24c -r 604a7377725c src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Tue Aug 29 16:42:08 2023 +0200
+++ b/src/Pure/Thy/latex.scala	Tue Aug 29 16:49:17 2023 +0200
@@ -93,9 +93,7 @@
   /* tags */
 
   object Tags {
-    object Op extends Enumeration {
-      val fold, drop, keep = Value
-    }
+    enum Op { case fold, drop, keep }
 
     val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
 
@@ -103,7 +101,7 @@
 
     def apply(spec: String): Tags =
       new Tags(spec,
-        (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op.Value]) {
+        (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op]) {
           case (m, tag) =>
             tag.toList match {
               case '/' :: cs => m + (cs.mkString -> Op.fold)
@@ -116,10 +114,10 @@
     val empty: Tags = apply("")
   }
 
-  class Tags private(spec: String, map: TreeMap[String, Tags.Op.Value]) {
+  class Tags private(spec: String, map: TreeMap[String, Tags.Op]) {
     override def toString: String = spec
 
-    def get(name: String): Option[Tags.Op.Value] = map.get(name)
+    def get(name: String): Option[Tags.Op] = map.get(name)
 
     def sty(comment_latex: Boolean): File.Content = {
       val path = Path.explode("isabelletags.sty")