# HG changeset patch # User wenzelm # Date 1353771642 -3600 # Node ID b5a09812abc44b3016a499989da8421af24aef65 # Parent f83cab68c788b0aba69558b41b4c8963e8459a6c special handling of control symbols in Symbols dockable; less obscure Scala names; diff -r f83cab68c788 -r b5a09812abc4 src/Tools/jEdit/src/isabelle_actions.scala --- a/src/Tools/jEdit/src/isabelle_actions.scala Sat Nov 24 16:24:39 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_actions.scala Sat Nov 24 16:40:42 2012 +0100 @@ -25,28 +25,28 @@ } } + def cancel_execution() { Isabelle.session.cancel_execution() } - def cancel_execution() { Isabelle.session.cancel_execution() } /* control styles */ def control_sub(text_area: JEditTextArea) - { Token_Markup.edit_ctrl_style(text_area, Symbol.sub_decoded) } + { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) } def control_sup(text_area: JEditTextArea) - { Token_Markup.edit_ctrl_style(text_area, Symbol.sup_decoded) } + { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) } def control_isub(text_area: JEditTextArea) - { Token_Markup.edit_ctrl_style(text_area, Symbol.isub_decoded) } + { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) } def control_isup(text_area: JEditTextArea) - { Token_Markup.edit_ctrl_style(text_area, Symbol.isup_decoded) } + { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) } def control_bold(text_area: JEditTextArea) - { Token_Markup.edit_ctrl_style(text_area, Symbol.bold_decoded) } + { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) } def control_reset(text_area: JEditTextArea) - { Token_Markup.edit_ctrl_style(text_area, "") } + { Token_Markup.edit_control_style(text_area, "") } /* block styles */ diff -r f83cab68c788 -r b5a09812abc4 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Nov 24 16:24:39 2012 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Nov 24 16:40:42 2012 +0100 @@ -25,22 +25,42 @@ private class Symbol_Component(val symbol: String) extends Button { - val dec = Symbol.decode(symbol) + private val decoded = Symbol.decode(symbol) font = new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()), Font.PLAIN, Isabelle.font_size("jedit_font_scale").round) - action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus } + action = + Action(decoded) { + val text_area = view.getTextArea + if (Token_Markup.is_control_style(decoded)) + Token_Markup.edit_control_style(text_area, decoded) + else text_area.setSelectedText(decoded) + text_area.requestFocus + } tooltip = JEdit_Lib.wrap_tooltip( symbol + (if (Symbol.abbrevs.isDefinedAt(symbol)) "\nabbrev: " + Symbol.abbrevs(symbol) else "")) } + private class Reset_Component extends Button + { + action = Action("Reset") { + val text_area = view.getTextArea + Token_Markup.edit_control_style(text_area, "") + text_area.requestFocus + } + tooltip = "Reset control symbols within text" + } + val group_tabs: TabbedPane = new TabbedPane { pages ++= (for ((group, symbols) <- Symbol.groups) yield { new TabbedPane.Page(group, - new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) }) + new FlowPanel { + contents ++= symbols.map(new Symbol_Component(_)) + if (group == "control") contents += new Reset_Component + }) }).toList.sortWith(_.title <= _.title) pages += new TabbedPane.Page("search", new BorderPanel { val search = new TextField(10) diff -r f83cab68c788 -r b5a09812abc4 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Sat Nov 24 16:24:39 2012 +0100 +++ b/src/Tools/jEdit/src/token_markup.scala Sat Nov 24 16:40:42 2012 +0100 @@ -27,45 +27,45 @@ { /* editing support for control symbols */ - private val is_ctrl_style = + val is_control_style = Set(Symbol.sub_decoded, Symbol.sup_decoded, Symbol.isub_decoded, Symbol.isup_decoded, Symbol.bold_decoded) - def update_ctrl_style(ctrl: String, text: String): String = + def update_control_style(control: String, text: String): String = { val result = new StringBuilder - for (sym <- Symbol.iterator(text) if !is_ctrl_style(sym)) { - if (Symbol.is_controllable(sym)) result ++= ctrl + for (sym <- Symbol.iterator(text) if !is_control_style(sym)) { + if (Symbol.is_controllable(sym)) result ++= control result ++= sym } result.toString } - def edit_ctrl_style(text_area: TextArea, ctrl: String) + def edit_control_style(text_area: TextArea, control: String) { Swing_Thread.assert() val buffer = text_area.getBuffer text_area.getSelection.toList match { - case Nil if ctrl == "" => + case Nil if control == "" => try { buffer.beginCompoundEdit() val caret = text_area.getCaretPosition - if (caret > 0 && is_ctrl_style(buffer.getText(caret - 1, 1))) + if (caret > 0 && is_control_style(buffer.getText(caret - 1, 1))) text_area.backspace() } finally { buffer.endCompoundEdit() } - case Nil if ctrl != "" => - text_area.setSelectedText(ctrl) + case Nil if control != "" => + text_area.setSelectedText(control) case sels => try { buffer.beginCompoundEdit() sels.foreach(sel => text_area.setSelectedText(sel, - update_ctrl_style(ctrl, text_area.getSelectedText(sel)))) + update_control_style(control, text_area.getSelectedText(sel)))) } finally { buffer.endCompoundEdit() @@ -165,7 +165,7 @@ def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] = { // FIXME Symbol.bsub_decoded etc. - def ctrl_style(sym: String): Option[Byte => Byte] = + def control_style(sym: String): Option[Byte => Byte] = if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_)) else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_)) else if (sym == Symbol.bold_decoded) Some(bold(_)) @@ -177,15 +177,15 @@ for (i <- start until stop) result += (i -> style) } var offset = 0 - var ctrl = "" + var control = "" for (sym <- Symbol.iterator(text)) { - if (ctrl_style(sym).isDefined) ctrl = sym - else if (ctrl != "") { + if (control_style(sym).isDefined) control = sym + else if (control != "") { if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) { - mark(offset - ctrl.length, offset, _ => hidden) - mark(offset, offset + sym.length, ctrl_style(ctrl).get) + mark(offset - control.length, offset, _ => hidden) + mark(offset, offset + sym.length, control_style(control).get) } - ctrl = "" + control = "" } Symbol.lookup_font(sym) match { case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))