--- a/src/Pure/Thy/latex.ML Sat Apr 01 20:26:20 2000 +0200
+++ b/src/Pure/Thy/latex.ML Mon Apr 03 14:00:16 2000 +0200
@@ -7,7 +7,8 @@
signature LATEX =
sig
- datatype token = Basic of OuterLex.token | Markup of string * string | Verbatim of string
+ datatype token = Basic of OuterLex.token | Markup of string * string |
+ MarkupEnv of string * string | Verbatim of string
val old_symbol_source: string -> Symbol.symbol list -> string
val token_source: token list -> string
val theory_entry: string -> string
@@ -57,7 +58,11 @@
structure T = OuterLex;
-datatype token = Basic of T.token | Markup of string * string | Verbatim of string;
+datatype token =
+ Basic of T.token |
+ Markup of string * string |
+ MarkupEnv of string * string |
+ Verbatim of string;
val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
@@ -80,6 +85,8 @@
else output_syms s
end
| output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
+ | output_tok (MarkupEnv (cmd, txt)) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
+ strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
| output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n";