1.1 --- a/src/Pure/Thy/latex.ML	Wed Jan 31 22:15:53 2001 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Wed Jan 31 22:16:22 2001 +0100
     1.3 @@ -92,10 +92,6 @@
     1.4  
     1.5  val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
     1.6  
     1.7 -fun strip_blanks s =
     1.8 -  implode (#1 (Library.take_suffix Symbol.is_blank
     1.9 -    (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
    1.10 -
    1.11  fun output_tok (Basic tok, _) =
    1.12        let val s = T.val_of tok in
    1.13          if invisible_token tok then ""
    1.14 @@ -107,10 +103,11 @@
    1.15          else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
    1.16          else output_syms s
    1.17        end
    1.18 -  | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "%\n}\n"
    1.19 +  | output_tok (Markup cmd, txt) =
    1.20 +      "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n"
    1.21    | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
    1.22 -      strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
    1.23 -  | output_tok (Verbatim, txt) = "%\n" ^ strip_blanks txt ^ "\n";
    1.24 +      Symbol.strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
    1.25 +  | output_tok (Verbatim, txt) = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
    1.26  
    1.27  
    1.28  val output_tokens = implode o map output_tok;