special handling of control symbols in Symbols dockable;
authorwenzelm
Sat Nov 24 16:40:42 2012 +0100 (2012-11-24)
changeset 50187b5a09812abc4
parent 50186 f83cab68c788
child 50188 6d22f5a7335c
special handling of control symbols in Symbols dockable;
less obscure Scala names;
src/Tools/jEdit/src/isabelle_actions.scala
src/Tools/jEdit/src/symbols_dockable.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/isabelle_actions.scala	Sat Nov 24 16:24:39 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle_actions.scala	Sat Nov 24 16:40:42 2012 +0100
     1.3 @@ -25,28 +25,28 @@
     1.4      }
     1.5    }
     1.6  
     1.7 +  def cancel_execution() { Isabelle.session.cancel_execution() }
     1.8  
     1.9 -  def cancel_execution() { Isabelle.session.cancel_execution() }
    1.10  
    1.11    /* control styles */
    1.12  
    1.13    def control_sub(text_area: JEditTextArea)
    1.14 -  { Token_Markup.edit_ctrl_style(text_area, Symbol.sub_decoded) }
    1.15 +  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
    1.16  
    1.17    def control_sup(text_area: JEditTextArea)
    1.18 -  { Token_Markup.edit_ctrl_style(text_area, Symbol.sup_decoded) }
    1.19 +  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    1.20  
    1.21    def control_isub(text_area: JEditTextArea)
    1.22 -  { Token_Markup.edit_ctrl_style(text_area, Symbol.isub_decoded) }
    1.23 +  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
    1.24  
    1.25    def control_isup(text_area: JEditTextArea)
    1.26 -  { Token_Markup.edit_ctrl_style(text_area, Symbol.isup_decoded) }
    1.27 +  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
    1.28  
    1.29    def control_bold(text_area: JEditTextArea)
    1.30 -  { Token_Markup.edit_ctrl_style(text_area, Symbol.bold_decoded) }
    1.31 +  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
    1.32  
    1.33    def control_reset(text_area: JEditTextArea)
    1.34 -  { Token_Markup.edit_ctrl_style(text_area, "") }
    1.35 +  { Token_Markup.edit_control_style(text_area, "") }
    1.36  
    1.37  
    1.38    /* block styles */
     2.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 16:24:39 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 16:40:42 2012 +0100
     2.3 @@ -25,22 +25,42 @@
     2.4  
     2.5    private class Symbol_Component(val symbol: String) extends Button
     2.6    {
     2.7 -    val dec = Symbol.decode(symbol)
     2.8 +    private val decoded = Symbol.decode(symbol)
     2.9      font =
    2.10        new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()),
    2.11          Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
    2.12 -    action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
    2.13 +    action =
    2.14 +      Action(decoded) {
    2.15 +        val text_area = view.getTextArea
    2.16 +        if (Token_Markup.is_control_style(decoded))
    2.17 +          Token_Markup.edit_control_style(text_area, decoded)
    2.18 +        else text_area.setSelectedText(decoded)
    2.19 +        text_area.requestFocus
    2.20 +      }
    2.21      tooltip =
    2.22        JEdit_Lib.wrap_tooltip(
    2.23          symbol +
    2.24            (if (Symbol.abbrevs.isDefinedAt(symbol)) "\nabbrev: " + Symbol.abbrevs(symbol) else ""))
    2.25    }
    2.26  
    2.27 +  private class Reset_Component extends Button
    2.28 +  {
    2.29 +    action = Action("Reset") {
    2.30 +      val text_area = view.getTextArea
    2.31 +      Token_Markup.edit_control_style(text_area, "")
    2.32 +      text_area.requestFocus
    2.33 +    }
    2.34 +    tooltip = "Reset control symbols within text"
    2.35 +  }
    2.36 +
    2.37    val group_tabs: TabbedPane = new TabbedPane {
    2.38      pages ++= (for ((group, symbols) <- Symbol.groups) yield
    2.39        {
    2.40          new TabbedPane.Page(group,
    2.41 -          new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) })
    2.42 +          new FlowPanel {
    2.43 +            contents ++= symbols.map(new Symbol_Component(_))
    2.44 +            if (group == "control") contents += new Reset_Component
    2.45 +          })
    2.46        }).toList.sortWith(_.title <= _.title)
    2.47      pages += new TabbedPane.Page("search", new BorderPanel {
    2.48        val search = new TextField(10)
     3.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 16:24:39 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 16:40:42 2012 +0100
     3.3 @@ -27,45 +27,45 @@
     3.4  {
     3.5    /* editing support for control symbols */
     3.6  
     3.7 -  private val is_ctrl_style =
     3.8 +  val is_control_style =
     3.9      Set(Symbol.sub_decoded, Symbol.sup_decoded,
    3.10        Symbol.isub_decoded, Symbol.isup_decoded, Symbol.bold_decoded)
    3.11  
    3.12 -  def update_ctrl_style(ctrl: String, text: String): String =
    3.13 +  def update_control_style(control: String, text: String): String =
    3.14    {
    3.15      val result = new StringBuilder
    3.16 -    for (sym <- Symbol.iterator(text) if !is_ctrl_style(sym)) {
    3.17 -      if (Symbol.is_controllable(sym)) result ++= ctrl
    3.18 +    for (sym <- Symbol.iterator(text) if !is_control_style(sym)) {
    3.19 +      if (Symbol.is_controllable(sym)) result ++= control
    3.20        result ++= sym
    3.21      }
    3.22      result.toString
    3.23    }
    3.24  
    3.25 -  def edit_ctrl_style(text_area: TextArea, ctrl: String)
    3.26 +  def edit_control_style(text_area: TextArea, control: String)
    3.27    {
    3.28      Swing_Thread.assert()
    3.29  
    3.30      val buffer = text_area.getBuffer
    3.31  
    3.32      text_area.getSelection.toList match {
    3.33 -      case Nil if ctrl == "" =>
    3.34 +      case Nil if control == "" =>
    3.35          try {
    3.36            buffer.beginCompoundEdit()
    3.37            val caret = text_area.getCaretPosition
    3.38 -          if (caret > 0 && is_ctrl_style(buffer.getText(caret - 1, 1)))
    3.39 +          if (caret > 0 && is_control_style(buffer.getText(caret - 1, 1)))
    3.40              text_area.backspace()
    3.41          }
    3.42          finally {
    3.43            buffer.endCompoundEdit()
    3.44          }
    3.45 -      case Nil if ctrl != "" =>
    3.46 -        text_area.setSelectedText(ctrl)
    3.47 +      case Nil if control != "" =>
    3.48 +        text_area.setSelectedText(control)
    3.49        case sels =>
    3.50          try {
    3.51            buffer.beginCompoundEdit()
    3.52            sels.foreach(sel =>
    3.53              text_area.setSelectedText(sel,
    3.54 -              update_ctrl_style(ctrl, text_area.getSelectedText(sel))))
    3.55 +              update_control_style(control, text_area.getSelectedText(sel))))
    3.56          }
    3.57          finally {
    3.58            buffer.endCompoundEdit()
    3.59 @@ -165,7 +165,7 @@
    3.60    def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
    3.61    {
    3.62      // FIXME Symbol.bsub_decoded etc.
    3.63 -    def ctrl_style(sym: String): Option[Byte => Byte] =
    3.64 +    def control_style(sym: String): Option[Byte => Byte] =
    3.65        if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_))
    3.66        else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_))
    3.67        else if (sym == Symbol.bold_decoded) Some(bold(_))
    3.68 @@ -177,15 +177,15 @@
    3.69        for (i <- start until stop) result += (i -> style)
    3.70      }
    3.71      var offset = 0
    3.72 -    var ctrl = ""
    3.73 +    var control = ""
    3.74      for (sym <- Symbol.iterator(text)) {
    3.75 -      if (ctrl_style(sym).isDefined) ctrl = sym
    3.76 -      else if (ctrl != "") {
    3.77 +      if (control_style(sym).isDefined) control = sym
    3.78 +      else if (control != "") {
    3.79          if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
    3.80 -          mark(offset - ctrl.length, offset, _ => hidden)
    3.81 -          mark(offset, offset + sym.length, ctrl_style(ctrl).get)
    3.82 +          mark(offset - control.length, offset, _ => hidden)
    3.83 +          mark(offset, offset + sym.length, control_style(control).get)
    3.84          }
    3.85 -        ctrl = ""
    3.86 +        control = ""
    3.87        }
    3.88        Symbol.lookup_font(sym) match {
    3.89          case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))