--- a/etc/symbols Sun Jun 19 00:03:44 2011 +0200
+++ b/etc/symbols Sun Jun 19 14:11:06 2011 +0200
@@ -353,4 +353,9 @@
\<hungarumlaut> code: 0x0002dd
\<spacespace> code: 0x002423 font: Isabelle
\<some> code: 0x0003f5 font: Isabelle
+\<^sub> code: 0x0021e9
+\<^sup> code: 0x0021e7
+\<^isub> code: 0x0021e3
+\<^isup> code: 0x0021e1
+\<^bold> code: 0x002759
--- a/src/Pure/General/symbol.scala Sun Jun 19 00:03:44 2011 +0200
+++ b/src/Pure/General/symbol.scala Sun Jun 19 14:11:06 2011 +0200
@@ -326,7 +326,19 @@
def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
def is_symbolic(sym: String): Boolean =
sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
+
+
+ /* special control symbols */
+
def is_controllable(sym: String): Boolean =
!is_blank(sym) && !sym.startsWith("\\<^") && !is_malformed(sym)
+
+ private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
+ private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
+ val bold_decoded = decode("\\<^bold>")
+
+ def is_subscript_decoded(sym: String): Boolean = subscript_decoded.contains(sym)
+ def is_superscript_decoded(sym: String): Boolean = superscript_decoded.contains(sym)
+ def is_bold_decoded(sym: String): Boolean = sym == bold_decoded
}
}
--- a/src/Pure/Isar/outer_syntax.scala Sun Jun 19 00:03:44 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Sun Jun 19 14:11:06 2011 +0200
@@ -15,14 +15,7 @@
{
protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
- lazy val completion: Completion = // FIXME odd initialization
- new Completion + symbols +
- ("sub", "\\<^sub>") +
- ("sup", "\\<^sup>") +
- ("isub", "\\<^isub>") +
- ("isup", "\\<^isup>") +
- ("bold", "\\<^bold>") +
- ("loc", "\\<^loc>")
+ lazy val completion: Completion = new Completion + symbols // FIXME odd initialization
def keyword_kind(name: String): Option[String] = keywords.get(name)
--- a/src/Pure/Thy/html.scala Sun Jun 19 00:03:44 2011 +0200
+++ b/src/Pure/Thy/html.scala Sun Jun 19 14:11:06 2011 +0200
@@ -50,7 +50,8 @@
def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
- def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
+ def spans(symbols: Symbol.Interpretation,
+ input: XML.Tree, original_data: Boolean = false): XML.Body =
{
def html_spans(tree: XML.Tree): XML.Body =
tree match {
@@ -75,18 +76,18 @@
while (syms.hasNext) {
val s1 = syms.next
def s2() = if (syms.hasNext) syms.next else ""
- s1 match {
- case "\n" => add(XML.elem(BR))
- case "\\<^bsub>" => t ++= s1 // FIXME
- case "\\<^esub>" => t ++= s1 // FIXME
- case "\\<^bsup>" => t ++= s1 // FIXME
- case "\\<^esup>" => t ++= s1 // FIXME
- case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
- case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
- case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
- case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
- case _ => t ++= s1
+ if (s1 == "\n") add(XML.elem(BR))
+ 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 == "\\<^bsub>") t ++= s1 // FIXME
+ else if (s1 == "\\<^esub>") t ++= s1 // FIXME
+ else if (s1 == "\\<^bsup>") t ++= s1 // FIXME
+ else if (s1 == "\\<^esup>") t ++= s1 // FIXME
+ else if (symbols.is_bold_decoded(s1)) {
+ add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
}
+ else if (s1 == "\\<^loc>") { add(hidden(s1)); add(span("loc", List(XML.Text(s2())))) }
+ else t ++= s1
}
flush()
ts.toList
--- a/src/Tools/jEdit/src/html_panel.scala Sun Jun 19 00:03:44 2011 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala Sun Jun 19 14:11:06 2011 +0200
@@ -168,7 +168,7 @@
Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
.map(t =>
XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))),
- HTML.spans(t, true))))
+ HTML.spans(system.symbols, t, true))))
val doc =
builder.parse(
new InputSourceImpl(
--- a/src/Tools/jEdit/src/token_markup.scala Sun Jun 19 00:03:44 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Sun Jun 19 14:11:06 2011 +0200
@@ -27,20 +27,17 @@
def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
val hidden: Byte = (3 * plain_range).toByte
- // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
- // FIXME \\<^bold> \\<^loc>
-
- private val ctrl_styles: Map[String, Byte => Byte] =
- Map(
- "\\<^sub>" -> subscript,
- "\\<^sup>" -> superscript,
- "\\<^isub>" -> subscript,
- "\\<^isup>" -> superscript)
-
private def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
: Map[Text.Offset, Byte => Byte] =
{
if (Isabelle.extended_styles) {
+ // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
+ // FIXME \\<^bold> \\<^loc>
+ 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 None
+
var result = Map[Text.Offset, Byte => Byte]()
def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
{
@@ -49,11 +46,11 @@
var offset = 0
var ctrl = ""
for (sym <- Symbol.iterator(text).map(_.toString)) {
- if (ctrl_styles.isDefinedAt(sym)) ctrl = sym
+ if (ctrl_style(sym).isDefined) ctrl = sym
else if (ctrl != "") {
if (symbols.is_controllable(sym)) {
mark(offset - ctrl.length, offset, _ => hidden)
- mark(offset, offset + sym.length, ctrl_styles(ctrl))
+ mark(offset, offset + sym.length, ctrl_style(ctrl).get)
}
ctrl = ""
}