src/Pure/Thy/latex.ML

--- a/src/Pure/Thy/latex.ML	Thu Oct 07 17:20:19 1999 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Oct 07 17:20:58 1999 +0200
@@ -7,7 +7,7 @@
 
 signature LATEX =
 sig
-  datatype token = Basic of OuterLex.token | Markup of string * string
+  datatype token = Basic of OuterLex.token | Markup of string * string | Verbatim of string
   val token_source: token list -> string
   val theory_entry: string -> string
 end;
@@ -51,7 +51,7 @@
 
 structure T = OuterLex;
 
-datatype token = Basic of T.token | Markup of string * string;
+datatype token = Basic of T.token | Markup of string * string | Verbatim of string;
 
 
 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
@@ -69,7 +69,8 @@
         else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
         else output_sym s
       end
-  | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n";
+  | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n"
+  | output_tok (Verbatim txt) = "\n" ^ txt ^ "\n";
 
 
 val output_tokens = implode o map output_tok;