diff -r 01e3d545ced8 -r f9f8660de23f src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Oct 06 18:12:05 1999 +0200
+++ b/src/Pure/Thy/latex.ML	Wed Oct 06 18:12:35 1999 +0200
@@ -7,7 +7,8 @@
 
 signature LATEX =
 sig
-  val token_source: (OuterLex.token * string option) list -> string
+  datatype token = Basic of OuterLex.token | Markup of string * string
+  val token_source: token list -> string
   val theory_entry: string -> string
 end;
 
@@ -30,40 +31,54 @@
   "~" => "{\\textasciitilde}" |
   "^" => "{\\textasciicircum}" |
   "\"" => "{\"}" |
-(*  "\\" => "{\\textbackslash}" |  FIXME *)
   "\\" => "\\verb,\\," |
-  "|" => "{|}" |
-  "<" => "{<}" |
-  ">" => "{>}" |
   c => c;
 
+val output_chr' = fn
+  "\\" => "{\\textbackslash}" |
+  "|" => "{\\textbar}" |
+  "<" => "{\\textless}" |
+  ">" => "{\\textgreater}" |
+  c => output_chr c;
+
 
 (* FIXME replace \<forall> etc. *)
 val output_sym = implode o map output_chr o explode;
-val output_symbols = map output_sym;
+val output_sym' = implode o map output_chr' o explode;
 
 
 (* token output *)
 
 structure T = OuterLex;
 
-fun output_tok (tok, Some s) = "\\isamarkup" ^ T.val_of tok ^ "{" ^ s ^ "}"
-  | output_tok (tok, None) =
+datatype token = Basic of T.token | Markup of string * string;
+
+
+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 T.is_kind T.Command tok then "\\isacommand{" ^ output_sym s ^ "}"
-        else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym s ^ "}"
+        if invisible_token tok then ""
+        else if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym' s ^ "}"
+        else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym' s ^ "}"
         else if T.is_kind T.String tok then output_sym (quote s)
         else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
         else output_sym s
-      end;
+      end
+  | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n";
 
-val output_tokens = map output_tok;
+
+val output_tokens = implode o map output_tok;
 
 
 (* theory presentation *)
 
 fun token_source toks =
-  "\\begin{isabellesimple}\n" ^ implode (output_tokens toks) ^ "\\end{isabellesimple}\n";
+  "\\begin{isabellesimple}\n" ^ output_tokens toks ^ "\\end{isabellesimple}\n";
 
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";