added markup for hidden text;
handle "\<^bold>" as markup;
HTML output: include original control symbols as hidden text, to enable copy-paste;

--- a/lib/html/isabelle.css	Fri Dec 04 22:51:59 2009 +0100
+++ b/lib/html/isabelle.css	Sat Dec 05 16:39:49 2009 +0100
@@ -18,8 +18,11 @@
 hr { height: 0px; border: 0px; }
 
 
-/* inner and outer syntax markup */
+/* basic syntax markup */
 
+.hidden, hidden { font-size: 0.1pt; visibility: hidden; }
+
+.tclass, tclass               { color: red; }
 .tfree, tfree                 { color: purple; }
 .tvar, tvar                   { color: purple; }
 .free, free                   { color: blue; }
@@ -31,8 +34,8 @@
 .inner_string, inner_string   { color: brown; }
 .inner_comment, inner_comment { color: #8B0000; }
 
-.loc, loc              { color: brown; }
-.tclass, tclass        { color: red; }
+.bold, bold  { font-weight: bold; }
+.loc, loc  { color: brown; }
 
 .keyword, keyword      { font-weight: bold; }
 .command, command      { font-weight: bold; }
@@ -45,3 +48,4 @@
 .malformed, malformed  { background-color: #FF6A6A; }
 
 .malformed_span, malformed_span { background-color: #FF6A6A; }
+

--- a/src/Pure/General/markup.ML	Fri Dec 04 22:51:59 2009 +0100
+++ b/src/Pure/General/markup.ML	Sat Dec 05 16:39:49 2009 +0100
@@ -34,6 +34,7 @@
   val widthN: string
   val breakN: string val break: int -> T
   val fbreakN: string val fbreak: T
+  val hiddenN: string val hidden: T
   val tclassN: string val tclass: string -> T
   val tyconN: string val tycon: string -> T
   val fixed_declN: string val fixed_decl: string -> T
@@ -191,6 +192,11 @@
 val (fbreakN, fbreak) = markup_elem "fbreak";
 
 
+(* hidden text *)
+
+val (hiddenN, hidden) = markup_elem "hidden";
+
+
 (* logical entities *)
 
 val (tclassN, tclass) = markup_string "tclass" nameN;

--- a/src/Pure/General/markup.scala	Fri Dec 04 22:51:59 2009 +0100
+++ b/src/Pure/General/markup.scala	Sat Dec 05 16:39:49 2009 +0100
@@ -40,6 +40,11 @@
   val LOCATION = "location"
 
 
+  /* hidden text */
+
+  val HIDDEN = "hidden"
+
+
   /* logical entities */
 
   val TCLASS = "tclass"

--- a/src/Pure/Thy/html.ML	Fri Dec 04 22:51:59 2009 +0100
+++ b/src/Pure/Thy/html.ML	Sat Dec 05 16:39:49 2009 +0100
@@ -45,9 +45,18 @@
 fun html_mode f x = PrintMode.with_modes [htmlN] f x;
 
 
+(* common markup *)
+
+fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
+
+val _ = Markup.add_mode htmlN (fn (name, _) => span name);
+
+
 (* symbol output *)
 
 local
+  val hidden = XML.text #> (span Markup.hiddenN |-> enclose);
+
   val html_syms = Symtab.make
    [("'", (1, "&#39;")),
     ("\\<spacespace>", (2, "&nbsp;&nbsp;")),
@@ -190,10 +199,10 @@
     ("\\<longleftrightarrow>", (3, "&lt;-&gt;")),
     ("\\<longrightarrow>", (3, "--&gt;")),
     ("\\<rightarrow>", (2, "-&gt;")),
-    ("\\<^bsub>", (0, "<sub>")),
-    ("\\<^esub>", (0, "</sub>")),
-    ("\\<^bsup>", (0, "<sup>")),
-    ("\\<^esup>", (0, "</sup>"))];
+    ("\\<^bsub>", (0, hidden "\\<^bsub>" ^ "<sub>")),
+    ("\\<^esub>", (0, hidden "\\<^esub>" ^ "</sub>")),
+    ("\\<^bsup>", (0, hidden "\\<^bsup>" ^ "<sup>")),
+    ("\\<^esup>", (0, hidden "\\<^esup>" ^ "</sup>"))];
 
   fun output_sym s =
     if Symbol.is_raw s then (1, Symbol.decode_raw s)
@@ -202,15 +211,21 @@
         SOME x => x
       | NONE => (size s, XML.text s));
 
-  fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
-  fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
-  fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s);
+  fun output_markup (bg, en) s1 s2 =
+    let val (n, txt) = output_sym s2
+    in (n, hidden s1 ^ enclose bg en txt) end;
 
-  fun output_syms ("\\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
-    | output_syms ("\\<^isub>" :: s :: ss) = output_sub s :: output_syms ss
-    | output_syms ("\\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
-    | output_syms ("\\<^isup>" :: s :: ss) = output_sup s :: output_syms ss
-    | output_syms ("\\<^loc>" :: s :: ss) = output_loc s :: output_syms ss
+  val output_sub = output_markup ("<sub>", "</sub>");
+  val output_sup = output_markup ("<sup>", "</sup>");
+  val output_bold = output_markup (span "bold");
+  val output_loc = output_markup (span "loc");
+
+  fun output_syms (s1 :: s2 :: ss) =
+        if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then output_sub s1 s2 :: output_syms ss
+        else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then output_sup s1 s2 :: output_syms ss
+        else if s1 = "\\<^bold>" then output_bold s1 s2 :: output_syms ss
+        else if s1 = "\\<^loc>" then output_loc s1 s2 :: output_syms ss
+        else output_sym s1 :: output_syms (s2 :: ss)
     | output_syms (s :: ss) = output_sym s :: output_syms ss
     | output_syms [] = [];
 in
@@ -230,13 +245,6 @@
 end;
 
 
-(* common markup *)
-
-fun span s = ("<span class=" ^ quote (XML.text s) ^ ">", "</span>");
-
-val _ = Markup.add_mode htmlN (fn (name, _) => span name);
-
-
 
 (** HTML markup **)