# HG changeset patch
# User wenzelm
# Date 1417268590 -3600
# Node ID b3c45d0e4fe1b4652f50c9640078024184d3e97f
# Parent  f26598b1a0da15f82c1eb1960d7be65b4f911f3d
encode text with control symbols;

diff -r f26598b1a0da -r b3c45d0e4fe1 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat Nov 29 14:42:32 2014 +0100
+++ b/src/Pure/Thy/html.scala	Sat Nov 29 14:43:10 2014 +0100
@@ -10,21 +10,48 @@
 
 object HTML
 {
-  /* encode text */
+  /* encode text with control symbols */
+
+  val control_decoded =
+    Map(Symbol.sub_decoded -> "sub",
+      Symbol.sup_decoded -> "sup",
+      Symbol.bold_decoded -> "b")
 
   def encode(text: String): String =
   {
-    val s = new StringBuilder
-    for (c <- text.iterator) c match {
-      case '<' => s ++= "&lt;"
-      case '>' => s ++= "&gt;"
-      case '&' => s ++= "&amp;"
-      case '"' => s ++= "&quot;"
-      case '\'' => s ++= "&#39;"
-      case '\n' => s ++= "<br/>"
-      case _ => s += c
+    val result = new StringBuilder
+
+    def encode_char(c: Char) =
+      c match {
+        case '<' => result ++= "&lt;"
+        case '>' => result ++= "&gt;"
+        case '&' => result ++= "&amp;"
+        case '"' => result ++= "&quot;"
+        case '\'' => result ++= "&#39;"
+        case '\n' => result ++= "<br/>"
+        case c => result += c
+      }
+    def encode_chars(s: String) = s.iterator.foreach(encode_char(_))
+
+    var control = ""
+    for (sym <- Symbol.iterator(text)) {
+      if (control_decoded.isDefinedAt(sym)) control = sym
+      else {
+        control_decoded.get(control) match {
+          case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
+            result ++= ("<" + elem + ">")
+            encode_chars(sym)
+            result ++= ("</" + elem + ">")
+          case _ =>
+            encode_chars(control)
+            encode_chars(sym)
+        }
+        control = ""
+      }
     }
-    s.toString
+    encode_chars(control)
+
+    result.toString
   }
 
 
diff -r f26598b1a0da -r b3c45d0e4fe1 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 29 14:42:32 2014 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 29 14:43:10 2014 +0100
@@ -30,7 +30,7 @@
     action =
       Action(decoded) {
         val text_area = view.getTextArea
-        if (Token_Markup.is_control_style(decoded))
+        if (HTML.control_decoded.isDefinedAt(decoded))
           Token_Markup.edit_control_style(text_area, decoded)
         else text_area.setSelectedText(decoded)
         text_area.requestFocus
diff -r f26598b1a0da -r b3c45d0e4fe1 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Nov 29 14:42:32 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Nov 29 14:43:10 2014 +0100
@@ -27,13 +27,10 @@
 {
   /* editing support for control symbols */
 
-  val is_control_style =
-    Set(Symbol.sub_decoded, Symbol.sup_decoded, Symbol.bold_decoded)
-
   def update_control_style(control: String, text: String): String =
   {
     val result = new StringBuilder
-    for (sym <- Symbol.iterator(text) if !is_control_style(sym)) {
+    for (sym <- Symbol.iterator(text) if !HTML.control_decoded.isDefinedAt(sym)) {
       if (Symbol.is_controllable(sym)) result ++= control
       result ++= sym
     }
@@ -49,7 +46,7 @@
     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 is_control_style(s) =>
+        case Some(s) if HTML.control_decoded.isDefinedAt(s) =>
           text_area.extendSelection(before.start, before.stop)
         case _ =>
       }