# HG changeset patch
# User wenzelm
# Date 1646318391 -3600
# Node ID 29e11ce79a52a37a8a94503fab63df460e6b958b
# Parent  e894577e10d8d6ea9131a716a45154a408560b01
clarified signature;
clarified data structures;

diff -r e894577e10d8 -r 29e11ce79a52 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Thu Mar 03 15:12:38 2022 +0100
+++ b/src/Pure/General/completion.scala	Thu Mar 03 15:39:51 2022 +0100
@@ -346,7 +346,7 @@
 {
   /* keywords */
 
-  private def is_symbol(name: String): Boolean = Symbol.symbols.names.isDefinedAt(name)
+  private def is_symbol(name: String): Boolean = Symbol.symbols.defined(name)
   private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name)
   private def is_keyword_template(name: String, template: Boolean): Boolean =
     is_keyword(name) && (words_map.getOrElse(name, name) != name) == template
@@ -367,12 +367,16 @@
   def add_symbols: Completion =
   {
     val words =
-      Symbol.symbols.names.toList.flatMap({ case (sym, (name, argument)) =>
-        val word = "\\" + name
+      Symbol.symbols.entries.flatMap(entry =>
+      {
+        val sym = entry.symbol
+        val word = "\\" + entry.name
         val seps =
-          if (argument == Symbol.Argument.cartouche) List("")
-          else if (argument == Symbol.Argument.space_cartouche) List(" ")
-          else Nil
+          entry.argument match {
+            case Symbol.Argument.none => Nil
+            case Symbol.Argument.cartouche => List("")
+            case Symbol.Argument.space_cartouche => List(" ")
+          }
         List(sym -> sym, word -> sym) :::
           seps.map(sep => word -> (sym + sep + "\\<open>\u0007\\<close>"))
       })
diff -r e894577e10d8 -r 29e11ce79a52 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Mar 03 15:12:38 2022 +0100
+++ b/src/Pure/General/symbol.scala	Thu Mar 03 15:39:51 2022 +0100
@@ -304,8 +304,64 @@
     def unapply(s: String): Option[Value] =
       try { Some(withName(s)) }
       catch { case _: NoSuchElementException => None}
+  }
 
-    val Prop = new Properties.String("argument")
+  object Entry
+  {
+    private val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
+    private val Argument = new Properties.String("argument")
+    private val Abbrev = new Properties.String("abbrev")
+    private val Code = new Properties.String("code")
+    private val Font = new Properties.String("font")
+    private val Group = new Properties.String("group")
+
+    def apply(symbol: Symbol, props: Properties.T): Entry =
+    {
+      def err(msg: String): Nothing = error(msg + " for symbol " + quote(symbol))
+
+      val name =
+        symbol match { case Name(a) => a case _ => err("Cannot determine name") }
+
+      val argument =
+        props match {
+          case Argument(arg) =>
+            Symbol.Argument.unapply(arg) getOrElse
+              error("Bad argument: " + quote(arg) + " for symbol " + quote(symbol))
+          case _ => Symbol.Argument.none
+        }
+
+      val code =
+        props match {
+          case Code(s) =>
+            try {
+              val code = Integer.decode(s).intValue
+              if (code >= 128) Some(code) else err("Illegal ASCII code")
+            }
+            catch { case _: NumberFormatException => err("Bad code") }
+          case _ => None
+        }
+
+      val groups = proper_list(for ((Group.name, a) <- props) yield a).getOrElse(List("unsorted"))
+
+      val abbrevs = for ((Abbrev.name, a) <- props) yield a
+
+      new Entry(symbol, name, argument, code, Font.unapply(props), groups, abbrevs)
+    }
+  }
+
+  class Entry private(
+    val symbol: Symbol,
+    val name: String,
+    val argument: Symbol.Argument.Value,
+    val code: Option[Int],
+    val font: Option[String],
+    val groups: List[String],
+    val abbrevs: List[String])
+  {
+    override def toString: String = symbol
+
+    val decode: Option[String] =
+      code.map(c => new String(Character.toChars(c)))
   }
 
   lazy val symbols: Symbols = Symbols.load()
@@ -345,82 +401,46 @@
         }
       }
 
-      val symbols: List[(Symbol, Properties.T)] =
+      new Symbols(
         split_lines(symbols_spec).reverse.
-          foldLeft((List.empty[(Symbol, Properties.T)], Set.empty[Symbol])) {
+          foldLeft((List.empty[Entry], Set.empty[Symbol])) {
             case (res, No_Decl()) => res
             case ((list, known), decl) =>
               val (sym, props) = read_decl(decl)
               if (known(sym)) (list, known)
-              else ((sym, props) :: list, known + sym)
-          }._1
-
-      new Symbols(symbols)
+              else (Entry(sym, props) :: list, known + sym)
+          }._1)
     }
   }
 
-  class Symbols(symbols: List[(Symbol, Properties.T)])
+  class Symbols(val entries: List[Entry])
   {
+    override def toString: String = entries.mkString("Symbols(", ", ", ")")
+
+
     /* basic properties */
 
-    val properties: Map[Symbol, Properties.T] = symbols.toMap
+    private val entries_map: Map[Symbol, Entry] =
+      (for (entry <- entries.iterator) yield entry.symbol -> entry).toMap
 
-    val names: Map[Symbol, (String, Argument.Value)] =
-    {
-      val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
-      def argument(sym: Symbol, props: Properties.T): Argument.Value =
-        props match {
-          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
-    }
+    def get(sym: Symbol): Option[Entry] = entries_map.get(sym)
+    def defined(sym: Symbol): Boolean = entries_map.isDefinedAt(sym)
+
+    def defined_code(sym: Symbol): Boolean =
+      get(sym) match { case Some(entry) => entry.code.isDefined case _ => false }
 
-    val groups: List[(String, List[Symbol])] =
-      symbols.flatMap({ case (sym, props) =>
-        val gs = for (("group", g) <- props) yield g
-        if (gs.isEmpty) List(sym -> "unsorted") else gs.map(sym -> _)
-      }).groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
-        .sortBy(_._1)
+    val code_defined: Int => Boolean =
+      (for (entry <- entries.iterator; code <- entry.code) yield code).toSet
 
-    def groups_code: List[(String, List[Symbol])] =
-    {
-      val has_code = codes.iterator.map(_._1).toSet
-      groups.flatMap({ case (group, symbols) =>
-        val symbols1 = symbols.filter(has_code)
-        if (symbols1.isEmpty) None else Some((group, symbols1))
-      })
-    }
+    val groups_code: List[(String, List[Symbol])] =
+      (for {
+        entry <- entries.iterator if entry.code.isDefined
+        group <- entry.groups.iterator
+      } yield entry.symbol -> group)
+        .toList.groupBy(_._2).toList.map({ case (g, list) => (g, list.map(_._1)) }).sortBy(_._1)
 
     val abbrevs: Multi_Map[Symbol, String] =
-      Multi_Map((
-        for {
-          (sym, props) <- symbols
-          ("abbrev", a) <- props.reverse
-        } yield sym -> a): _*)
-
-    val codes: List[(Symbol, Int)] =
-    {
-      val Code = new Properties.String("code")
-      for {
-        (sym, props) <- symbols
-        code <-
-          props match {
-            case Code(s) =>
-              try { Some(Integer.decode(s).intValue) }
-              catch { case _: NumberFormatException => error("Bad code for symbol " + sym) }
-            case _ => None
-          }
-      } yield {
-        if (code < 128) error("Illegal ASCII code for symbol " + sym)
-        else (sym, code)
-      }
-    }
-
-    lazy val is_code: Int => Boolean = codes.map(_._2).toSet
+      Multi_Map((for (entry <- entries; a <- entry.abbrevs.reverse) yield entry.symbol -> a): _*)
 
 
     /* recoding */
@@ -428,7 +448,7 @@
     private val (decoder, encoder) =
     {
       val mapping =
-        for ((sym, code) <- codes) yield (sym, new String(Character.toChars(code)))
+        for (entry <- entries; s <- entry.decode) yield entry.symbol -> s
       (new Recoder(mapping), new Recoder(for ((x, y) <- mapping) yield (y, x)))
     }
 
@@ -450,9 +470,8 @@
 
     /* user fonts */
 
-    private val Font = new Properties.String("font")
     val fonts: Map[Symbol, String] =
-      recode_map((for ((sym, Font(font)) <- symbols) yield sym -> font): _*)
+      recode_map((for (entry <- entries; font <- entry.font) yield entry.symbol -> font): _*)
 
     val font_names: List[String] = fonts.iterator.map(_._2).toSet.toList
     val font_index: Map[String, Int] = (font_names zip font_names.indices.toList).toMap
@@ -500,7 +519,8 @@
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
 
-    val symbolic: Set[String] = recode_set((for {(sym, _) <- symbols; if raw_symbolic(sym)} yield sym): _*)
+    val symbolic: Set[String] =
+      recode_set((for (entry <- entries if raw_symbolic(entry.symbol)) yield entry.symbol): _*)
 
 
     /* misc symbols */
@@ -517,7 +537,8 @@
     /* control symbols */
 
     val control_decoded: Set[Symbol] =
-      (for ((sym, _) <- symbols.iterator if sym.startsWith("\\<^")) yield decode(sym)).toSet
+      (for (entry <- entries.iterator if entry.symbol.startsWith("\\<^"); s <- entry.decode)
+        yield s).toSet
 
     val sub_decoded: Symbol = decode(sub)
     val sup_decoded: Symbol = decode(sup)
diff -r e894577e10d8 -r 29e11ce79a52 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Thu Mar 03 15:12:38 2022 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Thu Mar 03 15:39:51 2022 +0100
@@ -633,12 +633,12 @@
     def apply(): JSON.T =
     {
       val entries =
-        for ((sym, code) <- Symbol.symbols.codes)
+        for (entry <- Symbol.symbols.entries; code <- entry.code)
         yield JSON.Object(
-          "symbol" -> sym,
-          "name" -> Symbol.symbols.names(sym)._1,
+          "symbol" -> entry.symbol,
+          "name" -> entry.name,
           "code" -> code,
-          "abbrevs" -> Symbol.symbols.abbrevs.get_list(sym)
+          "abbrevs" -> entry.abbrevs
         )
       Notification("PIDE/symbols", JSON.Object("entries" -> entries))
     }
diff -r e894577e10d8 -r 29e11ce79a52 src/Tools/jEdit/src/isabelle_encoding.scala
--- a/src/Tools/jEdit/src/isabelle_encoding.scala	Thu Mar 03 15:12:38 2022 +0100
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Thu Mar 03 15:39:51 2022 +0100
@@ -36,7 +36,7 @@
   {
     val source = (new BufferedSource(in)(codec)).mkString
 
-    if (strict && Codepoint.iterator(source).exists(Symbol.symbols.is_code))
+    if (strict && Codepoint.iterator(source).exists(Symbol.symbols.code_defined))
       throw new CharacterCodingException()
 
     new CharArrayReader(Symbol.decode(source).toArray)
diff -r e894577e10d8 -r 29e11ce79a52 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Thu Mar 03 15:12:38 2022 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Thu Mar 03 15:39:51 2022 +0100
@@ -126,7 +126,9 @@
     layout(search_field) = BorderPanel.Position.North
     layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
 
-    val search_space = for ((sym, _) <- Symbol.symbols.codes) yield (sym, Word.lowercase(sym))
+    val search_space =
+      for (entry <- Symbol.symbols.entries if entry.code.isDefined)
+        yield entry.symbol -> Word.lowercase(entry.symbol)
     val search_delay =
       Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
         val search_words = Word.explode(Word.lowercase(search_field.text))