src/Pure/Thy/latex.ML
changeset 11012 8eb472444705
parent 10955 36741b4fe109
child 11719 49c14348a42b
--- a/src/Pure/Thy/latex.ML	Wed Jan 31 22:15:53 2001 +0100
+++ b/src/Pure/Thy/latex.ML	Wed Jan 31 22:16:22 2001 +0100
@@ -92,10 +92,6 @@
 
 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
 
-fun strip_blanks s =
-  implode (#1 (Library.take_suffix Symbol.is_blank
-    (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
-
 fun output_tok (Basic tok, _) =
       let val s = T.val_of tok in
         if invisible_token tok then ""
@@ -107,10 +103,11 @@
         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
         else output_syms s
       end
-  | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "%\n}\n"
+  | output_tok (Markup cmd, txt) =
+      "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n"
   | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
-      strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
-  | output_tok (Verbatim, txt) = "%\n" ^ strip_blanks txt ^ "\n";
+      Symbol.strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
+  | output_tok (Verbatim, txt) = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
 
 
 val output_tokens = implode o map output_tok;