# HG changeset patch
# User wenzelm
# Date 1646307637 -3600
# Node ID 5a9932dbaf1f31d234caad528f7985f138f814db
# Parent  d6aa59dde5b395359a6050ce9b8935021f8386a8
clarified signature;

diff -r d6aa59dde5b3 -r 5a9932dbaf1f src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Thu Mar 03 12:20:27 2022 +0100
+++ b/src/Pure/General/completion.scala	Thu Mar 03 12:40:37 2022 +0100
@@ -370,8 +370,8 @@
       Symbol.names.toList.flatMap({ case (sym, (name, argument)) =>
         val word = "\\" + name
         val seps =
-          if (argument == Symbol.ARGUMENT_CARTOUCHE) List("")
-          else if (argument == Symbol.ARGUMENT_SPACE_CARTOUCHE) List(" ")
+          if (argument == Symbol.Argument.cartouche) List("")
+          else if (argument == Symbol.Argument.space_cartouche) List(" ")
           else Nil
         List(sym -> sym, word -> sym) :::
           seps.map(sep => word -> (sym + sep + "\\<open>\u0007\\<close>"))
diff -r d6aa59dde5b3 -r 5a9932dbaf1f src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Mar 03 12:20:27 2022 +0100
+++ b/src/Pure/General/symbol.scala	Thu Mar 03 12:40:37 2022 +0100
@@ -295,16 +295,24 @@
 
 
 
-  /** symbol interpretation **/
+  /** defined symbols **/
 
-  val ARGUMENT_CARTOUCHE = "cartouche"
-  val ARGUMENT_SPACE_CARTOUCHE = "space_cartouche"
+  object Argument extends Enumeration
+  {
+    val none, cartouche, space_cartouche = Value
 
-  private lazy val symbols: Interpretation = Interpretation.init()
+    def unapply(s: String): Option[Value] =
+      try { Some(withName(s)) }
+      catch { case _: NoSuchElementException => None}
 
-  private object Interpretation
+    val Prop = new Properties.String("argument")
+  }
+
+  private lazy val symbols: Symbols = Symbols.init()
+
+  private object Symbols
   {
-    def init(): Interpretation =
+    def init(): Symbols =
     {
       val contents =
         for (path <- Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS")) if path.is_file)
@@ -312,7 +320,7 @@
       make(cat_lines(contents))
     }
 
-    def make(symbols_spec: String): Interpretation =
+    def make(symbols_spec: String): Symbols =
     {
       val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
       val Key = new Regex("""(?xs) (.+): """)
@@ -347,26 +355,25 @@
               else ((sym, props) :: list, known + sym)
           }._1
 
-      new Interpretation(symbols)
+      new Symbols(symbols)
     }
   }
 
-  private class Interpretation(symbols: List[(Symbol, Properties.T)])
+  private class Symbols(symbols: List[(Symbol, Properties.T)])
   {
     /* basic properties */
 
     val properties: Map[Symbol, Properties.T] = symbols.toMap
 
-    val names: Map[Symbol, (String, String)] =
+    val names: Map[Symbol, (String, Argument.Value)] =
     {
       val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
-      val Argument = new Properties.String("argument")
-      def argument(sym: Symbol, props: Properties.T): String =
+      def argument(sym: Symbol, props: Properties.T): Argument.Value =
         props match {
-          case Argument(arg) =>
-            if (arg == ARGUMENT_CARTOUCHE || arg == ARGUMENT_SPACE_CARTOUCHE) arg
-            else error("Bad argument: " + quote(arg) + " for symbol " + quote(sym))
-          case _ => ""
+          case Argument.Prop(arg) =>
+            Argument.unapply(arg) getOrElse
+              error("Bad argument: " + quote(arg) + " for symbol " + quote(sym))
+          case _ => Argument.none
         }
       (for ((sym @ Name(a), props) <- symbols.iterator)
         yield sym -> (a, argument(sym, props))).toMap
@@ -513,7 +520,7 @@
   /* tables */
 
   def properties: Map[Symbol, Properties.T] = symbols.properties
-  def names: Map[Symbol, (String, String)] = symbols.names
+  def names: Map[Symbol, (String, Argument.Value)] = symbols.names
   def groups: List[(String, List[Symbol])] = symbols.groups
   def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs
   def codes: List[(Symbol, Int)] = symbols.codes