output control symbols like ML version, with optionally hidden source;

--- a/src/Pure/General/symbol.scala	Thu Jun 01 21:14:38 2017 +0200
+++ b/src/Pure/General/symbol.scala	Thu Jun 01 21:15:56 2017 +0200
@@ -487,10 +487,10 @@
     val sup_decoded = decode(sup)
     val bold_decoded = decode(bold)
     val emph_decoded = decode(emph)
-    val bsub_decoded = decode("\\<^bsub>")
-    val esub_decoded = decode("\\<^esub>")
-    val bsup_decoded = decode("\\<^bsup>")
-    val esup_decoded = decode("\\<^esup>")
+    val bsub_decoded = decode(bsub)
+    val esub_decoded = decode(esub)
+    val bsup_decoded = decode(bsup)
+    val esup_decoded = decode(esup)
   }
 
 
@@ -585,6 +585,10 @@
   val sup = "\\<^sup>"
   val bold = "\\<^bold>"
   val emph = "\\<^emph>"
+  val bsub = "\\<^bsub>"
+  val esub = "\\<^esub>"
+  val bsup = "\\<^bsup>"
+  val esup = "\\<^esup>"
 
   def sub_decoded: Symbol = symbols.sub_decoded
   def sup_decoded: Symbol = symbols.sup_decoded

--- a/src/Pure/Thy/html.scala	Thu Jun 01 21:14:38 2017 +0200
+++ b/src/Pure/Thy/html.scala	Thu Jun 01 21:15:56 2017 +0200
@@ -9,41 +9,61 @@
 
 object HTML
 {
-  /* encode text with control symbols */
+  /* output text with control symbols */
 
-  val control =
+  private val control =
+    Map(
+      Symbol.sub -> "sub", Symbol.sub_decoded -> "sub",
+      Symbol.sup -> "sup", Symbol.sup_decoded -> "sup",
+      Symbol.bold -> "b", Symbol.bold_decoded -> "b")
+
+  private val control_block =
     Map(
-      Symbol.sub -> "sub",
-      Symbol.sub_decoded -> "sub",
-      Symbol.sup -> "sup",
-      Symbol.sup_decoded -> "sup",
-      Symbol.bold -> "b",
-      Symbol.bold_decoded -> "b")
+      Symbol.bsub -> "<sub>", Symbol.bsub_decoded -> "<sub>",
+      Symbol.esub -> "</sub>", Symbol.esub_decoded -> "</sub>",
+      Symbol.bsup -> "<sup>", Symbol.bsup_decoded -> "<sup>",
+      Symbol.esup -> "</sup>", Symbol.esup_decoded -> "</sup>")
+
+  def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
+
+  def output(text: String, s: StringBuilder, hidden: Boolean)
+  {
+    def output_hidden(body: => Unit): Unit =
+      if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
 
-  def output(text: String, s: StringBuilder)
-  {
-    def output_string(str: String) = XML.output_string(str, s)
+    def output_symbol(sym: Symbol.Symbol): Unit =
+      if (sym != "") {
+        control_block.get(sym) match {
+          case Some(html) if html.startsWith("</") =>
+            s ++= html; output_hidden(XML.output_string(sym, s))
+          case Some(html) =>
+            output_hidden(XML.output_string(sym, s)); s ++= html
+          case None =>
+            XML.output_string(sym, s)
+        }
+      }
 
     var ctrl = ""
     for (sym <- Symbol.iterator(text)) {
-      if (control.isDefinedAt(sym)) ctrl = sym
+      if (is_control(sym)) { output_symbol(ctrl); ctrl = sym }
       else {
         control.get(ctrl) match {
           case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
+            output_hidden(output_symbol(ctrl))
             s += '<'; s ++= elem; s += '>'
-            output_string(sym)
+            output_symbol(sym)
             s ++= "</"; s ++= elem; s += '>'
           case _ =>
-            output_string(ctrl)
-            output_string(sym)
+            output_symbol(ctrl)
+            output_symbol(sym)
         }
         ctrl = ""
       }
     }
-    output_string(ctrl)
+    output_symbol(ctrl)
   }
 
-  def output(text: String): String = Library.make_string(output(text, _))
+  def output(text: String): String = Library.make_string(output(text, _, hidden = false))
 
 
   /* output XML as HTML */
@@ -52,13 +72,13 @@
     Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
       "ul", "ol", "dl", "li", "dt", "dd")
 
-  def output(body: XML.Body, s: StringBuilder)
+  def output(body: XML.Body, s: StringBuilder, hidden: Boolean)
   {
     def elem(markup: Markup)
     {
       s ++= markup.name
       for ((a, b) <- markup.properties) {
-        s += ' '; s ++= a; s += '='; s += '"'; output(b, s); s += '"'
+        s += ' '; s ++= a; s += '='; s += '"'; output(b, s, hidden); s += '"'
       }
     }
     def tree(t: XML.Tree): Unit =
@@ -71,13 +91,17 @@
           ts.foreach(tree)
           s ++= "</"; s ++= markup.name; s += '>'
           if (structural_elements(markup.name)) s += '\n'
-        case XML.Text(txt) => output(txt, s)
+        case XML.Text(txt) =>
+          output(txt, s, hidden)
       }
     body.foreach(tree)
   }
 
-  def output(body: XML.Body): String = Library.make_string(output(body, _))
-  def output(tree: XML.Tree): String = output(List(tree))
+  def output(body: XML.Body, hidden: Boolean): String =
+    Library.make_string(output(body, _, hidden))
+
+  def output(tree: XML.Tree, hidden: Boolean): String =
+    output(List(tree), hidden)
 
 
   /* attributes */
@@ -187,11 +211,16 @@
   def head_css(css: String): XML.Elem =
     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil)
 
-  def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String =
+  def output_document(head: XML.Body, body: XML.Body,
+    css: String = "isabelle.css", hidden: Boolean = true): String =
+  {
     cat_lines(
       List(header,
-        output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)),
-        output(XML.elem("body", body))))
+        output(
+          XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head),
+          hidden = hidden),
+        output(XML.elem("body", body), hidden = hidden)))
+  }
 
 
   /* document directory */
@@ -203,9 +232,9 @@
   }
 
   def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
-    css: String = "isabelle.css")
+    css: String = "isabelle.css", hidden: Boolean = true)
   {
     init_dir(dir)
-    File.write(dir + Path.basic(name), output_document(head, body, css))
+    File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden))
   }
 }

--- a/src/Tools/jEdit/src/symbols_dockable.scala	Thu Jun 01 21:14:38 2017 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Thu Jun 01 21:15:56 2017 +0200
@@ -96,7 +96,7 @@
     action =
       Action(Symbol.decode(symbol)) {
         val text_area = view.getTextArea
-        if (is_control && HTML.control.isDefinedAt(symbol))
+        if (is_control && HTML.is_control(symbol))
           Syntax_Style.edit_control_style(text_area, symbol)
         else
           text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))

--- a/src/Tools/jEdit/src/syntax_style.scala	Thu Jun 01 21:14:38 2017 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala	Thu Jun 01 21:15:56 2017 +0200
@@ -138,7 +138,7 @@
     def update_style(text: String): String =
     {
       val result = new StringBuilder
-      for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) {
+      for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) {
         if (Symbol.is_controllable(sym)) result ++= control_decoded
         result ++= sym
       }
@@ -148,7 +148,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 HTML.control.isDefinedAt(s) =>
+        case Some(s) if HTML.is_control(s) =>
           text_area.extendSelection(before.start, before.stop)
         case _ =>
       }