# HG changeset patch
# User wenzelm
# Date 1646309305 -3600
# Node ID 596e77cda1698c319b21ae3c7793ba02d23a027b
# Parent  5a9932dbaf1f31d234caad528f7985f138f814db
clarified signature;

diff -r 5a9932dbaf1f -r 596e77cda169 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Thu Mar 03 12:40:37 2022 +0100
+++ b/src/Pure/General/completion.scala	Thu Mar 03 13:08:25 2022 +0100
@@ -320,7 +320,7 @@
   /* abbreviations */
 
   private def symbol_abbrevs: Thy_Header.Abbrevs =
-    for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
+    for ((sym, abbr) <- Symbol.symbols.abbrevs.toList) yield (abbr, sym)
 
   private val antiquote = "@{"
 
@@ -346,7 +346,7 @@
 {
   /* keywords */
 
-  private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
+  private def is_symbol(name: String): Boolean = Symbol.symbols.names.isDefinedAt(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,7 +367,7 @@
   def add_symbols: Completion =
   {
     val words =
-      Symbol.names.toList.flatMap({ case (sym, (name, argument)) =>
+      Symbol.symbols.names.toList.flatMap({ case (sym, (name, argument)) =>
         val word = "\\" + name
         val seps =
           if (argument == Symbol.Argument.cartouche) List("")
diff -r 5a9932dbaf1f -r 596e77cda169 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Mar 03 12:40:37 2022 +0100
+++ b/src/Pure/General/symbol.scala	Thu Mar 03 13:08:25 2022 +0100
@@ -308,11 +308,11 @@
     val Prop = new Properties.String("argument")
   }
 
-  private lazy val symbols: Symbols = Symbols.init()
+  lazy val symbols: Symbols = Symbols.load()
 
-  private object Symbols
+  object Symbols
   {
-    def init(): Symbols =
+    def load(): Symbols =
     {
       val contents =
         for (path <- Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS")) if path.is_file)
@@ -359,7 +359,7 @@
     }
   }
 
-  private class Symbols(symbols: List[(Symbol, Properties.T)])
+  class Symbols(symbols: List[(Symbol, Properties.T)])
   {
     /* basic properties */
 
@@ -386,6 +386,15 @@
       }).groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
         .sortBy(_._1)
 
+    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 abbrevs: Multi_Map[Symbol, String] =
       Multi_Map((
         for {
@@ -411,6 +420,8 @@
       }
     }
 
+    lazy val is_code: Int => Boolean = codes.map(_._2).toSet
+
 
     /* recoding */
 
@@ -446,6 +457,8 @@
     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
 
+    def lookup_font(sym: Symbol): Option[Int] = fonts.get(sym).map(font_index(_))
+
 
     /* classification */
 
@@ -519,21 +532,6 @@
 
   /* tables */
 
-  def properties: Map[Symbol, Properties.T] = symbols.properties
-  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
-  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))
-    })
-  }
-
-  lazy val is_code: Int => Boolean = codes.map(_._2).toSet
   def decode(text: String): String = symbols.decode(text)
   def encode(text: String): String = symbols.encode(text)
 
@@ -560,11 +558,6 @@
   def output(unicode_symbols: Boolean, text: String): String =
     if (unicode_symbols) Symbol.decode(text) else Symbol.encode(text)
 
-  def fonts: Map[Symbol, String] = symbols.fonts
-  def font_names: List[String] = symbols.font_names
-  def font_index: Map[String, Int] = symbols.font_index
-  def lookup_font(sym: Symbol): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
-
 
   /* classification */
 
diff -r 5a9932dbaf1f -r 596e77cda169 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Thu Mar 03 12:40:37 2022 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Thu Mar 03 13:08:25 2022 +0100
@@ -161,7 +161,7 @@
         "completionProvider" -> JSON.Object(
           "resolveProvider" -> false,
           "triggerCharacters" ->
-            Symbol.abbrevs.values.flatMap(_.iterator).map(_.toString).toList.distinct
+            Symbol.symbols.abbrevs.values.flatMap(_.iterator).map(_.toString).toList.distinct
         ),
         "hoverProvider" -> true,
         "definitionProvider" -> true,
@@ -633,12 +633,12 @@
     def apply(): JSON.T =
     {
       val entries =
-        for ((sym, code) <- Symbol.codes)
+        for ((sym, code) <- Symbol.symbols.codes)
         yield JSON.Object(
           "symbol" -> sym,
-          "name" -> Symbol.names(sym)._1,
+          "name" -> Symbol.symbols.names(sym)._1,
           "code" -> code,
-          "abbrevs" -> Symbol.abbrevs.get_list(sym)
+          "abbrevs" -> Symbol.symbols.abbrevs.get_list(sym)
         )
       Notification("PIDE/symbols", JSON.Object("entries" -> entries))
     }
diff -r 5a9932dbaf1f -r 596e77cda169 src/Tools/jEdit/src/isabelle_encoding.scala
--- a/src/Tools/jEdit/src/isabelle_encoding.scala	Thu Mar 03 12:40:37 2022 +0100
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Thu Mar 03 13:08:25 2022 +0100
@@ -36,7 +36,7 @@
   {
     val source = (new BufferedSource(in)(codec)).mkString
 
-    if (strict && Codepoint.iterator(source).exists(Symbol.is_code))
+    if (strict && Codepoint.iterator(source).exists(Symbol.symbols.is_code))
       throw new CharacterCodingException()
 
     new CharArrayReader(Symbol.decode(source).toArray)
diff -r 5a9932dbaf1f -r 596e77cda169 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Thu Mar 03 12:40:37 2022 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Thu Mar 03 13:08:25 2022 +0100
@@ -86,7 +86,7 @@
     def update_font: Unit =
     {
       font =
-        Symbol.fonts.get(symbol) match {
+        Symbol.symbols.fonts.get(symbol) match {
           case None => GUI.font(size = font_size)
           case Some(font_family) => GUI.font(family = font_family, size = font_size)
         }
@@ -104,7 +104,7 @@
       }
     tooltip =
       GUI.tooltip_lines(
-        cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
+        cat_lines(symbol :: Symbol.symbols.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
   }
 
   private class Reset_Component extends Button
@@ -126,7 +126,7 @@
     layout(search_field) = BorderPanel.Position.North
     layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
 
-    val search_space = for ((sym, _) <- Symbol.codes) yield (sym, Word.lowercase(sym))
+    val search_space = for ((sym, _) <- Symbol.symbols.codes) yield (sym, Word.lowercase(sym))
     val search_delay =
       Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
         val search_words = Word.explode(Word.lowercase(search_field.text))
@@ -153,7 +153,7 @@
     pages += new TabbedPane.Page("abbrevs", abbrevs_panel)
 
     pages ++=
-      Symbol.groups_code.map({ case (group, symbols) =>
+      Symbol.symbols.groups_code.map({ case (group, symbols) =>
         val control = group == "control"
         new TabbedPane.Page(group,
           new ScrollPane(Wrap_Panel(
diff -r 5a9932dbaf1f -r 596e77cda169 src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Thu Mar 03 12:40:37 2022 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala	Thu Mar 03 13:08:25 2022 +0100
@@ -84,9 +84,9 @@
   object Main_Extender extends SyntaxUtilities.StyleExtender
   {
     val max_user_fonts = 2
-    if (Symbol.font_names.length > max_user_fonts)
+    if (Symbol.symbols.font_names.length > max_user_fonts)
       error("Too many user symbol fonts (" + max_user_fonts + " permitted): " +
-        Symbol.font_names.mkString(", "))
+        Symbol.symbols.font_names.mkString(", "))
 
     override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
     {
@@ -102,7 +102,7 @@
         new_styles(bold(i.toByte)) = bold_style(style)
         for (idx <- 0 until max_user_fonts)
           new_styles(user_font(idx, i.toByte)) = style
-        for ((family, idx) <- Symbol.font_index)
+        for ((family, idx) <- Symbol.symbols.font_index)
           new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family))
       }
       new_styles(hidden) =
@@ -140,7 +140,7 @@
 
       if (control_style(sym).isDefined) control_sym = sym
       else if (control_sym != "") {
-        if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
+        if (Symbol.is_controllable(sym) && !Symbol.symbols.fonts.isDefinedAt(sym)) {
           mark(offset - control_sym.length, offset, _ => hidden)
           mark(offset, end_offset, control_style(control_sym).get)
         }
@@ -155,7 +155,7 @@
         mark(b, end_offset, _ => hidden)
       }
 
-      Symbol.lookup_font(sym) match {
+      Symbol.symbols.lookup_font(sym) match {
         case Some(idx) => mark(offset, end_offset, user_font(idx, _))
         case _ =>
       }