# HG changeset patch
# User wenzelm
# Date 1335970585 -7200
# Node ID c638127b46537faf1e5f7a32c16fb1218538223d
# Parent  48b52cdc214ae7abb1efa0cdbbb34481a26ffbd6
avoid interference of markup for literal tokens, which may contain slightly odd \<^bsub> \<^esub> counted as pseudo-markup (especially relevant for HTML output, e.g. of thm power3_eq_cube);

diff -r 48b52cdc214a -r c638127b4653 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed May 02 16:04:07 2012 +0200
+++ b/src/Pure/General/symbol.ML	Wed May 02 16:56:25 2012 +0200
@@ -48,6 +48,7 @@
   val is_digit: symbol -> bool
   val is_quasi: symbol -> bool
   val is_blank: symbol -> bool
+  val is_block_ctrl: symbol -> bool
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
   val is_ident: symbol list -> bool
@@ -390,6 +391,8 @@
 fun is_quasi s = kind s = Quasi;
 fun is_blank s = kind s = Blank;
 
+val is_block_ctrl = member (op =) ["\\<^bsub>", "\\<^esub>", "\\<^bsup>", "\\<^esup>"];
+
 fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
 
diff -r 48b52cdc214a -r c638127b4653 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed May 02 16:04:07 2012 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed May 02 16:56:25 2012 +0200
@@ -191,8 +191,13 @@
                 tabs trf token_trans markup_extern t @ Ts, args')
           end
       | synT m (String s :: symbs, args) =
-          let val (Ts, args') = synT m (symbs, args);
-          in (Pretty.marks_str (m, s) :: Ts, args') end
+          let
+            val (Ts, args') = synT m (symbs, args);
+            val T =
+              if exists Symbol.is_block_ctrl (Symbol.explode s)
+              then Pretty.str s
+              else Pretty.marks_str (m, s);
+          in (T :: Ts, args') end
       | synT m (Space s :: symbs, args) =
           let val (Ts, args') = synT m (symbs, args);
           in (Pretty.str s :: Ts, args') end