--- 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
--- 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 ++= ("</" + elem + ">")
case _ =>
- encode_chars(control)
+ encode_chars(ctrl)
encode_chars(sym)
}
- control = ""
+ ctrl = ""
}
}
- encode_chars(control)
+ encode_chars(ctrl)
result.toString
}
--- 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, "") }
--- 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
--- 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 =
--- 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))))
}
}
}