# HG changeset patch
# User wenzelm
# Date 980975782 -3600
# Node ID 8eb472444705e4e30d019760de52ec29664794a3
# Parent  14b78c0c9f0589df1187eb802114ba7e2bc73cfc
strip_blanks moved to General/symbol.ML;

diff -r 14b78c0c9f05 -r 8eb472444705 src/Pure/Thy/latex.ML
--- 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;