some unicode chars for special control symbols;
authorwenzelm
Sun Jun 19 14:11:06 2011 +0200 (2011-06-19 ago)
changeset 434554b4b93672f15
parent 43454 71b7a535cf96
child 43456 8a6de1a6e1dc
some unicode chars for special control symbols;
etc/symbols
src/Pure/General/symbol.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/Thy/html.scala
src/Tools/jEdit/src/html_panel.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/etc/symbols	Sun Jun 19 00:03:44 2011 +0200
     1.2 +++ b/etc/symbols	Sun Jun 19 14:11:06 2011 +0200
     1.3 @@ -353,4 +353,9 @@
     1.4  \<hungarumlaut>         code: 0x0002dd
     1.5  \<spacespace>           code: 0x002423  font: Isabelle
     1.6  \<some>                 code: 0x0003f5  font: Isabelle
     1.7 +\<^sub>                 code: 0x0021e9
     1.8 +\<^sup>                 code: 0x0021e7
     1.9 +\<^isub>                code: 0x0021e3
    1.10 +\<^isup>                code: 0x0021e1
    1.11 +\<^bold>                code: 0x002759
    1.12  
     2.1 --- a/src/Pure/General/symbol.scala	Sun Jun 19 00:03:44 2011 +0200
     2.2 +++ b/src/Pure/General/symbol.scala	Sun Jun 19 14:11:06 2011 +0200
     2.3 @@ -326,7 +326,19 @@
     2.4      def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
     2.5      def is_symbolic(sym: String): Boolean =
     2.6        sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
     2.7 +
     2.8 +
     2.9 +    /* special control symbols */
    2.10 +
    2.11      def is_controllable(sym: String): Boolean =
    2.12        !is_blank(sym) && !sym.startsWith("\\<^") && !is_malformed(sym)
    2.13 +
    2.14 +    private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
    2.15 +    private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
    2.16 +    val bold_decoded = decode("\\<^bold>")
    2.17 +
    2.18 +    def is_subscript_decoded(sym: String): Boolean = subscript_decoded.contains(sym)
    2.19 +    def is_superscript_decoded(sym: String): Boolean = superscript_decoded.contains(sym)
    2.20 +    def is_bold_decoded(sym: String): Boolean = sym == bold_decoded
    2.21    }
    2.22  }
     3.1 --- a/src/Pure/Isar/outer_syntax.scala	Sun Jun 19 00:03:44 2011 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sun Jun 19 14:11:06 2011 +0200
     3.3 @@ -15,14 +15,7 @@
     3.4  {
     3.5    protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
     3.6    protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
     3.7 -  lazy val completion: Completion = // FIXME odd initialization
     3.8 -    new Completion + symbols +
     3.9 -      ("sub", "\\<^sub>") +
    3.10 -      ("sup", "\\<^sup>") +
    3.11 -      ("isub", "\\<^isub>") +
    3.12 -      ("isup", "\\<^isup>") +
    3.13 -      ("bold", "\\<^bold>") +
    3.14 -      ("loc", "\\<^loc>")
    3.15 +  lazy val completion: Completion = new Completion + symbols // FIXME odd initialization
    3.16  
    3.17    def keyword_kind(name: String): Option[String] = keywords.get(name)
    3.18  
     4.1 --- a/src/Pure/Thy/html.scala	Sun Jun 19 00:03:44 2011 +0200
     4.2 +++ b/src/Pure/Thy/html.scala	Sun Jun 19 14:11:06 2011 +0200
     4.3 @@ -50,7 +50,8 @@
     4.4    def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
     4.5    def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
     4.6  
     4.7 -  def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
     4.8 +  def spans(symbols: Symbol.Interpretation,
     4.9 +    input: XML.Tree, original_data: Boolean = false): XML.Body =
    4.10    {
    4.11      def html_spans(tree: XML.Tree): XML.Body =
    4.12        tree match {
    4.13 @@ -75,18 +76,18 @@
    4.14            while (syms.hasNext) {
    4.15              val s1 = syms.next
    4.16              def s2() = if (syms.hasNext) syms.next else ""
    4.17 -            s1 match {
    4.18 -              case "\n" => add(XML.elem(BR))
    4.19 -              case "\\<^bsub>" => t ++= s1  // FIXME
    4.20 -              case "\\<^esub>" => t ++= s1  // FIXME
    4.21 -              case "\\<^bsup>" => t ++= s1  // FIXME
    4.22 -              case "\\<^esup>" => t ++= s1  // FIXME
    4.23 -              case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
    4.24 -              case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
    4.25 -              case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    4.26 -              case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
    4.27 -              case _ => t ++= s1
    4.28 +            if (s1 == "\n") add(XML.elem(BR))
    4.29 +            else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    4.30 +            else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    4.31 +            else if (s1 == "\\<^bsub>") t ++= s1  // FIXME
    4.32 +            else if (s1 == "\\<^esub>") t ++= s1  // FIXME
    4.33 +            else if (s1 == "\\<^bsup>") t ++= s1  // FIXME
    4.34 +            else if (s1 == "\\<^esup>") t ++= s1  // FIXME
    4.35 +            else if (symbols.is_bold_decoded(s1)) {
    4.36 +              add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    4.37              }
    4.38 +            else if (s1 == "\\<^loc>") { add(hidden(s1)); add(span("loc", List(XML.Text(s2())))) }
    4.39 +            else t ++= s1
    4.40            }
    4.41            flush()
    4.42            ts.toList
     5.1 --- a/src/Tools/jEdit/src/html_panel.scala	Sun Jun 19 00:03:44 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Sun Jun 19 14:11:06 2011 +0200
     5.3 @@ -168,7 +168,7 @@
     5.4            Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
     5.5              .map(t =>
     5.6                XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))),
     5.7 -                HTML.spans(t, true))))
     5.8 +                HTML.spans(system.symbols, t, true))))
     5.9        val doc =
    5.10          builder.parse(
    5.11            new InputSourceImpl(
     6.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Jun 19 00:03:44 2011 +0200
     6.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Jun 19 14:11:06 2011 +0200
     6.3 @@ -27,20 +27,17 @@
     6.4    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
     6.5    val hidden: Byte = (3 * plain_range).toByte
     6.6  
     6.7 -  // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
     6.8 -  // FIXME \\<^bold> \\<^loc>
     6.9 -
    6.10 -  private val ctrl_styles: Map[String, Byte => Byte] =
    6.11 -    Map(
    6.12 -      "\\<^sub>" -> subscript,
    6.13 -      "\\<^sup>" -> superscript,
    6.14 -      "\\<^isub>" -> subscript,
    6.15 -      "\\<^isup>" -> superscript)
    6.16 -
    6.17    private def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
    6.18      : Map[Text.Offset, Byte => Byte] =
    6.19    {
    6.20      if (Isabelle.extended_styles) {
    6.21 +      // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
    6.22 +      // FIXME \\<^bold> \\<^loc>
    6.23 +      def ctrl_style(sym: String): Option[Byte => Byte] =
    6.24 +        if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
    6.25 +        else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))
    6.26 +        else None
    6.27 +
    6.28        var result = Map[Text.Offset, Byte => Byte]()
    6.29        def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
    6.30        {
    6.31 @@ -49,11 +46,11 @@
    6.32        var offset = 0
    6.33        var ctrl = ""
    6.34        for (sym <- Symbol.iterator(text).map(_.toString)) {
    6.35 -        if (ctrl_styles.isDefinedAt(sym)) ctrl = sym
    6.36 +        if (ctrl_style(sym).isDefined) ctrl = sym
    6.37          else if (ctrl != "") {
    6.38            if (symbols.is_controllable(sym)) {
    6.39              mark(offset - ctrl.length, offset, _ => hidden)
    6.40 -            mark(offset, offset + sym.length, ctrl_styles(ctrl))
    6.41 +            mark(offset, offset + sym.length, ctrl_style(ctrl).get)
    6.42            }
    6.43            ctrl = ""
    6.44          }