# HG changeset patch
# User wenzelm
# Date 939151093 -7200
# Node ID 131005d3a62ddf9d1df7bd1fac23c4e334f2c939
# Parent  f27d54c1ef399b092f6da80e7eda6a3b4514bfa6
strip_blanks;

diff -r f27d54c1ef39 -r 131005d3a62d src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Oct 05 21:17:44 1999 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Oct 05 21:18:13 1999 +0200
@@ -53,6 +53,10 @@
 
 structure T = OuterLex;
 
+fun strip_blanks s =
+  implode (#1 (Library.take_suffix Symbol.is_blank
+    (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
+
 fun output_tok tok =
   let
     val out = output_symbol;
@@ -61,7 +65,7 @@
     if T.is_kind T.Command tok then "\\isacommand{" ^ out s ^ "}"
     else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ out s ^ "}"
     else if T.is_kind T.String tok then out (quote s)
-    else if T.is_kind T.Verbatim tok then "\\isatext{" ^ s ^ "}"
+    else if T.is_kind T.Verbatim tok then "\\isatext{" ^ strip_blanks s ^ "}"
     else out s
   end;