clarified symbol insertion, depending on buffer encoding;
authorwenzelm
Fri Jan 08 18:18:40 2016 +0100 (2016-01-08)
changeset 62104fb73c0d7bb37
parent 62103 3b61d05eadad
child 62105 686681f69d5e
clarified symbol insertion, depending on buffer encoding;
src/Pure/General/symbol.scala
src/Pure/Thy/html.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_encoding.scala
src/Tools/jEdit/src/symbols_dockable.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/General/symbol.scala	Fri Jan 08 17:17:43 2016 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Fri Jan 08 18:18:40 2016 +0100
     1.3 @@ -471,7 +471,7 @@
     1.4      val sub_decoded = decode(sub)
     1.5      val sup_decoded = decode(sup)
     1.6      val bold_decoded = decode(bold)
     1.7 -    val emph_decoded = decode("\\<^emph>")
     1.8 +    val emph_decoded = decode(emph)
     1.9      val bsub_decoded = decode("\\<^bsub>")
    1.10      val esub_decoded = decode("\\<^esub>")
    1.11      val bsup_decoded = decode("\\<^bsup>")
    1.12 @@ -560,6 +560,7 @@
    1.13    val sub = "\\<^sub>"
    1.14    val sup = "\\<^sup>"
    1.15    val bold = "\\<^bold>"
    1.16 +  val emph = "\\<^emph>"
    1.17  
    1.18    def sub_decoded: Symbol = symbols.sub_decoded
    1.19    def sup_decoded: Symbol = symbols.sup_decoded
     2.1 --- a/src/Pure/Thy/html.scala	Fri Jan 08 17:17:43 2016 +0100
     2.2 +++ b/src/Pure/Thy/html.scala	Fri Jan 08 18:18:40 2016 +0100
     2.3 @@ -11,9 +11,13 @@
     2.4  {
     2.5    /* encode text with control symbols */
     2.6  
     2.7 -  val control_decoded =
     2.8 -    Map(Symbol.sub_decoded -> "sub",
     2.9 +  val control =
    2.10 +    Map(
    2.11 +      Symbol.sub -> "sub",
    2.12 +      Symbol.sub_decoded -> "sub",
    2.13 +      Symbol.sup -> "sup",
    2.14        Symbol.sup_decoded -> "sup",
    2.15 +      Symbol.bold -> "b",
    2.16        Symbol.bold_decoded -> "b")
    2.17  
    2.18    def encode(text: String): String =
    2.19 @@ -32,23 +36,23 @@
    2.20        }
    2.21      def encode_chars(s: String) = s.iterator.foreach(encode_char(_))
    2.22  
    2.23 -    var control = ""
    2.24 +    var ctrl = ""
    2.25      for (sym <- Symbol.iterator(text)) {
    2.26 -      if (control_decoded.isDefinedAt(sym)) control = sym
    2.27 +      if (control.isDefinedAt(sym)) ctrl = sym
    2.28        else {
    2.29 -        control_decoded.get(control) match {
    2.30 +        control.get(ctrl) match {
    2.31            case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
    2.32              result ++= ("<" + elem + ">")
    2.33              encode_chars(sym)
    2.34              result ++= ("</" + elem + ">")
    2.35            case _ =>
    2.36 -            encode_chars(control)
    2.37 +            encode_chars(ctrl)
    2.38              encode_chars(sym)
    2.39          }
    2.40 -        control = ""
    2.41 +        ctrl = ""
    2.42        }
    2.43      }
    2.44 -    encode_chars(control)
    2.45 +    encode_chars(ctrl)
    2.46  
    2.47      result.toString
    2.48    }
     3.1 --- a/src/Tools/jEdit/src/isabelle.scala	Fri Jan 08 17:17:43 2016 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Fri Jan 08 18:18:40 2016 +0100
     3.3 @@ -303,16 +303,16 @@
     3.4    /* control styles */
     3.5  
     3.6    def control_sub(text_area: JEditTextArea)
     3.7 -  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
     3.8 +  { Token_Markup.edit_control_style(text_area, Symbol.sub) }
     3.9  
    3.10    def control_sup(text_area: JEditTextArea)
    3.11 -  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    3.12 +  { Token_Markup.edit_control_style(text_area, Symbol.sup) }
    3.13  
    3.14    def control_bold(text_area: JEditTextArea)
    3.15 -  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
    3.16 +  { Token_Markup.edit_control_style(text_area, Symbol.bold) }
    3.17  
    3.18    def control_emph(text_area: JEditTextArea)
    3.19 -  { Token_Markup.edit_control_style(text_area, Symbol.emph_decoded) }
    3.20 +  { Token_Markup.edit_control_style(text_area, Symbol.emph) }
    3.21  
    3.22    def control_reset(text_area: JEditTextArea)
    3.23    { Token_Markup.edit_control_style(text_area, "") }
     4.1 --- a/src/Tools/jEdit/src/isabelle_encoding.scala	Fri Jan 08 17:17:43 2016 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Fri Jan 08 18:18:40 2016 +0100
     4.3 @@ -25,6 +25,9 @@
     4.4  
     4.5    def is_active(buffer: JEditBuffer): Boolean =
     4.6      buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
     4.7 +
     4.8 +  def maybe_decode(buffer: JEditBuffer, s: String): String =
     4.9 +    if (is_active(buffer)) Symbol.decode(s) else s
    4.10  }
    4.11  
    4.12  class Isabelle_Encoding extends Encoding
     5.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Fri Jan 08 17:17:43 2016 +0100
     5.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Fri Jan 08 18:18:40 2016 +0100
     5.3 @@ -17,9 +17,8 @@
     5.4  
     5.5  class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
     5.6  {
     5.7 -  private class Symbol_Component(val symbol: String, control: Boolean) extends Button
     5.8 +  private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button
     5.9    {
    5.10 -    private val decoded = Symbol.decode(symbol)
    5.11      private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
    5.12  
    5.13      font =
    5.14 @@ -28,11 +27,12 @@
    5.15          case Some(font_family) => GUI.font(family = font_family, size = font_size)
    5.16        }
    5.17      action =
    5.18 -      Action(decoded) {
    5.19 +      Action(Symbol.decode(symbol)) {
    5.20          val text_area = view.getTextArea
    5.21 -        if (control && HTML.control_decoded.isDefinedAt(decoded))
    5.22 -          Token_Markup.edit_control_style(text_area, decoded)
    5.23 -        else text_area.setSelectedText(decoded)
    5.24 +        if (is_control && HTML.control.isDefinedAt(symbol))
    5.25 +          Token_Markup.edit_control_style(text_area, symbol)
    5.26 +        else
    5.27 +          text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
    5.28          text_area.requestFocus
    5.29        }
    5.30      tooltip =
     6.1 --- a/src/Tools/jEdit/src/token_markup.scala	Fri Jan 08 17:17:43 2016 +0100
     6.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Fri Jan 08 18:18:40 2016 +0100
     6.3 @@ -27,26 +27,28 @@
     6.4  {
     6.5    /* editing support for control symbols */
     6.6  
     6.7 -  def update_control_style(control: String, text: String): String =
     6.8 -  {
     6.9 -    val result = new StringBuilder
    6.10 -    for (sym <- Symbol.iterator(text) if !HTML.control_decoded.isDefinedAt(sym)) {
    6.11 -      if (Symbol.is_controllable(sym)) result ++= control
    6.12 -      result ++= sym
    6.13 -    }
    6.14 -    result.toString
    6.15 -  }
    6.16 -
    6.17    def edit_control_style(text_area: TextArea, control: String)
    6.18    {
    6.19      GUI_Thread.assert {}
    6.20  
    6.21      val buffer = text_area.getBuffer
    6.22  
    6.23 +    val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
    6.24 +
    6.25 +    def update_style(text: String): String =
    6.26 +    {
    6.27 +      val result = new StringBuilder
    6.28 +      for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) {
    6.29 +        if (Symbol.is_controllable(sym)) result ++= control_decoded
    6.30 +        result ++= sym
    6.31 +      }
    6.32 +      result.toString
    6.33 +    }
    6.34 +
    6.35      text_area.getSelection.foreach(sel => {
    6.36        val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
    6.37        JEdit_Lib.try_get_text(buffer, before) match {
    6.38 -        case Some(s) if HTML.control_decoded.isDefinedAt(s) =>
    6.39 +        case Some(s) if HTML.control.isDefinedAt(s) =>
    6.40            text_area.extendSelection(before.start, before.stop)
    6.41          case _ =>
    6.42        }
    6.43 @@ -54,12 +56,11 @@
    6.44  
    6.45      text_area.getSelection.toList match {
    6.46        case Nil =>
    6.47 -        text_area.setSelectedText(control)
    6.48 +        text_area.setSelectedText(control_decoded)
    6.49        case sels =>
    6.50          JEdit_Lib.buffer_edit(buffer) {
    6.51            sels.foreach(sel =>
    6.52 -            text_area.setSelectedText(sel,
    6.53 -              update_control_style(control, text_area.getSelectedText(sel))))
    6.54 +            text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel))))
    6.55          }
    6.56      }
    6.57    }