# HG changeset patch
# User wenzelm
# Date 1693319969 -7200
# Node ID 1ce1abed508255a57bb0906c0e84554ce615a68b
# Parent  e1a19c7778e04f8a3cfc43ba132f7f854ad10452
clarified signature: prefer enum types;

diff -r e1a19c7778e0 -r 1ce1abed5082 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Aug 29 16:30:07 2023 +0200
+++ b/src/Pure/General/symbol.scala	Tue Aug 29 16:39:29 2023 +0200
@@ -286,13 +286,13 @@
 
   /** defined symbols **/
 
-  object Argument extends Enumeration {
-    val none, cartouche, space_cartouche = Value
+  object Argument {
+    def unapply(s: String): Option[Argument] =
+      try { Some(valueOf(s)) }
+      catch { case _: IllegalArgumentException => None}
+  }
 
-    def unapply(s: String): Option[Value] =
-      try { Some(withName(s)) }
-      catch { case _: NoSuchElementException => None}
-  }
+  enum Argument { case none, cartouche, space_cartouche }
 
   object Entry {
     private val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
@@ -339,7 +339,7 @@
   class Entry private(
     val symbol: Symbol,
     val name: String,
-    val argument: Symbol.Argument.Value,
+    val argument: Symbol.Argument,
     val code: Option[Int],
     val font: Option[String],
     val groups: List[String],