--- 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("")
--- 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 */
--- 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))
}
--- 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)
--- 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(
--- 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 _ =>
}