# HG changeset patch
# User wenzelm
# Date 961970122 -7200
# Node ID 3aa95ab3f02dadd9221cbd957473448a331deb58
# Parent  b38e94631f199e418a39c72b66b6d001db120e1f
adapted to improved presentation;

diff -r b38e94631f19 -r 3aa95ab3f02d src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Jun 25 23:54:56 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Sun Jun 25 23:55:22 2000 +0200
@@ -8,11 +8,12 @@
 
 signature LATEX =
 sig
-  datatype token = Basic of OuterLex.token | Markup of string * string |
-    MarkupEnv of string * string | Verbatim of string
+  datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
+  val output_tokens: (token * string) list -> string
+  val isabelle_file: string -> string
   val old_symbol_source: string -> Symbol.symbol list -> string
-  val token_source: token list -> string
   val theory_entry: string -> string
+  val modes: string list
   val setup: (theory -> theory) list
 end;
 
@@ -62,9 +63,9 @@
 
 datatype token =
   Basic of T.token |
-  Markup of string * string |
-  MarkupEnv of string * string |
-  Verbatim of string;
+  Markup of string |
+  MarkupEnv of string |
+  Verbatim;
 
 
 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
@@ -73,7 +74,7 @@
   implode (#1 (Library.take_suffix Symbol.is_blank
     (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
 
-fun output_tok (Basic tok) =
+fun output_tok (Basic tok, _) =
       let val s = T.val_of tok in
         if invisible_token tok then ""
         else if T.is_kind T.Command tok then
@@ -86,10 +87,10 @@
         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
         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" ^
+  | 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";
+  | output_tok (Verbatim, txt) = "%\n" ^ strip_blanks txt ^ "\n";
 
 
 val output_tokens = implode o map output_tok;
@@ -97,12 +98,16 @@
 
 (* theory presentation *)
 
-val isabelle_env = enclose "\\begin{isabelle}%\n" "\\end{isabelle}%\n";
+val isabelle_file = enclose
+  "\\begin{isabelle}%\n"
+  "\\end{isabelle}%\n\
+  \%%% Local Variables:\n\
+  \%%% mode: latex\n\
+  \%%% TeX-master: \"root\"\n\
+  \%%% End:\n%";
 
 fun old_symbol_source name syms =
-  isabelle_env ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
-
-val token_source = isabelle_env o output_tokens;
+  isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
 
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
 
@@ -110,6 +115,7 @@
 (* print mode *)
 
 val latexN = "latex";
+val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN];
 
 fun latex_output str =
   let val syms = Symbol.explode str