simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
tuned implicit build/init messages;
--- a/src/Pure/General/scan.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/General/scan.scala Thu Jul 07 13:48:30 2011 +0200
@@ -335,11 +335,11 @@
string | (alt_string | (verb | cmt))
}
- private def other_token(symbols: Symbol.Interpretation, is_command: String => Boolean)
+ private def other_token(is_command: String => Boolean)
: Parser[Token] =
{
- val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y }
- val nat = many1(symbols.is_digit)
+ val id = one(Symbol.is_letter) ~ many(Symbol.is_letdig) ^^ { case x ~ y => x + y }
+ val nat = many1(Symbol.is_digit)
val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z }
val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
@@ -355,14 +355,14 @@
("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x))
val sym_ident =
- (many1(symbols.is_symbolic_char) | one(sym => symbols.is_symbolic(sym))) ^^
+ (many1(Symbol.is_symbolic_char) | one(sym => Symbol.is_symbolic(sym))) ^^
(x => Token(Token.Kind.SYM_IDENT, x))
- val space = many1(symbols.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
+ val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
// FIXME check
- val junk = many(sym => !(symbols.is_blank(sym)))
- val junk1 = many1(sym => !(symbols.is_blank(sym)))
+ val junk = many(sym => !(Symbol.is_blank(sym)))
+ val junk1 = many1(sym => !(Symbol.is_blank(sym)))
val bad_delimiter =
("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.UNPARSED, x + y) }
@@ -376,11 +376,10 @@
command_keyword) | bad))
}
- def token(symbols: Symbol.Interpretation, is_command: String => Boolean): Parser[Token] =
- delimited_token | other_token(symbols, is_command)
+ def token(is_command: String => Boolean): Parser[Token] =
+ delimited_token | other_token(is_command)
- def token_context(symbols: Symbol.Interpretation, is_command: String => Boolean, ctxt: Context)
- : Parser[(Token, Context)] =
+ def token_context(is_command: String => Boolean, ctxt: Context): Parser[(Token, Context)] =
{
val string =
quoted_context("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) }
@@ -388,7 +387,7 @@
quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) }
val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
- val other = other_token(symbols, is_command) ^^ { case x => (x, Finished) }
+ val other = other_token(is_command) ^^ { case x => (x, Finished) }
string | (alt_string | (verb | (cmt | other)))
}
--- a/src/Pure/General/symbol.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/General/symbol.scala Thu Jul 07 13:48:30 2011 +0200
@@ -85,7 +85,7 @@
}
- /* efficient iterators */
+ /* iterator */
private val char_symbols: Array[String] =
(0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
@@ -203,9 +203,13 @@
- /** Symbol interpretation **/
+ /** symbol interpretation **/
- class Interpretation(symbol_decls: List[String])
+ private lazy val symbols =
+ new Interpretation(
+ Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS"))))
+
+ private class Interpretation(symbols_spec: String)
{
/* read symbols */
@@ -233,7 +237,7 @@
private val symbols: List[(String, Map[String, String])] =
Map((
- for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
+ for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
yield read_decl(decl)): _*) toList
@@ -299,12 +303,10 @@
val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
- def lookup_font(sym: String): Option[Int] = fonts.get(sym).map(font_index(_))
-
/* classification */
- private val letters = recode_set(
+ val letters = recode_set(
"A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
"N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
"a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
@@ -339,37 +341,20 @@
"\\<^isub>", "\\<^isup>")
- private val blanks =
+ val blanks =
recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
- private val sym_chars =
+ val sym_chars =
Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
- def is_letter(sym: String): Boolean = letters.contains(sym)
- def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
- def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
- def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
- def is_blank(sym: String): Boolean = blanks.contains(sym)
- def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
- def is_symbolic(sym: String): Boolean =
- sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
-
/* control symbols */
- private val ctrl_decoded: Set[String] =
+ val ctrl_decoded: Set[String] =
Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
- def is_ctrl(sym: String): Boolean =
- sym.startsWith("\\<^") || ctrl_decoded.contains(sym)
-
- def is_controllable(sym: String): Boolean =
- !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
-
- private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
- private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
- def is_subscript_decoded(sym: String): Boolean = subscript_decoded.contains(sym)
- def is_superscript_decoded(sym: String): Boolean = superscript_decoded.contains(sym)
+ val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
+ val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
val bold_decoded = decode("\\<^bold>")
val bsub_decoded = decode("\\<^bsub>")
@@ -377,4 +362,47 @@
val bsup_decoded = decode("\\<^bsup>")
val esup_decoded = decode("\\<^esup>")
}
+
+
+ /* tables */
+
+ def names: Map[String, String] = symbols.names
+ def abbrevs: Map[String, String] = symbols.abbrevs
+
+ def decode(text: String): String = symbols.decode(text)
+ def encode(text: String): String = symbols.encode(text)
+
+ def fonts: Map[String, String] = symbols.fonts
+ def font_names: List[String] = symbols.font_names
+ def font_index: Map[String, Int] = symbols.font_index
+ def lookup_font(sym: String): Option[Int] = symbols.fonts.get(sym).map(font_index(_))
+
+
+ /* classification */
+
+ def is_letter(sym: String): Boolean = symbols.letters.contains(sym)
+ def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
+ def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
+ def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
+ def is_blank(sym: String): Boolean = symbols.blanks.contains(sym)
+ def is_symbolic_char(sym: String): Boolean = symbols.sym_chars.contains(sym)
+ def is_symbolic(sym: String): Boolean =
+ sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
+
+
+ /* control symbols */
+
+ def is_ctrl(sym: String): Boolean =
+ sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
+
+ def is_controllable(sym: String): Boolean =
+ !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
+
+ def is_subscript_decoded(sym: String): Boolean = symbols.subscript_decoded.contains(sym)
+ def is_superscript_decoded(sym: String): Boolean = symbols.superscript_decoded.contains(sym)
+ def is_bold_decoded(sym: String): Boolean = sym == symbols.bold_decoded
+ def is_bsub_decoded(sym: String): Boolean = sym == symbols.bsub_decoded
+ def is_esub_decoded(sym: String): Boolean = sym == symbols.esub_decoded
+ def is_bsup_decoded(sym: String): Boolean = sym == symbols.bsup_decoded
+ def is_esup_decoded(sym: String): Boolean = sym == symbols.esup_decoded
}
--- a/src/Pure/Isar/outer_syntax.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Thu Jul 07 13:48:30 2011 +0200
@@ -11,11 +11,11 @@
import scala.collection.mutable
-class Outer_Syntax(symbols: Symbol.Interpretation)
+class Outer_Syntax
{
protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
- lazy val completion: Completion = new Completion + symbols // FIXME odd initialization
+ lazy val completion: Completion = (new Completion).add_symbols // FIXME odd initialization
def keyword_kind(name: String): Option[String] = keywords.get(name)
@@ -24,7 +24,7 @@
val new_keywords = keywords + (name -> kind)
val new_lexicon = lexicon + name
val new_completion = completion + (name, replace)
- new Outer_Syntax(symbols) {
+ new Outer_Syntax {
override val lexicon = new_lexicon
override val keywords = new_keywords
override lazy val completion = new_completion
@@ -66,7 +66,7 @@
{
import lexicon._
- parseAll(rep(token(symbols, is_command)), input) match {
+ parseAll(rep(token(is_command)), input) match {
case Success(tokens, _) => tokens
case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
}
@@ -83,7 +83,7 @@
val toks = new mutable.ListBuffer[Token]
var ctxt = context
while (!in.atEnd) {
- parse(token_context(symbols, is_command, ctxt), in) match {
+ parse(token_context(is_command, ctxt), in) match {
case Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
case NoSuccess(_, rest) =>
error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
--- a/src/Pure/System/isabelle_process.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala Thu Jul 07 13:48:30 2011 +0200
@@ -92,7 +92,7 @@
private def put_result(kind: String, text: String)
{
- put_result(kind, Nil, List(XML.Text(Isabelle_System.symbols.decode(text))))
+ put_result(kind, Nil, List(XML.Text(Symbol.decode(text))))
}
@@ -341,7 +341,7 @@
if (i != n) throw new Protocol_Error("bad message chunk content")
- YXML.parse_body_failsafe(YXML.decode_chars(Isabelle_System.symbols.decode, buf, 0, n))
+ YXML.parse_body_failsafe(YXML.decode_chars(Symbol.decode, buf, 0, n))
//}}}
}
--- a/src/Pure/System/isabelle_system.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Jul 07 13:48:30 2011 +0200
@@ -1,8 +1,8 @@
/* Title: Pure/System/isabelle_system.scala
Author: Makarius
-Fundamental Isabelle system environment: settings, symbols etc.
-Quasi-static module with optional init operation.
+Fundamental Isabelle system environment: quasi-static module with
+optional init operation.
*/
package isabelle
@@ -24,10 +24,7 @@
{
/** implicit state **/
- private case class State(
- standard_system: Standard_System,
- settings: Map[String, String],
- symbols: Symbol.Interpretation)
+ private case class State(standard_system: Standard_System, settings: Map[String, String])
@volatile private var _state: Option[State] = None
@@ -39,7 +36,6 @@
def standard_system: Standard_System = check_state().standard_system
def settings: Map[String, String] = check_state().settings
- def symbols: Symbol.Interpretation = check_state().symbols
/*
isabelle_home precedence:
@@ -51,8 +47,9 @@
if (_state.isEmpty) {
import scala.collection.JavaConversions._
+ System.err.println("### Isabelle system initialization")
+
val standard_system = new Standard_System
-
val settings =
{
val env = Map(System.getenv.toList: _*) +
@@ -89,17 +86,7 @@
("PATH" -> System.getenv("PATH"))
}
}
-
- val symbols =
- {
- val isabelle_symbols = settings.getOrElse("ISABELLE_SYMBOLS", "")
- if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
- val files =
- Path.split(isabelle_symbols).map(p => new File(standard_system.jvm_path(p.implode)))
- new Symbol.Interpretation(split_lines(Standard_System.try_read(files)))
- }
-
- _state = Some(State(standard_system, settings, symbols))
+ _state = Some(State(standard_system, settings))
}
}
--- a/src/Pure/System/session.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/System/session.scala Thu Jul 07 13:48:30 2011 +0200
@@ -117,7 +117,7 @@
@volatile var loaded_theories: Set[String] = Set()
- @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
+ @volatile private var syntax = new Outer_Syntax
def current_syntax(): Outer_Syntax = syntax
@volatile private var reverse_syslog = List[XML.Elem]()
@@ -202,9 +202,7 @@
case Some(command) =>
if (global_state.peek().lookup_command(command.id).isEmpty) {
global_state.change(_.define_command(command))
- prover.get.
- define_command(command.id,
- Isabelle_System.symbols.encode(command.source))
+ prover.get.define_command(command.id, Symbol.encode(command.source))
}
Some(command.id)
}
--- a/src/Pure/System/standard_system.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/System/standard_system.scala Thu Jul 07 13:48:30 2011 +0200
@@ -96,16 +96,6 @@
def read_file(file: File): String = slurp(new FileInputStream(file))
- def try_read(files: Seq[File]): String =
- {
- val buf = new StringBuilder
- for {
- file <- files if file.isFile
- c <- (Source.fromFile(file) ++ Iterator.single('\n'))
- } buf.append(c)
- buf.toString
- }
-
def write_file(file: File, text: CharSequence)
{
val writer =
--- a/src/Pure/Thy/completion.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/Thy/completion.scala Thu Jul 07 13:48:30 2011 +0200
@@ -62,15 +62,15 @@
def + (keyword: String): Completion = this + (keyword, keyword)
- def + (symbols: Symbol.Interpretation): Completion =
+ def add_symbols: Completion =
{
val words =
- (for ((x, _) <- symbols.names) yield (x, x)).toList :::
- (for ((x, y) <- symbols.names) yield (y, x)).toList :::
- (for ((x, y) <- symbols.abbrevs if Completion.is_word(y)) yield (y, x)).toList
+ (for ((x, _) <- Symbol.names) yield (x, x)).toList :::
+ (for ((x, y) <- Symbol.names) yield (y, x)).toList :::
+ (for ((x, y) <- Symbol.abbrevs if Completion.is_word(y)) yield (y, x)).toList
val abbrs =
- (for ((x, y) <- symbols.abbrevs if !Completion.is_word(y))
+ (for ((x, y) <- Symbol.abbrevs if !Completion.is_word(y))
yield (y.reverse.toString, (y, x))).toList
val old = this
--- a/src/Pure/Thy/html.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/Thy/html.scala Thu Jul 07 13:48:30 2011 +0200
@@ -57,8 +57,6 @@
def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
{
- val symbols = Isabelle_System.symbols
-
def html_spans(tree: XML.Tree): XML.Body =
tree match {
case XML.Elem(m @ Markup(name, props), ts) =>
@@ -85,14 +83,14 @@
val s1 = syms.next
def s2() = if (syms.hasNext) syms.next else ""
if (s1 == "\n") add(XML.elem(BR))
- else if (s1 == symbols.bsub_decoded) t ++= s1 // FIXME
- else if (s1 == symbols.esub_decoded) t ++= s1 // FIXME
- else if (s1 == symbols.bsup_decoded) t ++= s1 // FIXME
- else if (s1 == symbols.esup_decoded) t ++= s1 // FIXME
- else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
- else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
- else if (s1 == symbols.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
- else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }
+ else if (Symbol.is_bsub_decoded(s1)) t ++= s1 // FIXME
+ else if (Symbol.is_esub_decoded(s1)) t ++= s1 // FIXME
+ else if (Symbol.is_bsup_decoded(s1)) t ++= s1 // FIXME
+ else if (Symbol.is_esup_decoded(s1)) t ++= s1 // FIXME
+ else if (Symbol.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
+ else if (Symbol.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
+ else if (Symbol.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
+ else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
else t ++= s1
}
flush()
--- a/src/Pure/Thy/thy_header.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala Thu Jul 07 13:48:30 2011 +0200
@@ -75,7 +75,7 @@
def read(reader: Reader[Char]): Header =
{
- val token = lexicon.token(Isabelle_System.symbols, _ => false)
+ val token = lexicon.token(_ => false)
val toks = new mutable.ListBuffer[Token]
@tailrec def scan_to_begin(in: Reader[Char])
--- a/src/Pure/build-jars Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Pure/build-jars Thu Jul 07 13:48:30 2011 +0200
@@ -138,9 +138,7 @@
if [ "$OUTDATED" = true ]
then
- echo "###"
echo "### Building Isabelle/Scala layer ..."
- echo "###"
[ "${#UPDATED[@]}" -gt 0 ] && {
echo "Changed files:"
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Jul 07 13:48:30 2011 +0200
@@ -202,9 +202,7 @@
if [ "$OUTDATED" = true ]
then
- echo "###"
echo "### Building Isabelle/jEdit ..."
- echo "###"
[ "${#UPDATED[@]}" -gt 0 ] && {
echo "Changed files:"
--- a/src/Tools/jEdit/src/isabelle_encoding.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala Thu Jul 07 13:48:30 2011 +0200
@@ -34,7 +34,7 @@
private def text_reader(in: InputStream, codec: Codec): Reader =
{
val source = new BufferedSource(in)(codec)
- new CharArrayReader(Isabelle_System.symbols.decode(source.mkString).toArray)
+ new CharArrayReader(Symbol.decode(source.mkString).toArray)
}
override def getTextReader(in: InputStream): Reader =
@@ -53,7 +53,7 @@
val buffer = new ByteArrayOutputStream(BUFSIZE) {
override def flush()
{
- val text = Isabelle_System.symbols.encode(toString(Standard_System.charset_name))
+ val text = Symbol.encode(toString(Standard_System.charset_name))
out.write(text.getBytes(Standard_System.charset))
out.flush()
}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Jul 07 13:48:30 2011 +0200
@@ -96,7 +96,7 @@
case Some((word, cs)) =>
val ds =
(if (Isabelle_Encoding.is_active(buffer))
- cs.map(Isabelle_System.symbols.decode(_)).sortWith(_ < _)
+ cs.map(Symbol.decode(_)).sortWith(_ < _)
else cs).filter(_ != word)
if (ds.isEmpty) null
else new SideKickCompletion(
--- a/src/Tools/jEdit/src/token_markup.scala Wed Jul 06 23:11:59 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Thu Jul 07 13:48:30 2011 +0200
@@ -81,9 +81,8 @@
class Style_Extender extends SyntaxUtilities.StyleExtender
{
- val symbols = Isabelle_System.symbols
- if (symbols.font_names.length > 2)
- error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", "))
+ if (Symbol.font_names.length > 2)
+ error("Too many user symbol fonts (max 2 permitted): " + Symbol.font_names.mkString(", "))
override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
{
@@ -94,7 +93,7 @@
new_styles(subscript(i.toByte)) = script_style(style, -1)
new_styles(superscript(i.toByte)) = script_style(style, 1)
new_styles(bold(i.toByte)) = bold_style(style)
- for ((family, idx) <- symbols.font_index)
+ for ((family, idx) <- Symbol.font_index)
new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
}
new_styles(hidden) =
@@ -108,13 +107,11 @@
def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
{
- val symbols = Isabelle_System.symbols
-
- // FIXME symbols.bsub_decoded etc.
+ // FIXME Symbol.is_bsub_decoded etc.
def ctrl_style(sym: String): Option[Byte => Byte] =
- if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
- else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))
- else if (sym == symbols.bold_decoded) Some(bold(_))
+ if (Symbol.is_subscript_decoded(sym)) Some(subscript(_))
+ else if (Symbol.is_superscript_decoded(sym)) Some(superscript(_))
+ else if (Symbol.is_bold_decoded(sym)) Some(bold(_))
else None
var result = Map[Text.Offset, Byte => Byte]()
@@ -127,13 +124,13 @@
for (sym <- Symbol.iterator(text)) {
if (ctrl_style(sym).isDefined) ctrl = sym
else if (ctrl != "") {
- if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {
+ if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
mark(offset - ctrl.length, offset, _ => hidden)
mark(offset, offset + sym.length, ctrl_style(ctrl).get)
}
ctrl = ""
}
- symbols.lookup_font(sym) match {
+ Symbol.lookup_font(sym) match {
case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
case _ =>
}