src/Pure/Thy/latex.ML

 Simple LaTeX presentation primitives (based on outer lexical syntax).
 *)
 
 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;
 
 structure Latex: LATEX =

 
 (* token output *)
 
 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;
 
 fun strip_blanks 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
-  | 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;