# HG changeset patch # User wenzelm # Date 1310039310 -7200 # Node ID 5130dfe1b7beafe187ca4c9c050b02e5b572fa58 # Parent 93dcfcf914848dea333e530761dd616c2c5c1744 simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style"; tuned implicit build/init messages; diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/General/scan.scala --- 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))) } diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/General/symbol.scala --- 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", "\\", "\\<^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 } diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/Isar/outer_syntax.scala --- 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) diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/System/isabelle_process.scala --- 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)) //}}} } diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/System/isabelle_system.scala --- 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)) } } diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/System/session.scala --- 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) } diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/System/standard_system.scala --- 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 = diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/Thy/completion.scala --- 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 diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/Thy/html.scala --- 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() diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/Thy/thy_header.scala --- 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]) diff -r 93dcfcf91484 -r 5130dfe1b7be src/Pure/build-jars --- 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:" diff -r 93dcfcf91484 -r 5130dfe1b7be src/Tools/jEdit/lib/Tools/jedit --- 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:" diff -r 93dcfcf91484 -r 5130dfe1b7be src/Tools/jEdit/src/isabelle_encoding.scala --- 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() } diff -r 93dcfcf91484 -r 5130dfe1b7be src/Tools/jEdit/src/isabelle_sidekick.scala --- 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( diff -r 93dcfcf91484 -r 5130dfe1b7be src/Tools/jEdit/src/token_markup.scala --- 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 _ => }