Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/src/token_markup.scala
changeset 43460 2852f309174a
parent 43458 b55a273ede18
child 43464 265d9300d523 
--- a/src/Tools/jEdit/src/token_markup.scala	Sun Jun 19 15:31:16 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun Jun 19 21:34:55 2011 +0200
@@ -25,17 +25,18 @@
 
   def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
   def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
-  val hidden: Byte = (3 * plain_range).toByte
+  def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
+  val hidden: Byte = (4 * plain_range).toByte
 
   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>
       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 (symbols.is_bold_decoded(sym)) Some(bold(_))
         else None
 
       var result = Map[Text.Offset, Byte => Byte]()
isabelle