# HG changeset patch
# User wenzelm
# Date 1308485466 -7200
# Node ID 4b4b93672f15dae0f6047b67f281ef020c9626c2
# Parent  71b7a535cf9619d0a1d85c311e255d6973f5ca33
some unicode chars for special control symbols;

diff -r 71b7a535cf96 -r 4b4b93672f15 etc/symbols
--- 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
 
diff -r 71b7a535cf96 -r 4b4b93672f15 src/Pure/General/symbol.scala
--- 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
   }
 }
diff -r 71b7a535cf96 -r 4b4b93672f15 src/Pure/Isar/outer_syntax.scala
--- 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)
 
diff -r 71b7a535cf96 -r 4b4b93672f15 src/Pure/Thy/html.scala
--- 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
diff -r 71b7a535cf96 -r 4b4b93672f15 src/Tools/jEdit/src/html_panel.scala
--- 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(
diff -r 71b7a535cf96 -r 4b4b93672f15 src/Tools/jEdit/src/token_markup.scala
--- 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 = ""
         }