strip_blanks;
authorwenzelm
Tue Oct 05 21:18:13 1999 +0200 (1999-10-05)
changeset 7745131005d3a62d
parent 7744 f27d54c1ef39
child 7746 b52c1a632e6a
strip_blanks;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Tue Oct 05 21:17:44 1999 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Oct 05 21:18:13 1999 +0200
     1.3 @@ -53,6 +53,10 @@
     1.4  
     1.5  structure T = OuterLex;
     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 tok =
    1.12    let
    1.13      val out = output_symbol;
    1.14 @@ -61,7 +65,7 @@
    1.15      if T.is_kind T.Command tok then "\\isacommand{" ^ out s ^ "}"
    1.16      else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ out s ^ "}"
    1.17      else if T.is_kind T.String tok then out (quote s)
    1.18 -    else if T.is_kind T.Verbatim tok then "\\isatext{" ^ s ^ "}"
    1.19 +    else if T.is_kind T.Verbatim tok then "\\isatext{" ^ strip_blanks s ^ "}"
    1.20      else out s
    1.21    end;
    1.22