# HG changeset patch # User wenzelm # Date 1452273520 -3600 # Node ID fb73c0d7bb37e642e084f0f88fe11646fadef2f5 # Parent 3b61d05eadadce8be188cdad493a2bebfad1e43b clarified symbol insertion, depending on buffer encoding; diff -r 3b61d05eadad -r fb73c0d7bb37 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Jan 08 17:17:43 2016 +0100 +++ b/src/Pure/General/symbol.scala Fri Jan 08 18:18:40 2016 +0100 @@ -471,7 +471,7 @@ val sub_decoded = decode(sub) val sup_decoded = decode(sup) val bold_decoded = decode(bold) - val emph_decoded = decode("\\<^emph>") + val emph_decoded = decode(emph) val bsub_decoded = decode("\\<^bsub>") val esub_decoded = decode("\\<^esub>") val bsup_decoded = decode("\\<^bsup>") @@ -560,6 +560,7 @@ val sub = "\\<^sub>" val sup = "\\<^sup>" val bold = "\\<^bold>" + val emph = "\\<^emph>" def sub_decoded: Symbol = symbols.sub_decoded def sup_decoded: Symbol = symbols.sup_decoded diff -r 3b61d05eadad -r fb73c0d7bb37 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Fri Jan 08 17:17:43 2016 +0100 +++ b/src/Pure/Thy/html.scala Fri Jan 08 18:18:40 2016 +0100 @@ -11,9 +11,13 @@ { /* encode text with control symbols */ - val control_decoded = - Map(Symbol.sub_decoded -> "sub", + val control = + Map( + Symbol.sub -> "sub", + Symbol.sub_decoded -> "sub", + Symbol.sup -> "sup", Symbol.sup_decoded -> "sup", + Symbol.bold -> "b", Symbol.bold_decoded -> "b") def encode(text: String): String = @@ -32,23 +36,23 @@ } def encode_chars(s: String) = s.iterator.foreach(encode_char(_)) - var control = "" + var ctrl = "" for (sym <- Symbol.iterator(text)) { - if (control_decoded.isDefinedAt(sym)) control = sym + if (control.isDefinedAt(sym)) ctrl = sym else { - control_decoded.get(control) match { + control.get(ctrl) match { case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" => result ++= ("<" + elem + ">") encode_chars(sym) result ++= ("") case _ => - encode_chars(control) + encode_chars(ctrl) encode_chars(sym) } - control = "" + ctrl = "" } } - encode_chars(control) + encode_chars(ctrl) result.toString } diff -r 3b61d05eadad -r fb73c0d7bb37 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Fri Jan 08 17:17:43 2016 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Fri Jan 08 18:18:40 2016 +0100 @@ -303,16 +303,16 @@ /* control styles */ def control_sub(text_area: JEditTextArea) - { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) } + { Token_Markup.edit_control_style(text_area, Symbol.sub) } def control_sup(text_area: JEditTextArea) - { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) } + { Token_Markup.edit_control_style(text_area, Symbol.sup) } def control_bold(text_area: JEditTextArea) - { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) } + { Token_Markup.edit_control_style(text_area, Symbol.bold) } def control_emph(text_area: JEditTextArea) - { Token_Markup.edit_control_style(text_area, Symbol.emph_decoded) } + { Token_Markup.edit_control_style(text_area, Symbol.emph) } def control_reset(text_area: JEditTextArea) { Token_Markup.edit_control_style(text_area, "") } diff -r 3b61d05eadad -r fb73c0d7bb37 src/Tools/jEdit/src/isabelle_encoding.scala --- a/src/Tools/jEdit/src/isabelle_encoding.scala Fri Jan 08 17:17:43 2016 +0100 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala Fri Jan 08 18:18:40 2016 +0100 @@ -25,6 +25,9 @@ def is_active(buffer: JEditBuffer): Boolean = buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME + + def maybe_decode(buffer: JEditBuffer, s: String): String = + if (is_active(buffer)) Symbol.decode(s) else s } class Isabelle_Encoding extends Encoding diff -r 3b61d05eadad -r fb73c0d7bb37 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Fri Jan 08 17:17:43 2016 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Fri Jan 08 18:18:40 2016 +0100 @@ -17,9 +17,8 @@ class Symbols_Dockable(view: View, position: String) extends Dockable(view, position) { - private class Symbol_Component(val symbol: String, control: Boolean) extends Button + private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button { - private val decoded = Symbol.decode(symbol) private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round font = @@ -28,11 +27,12 @@ case Some(font_family) => GUI.font(family = font_family, size = font_size) } action = - Action(decoded) { + Action(Symbol.decode(symbol)) { val text_area = view.getTextArea - if (control && HTML.control_decoded.isDefinedAt(decoded)) - Token_Markup.edit_control_style(text_area, decoded) - else text_area.setSelectedText(decoded) + if (is_control && HTML.control.isDefinedAt(symbol)) + Token_Markup.edit_control_style(text_area, symbol) + else + text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol)) text_area.requestFocus } tooltip = diff -r 3b61d05eadad -r fb73c0d7bb37 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Fri Jan 08 17:17:43 2016 +0100 +++ b/src/Tools/jEdit/src/token_markup.scala Fri Jan 08 18:18:40 2016 +0100 @@ -27,26 +27,28 @@ { /* editing support for control symbols */ - def update_control_style(control: String, text: String): String = - { - val result = new StringBuilder - for (sym <- Symbol.iterator(text) if !HTML.control_decoded.isDefinedAt(sym)) { - if (Symbol.is_controllable(sym)) result ++= control - result ++= sym - } - result.toString - } - def edit_control_style(text_area: TextArea, control: String) { GUI_Thread.assert {} val buffer = text_area.getBuffer + val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control) + + def update_style(text: String): String = + { + val result = new StringBuilder + for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) { + if (Symbol.is_controllable(sym)) result ++= control_decoded + result ++= sym + } + result.toString + } + text_area.getSelection.foreach(sel => { val before = JEdit_Lib.point_range(buffer, sel.getStart - 1) JEdit_Lib.try_get_text(buffer, before) match { - case Some(s) if HTML.control_decoded.isDefinedAt(s) => + case Some(s) if HTML.control.isDefinedAt(s) => text_area.extendSelection(before.start, before.stop) case _ => } @@ -54,12 +56,11 @@ text_area.getSelection.toList match { case Nil => - text_area.setSelectedText(control) + text_area.setSelectedText(control_decoded) case sels => JEdit_Lib.buffer_edit(buffer) { sels.foreach(sel => - text_area.setSelectedText(sel, - update_control_style(control, text_area.getSelectedText(sel)))) + text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel)))) } } }