--- 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>"))
--- 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