adapted to improved presentation;
authorwenzelm
Sun Jun 25 23:55:22 2000 +0200 (2000-06-25)
changeset 91353aa95ab3f02d
parent 9134 b38e94631f19
child 9136 8196955b02ec
adapted to improved presentation;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Sun Jun 25 23:54:56 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Sun Jun 25 23:55:22 2000 +0200
     1.3 @@ -8,11 +8,12 @@
     1.4  
     1.5  signature LATEX =
     1.6  sig
     1.7 -  datatype token = Basic of OuterLex.token | Markup of string * string |
     1.8 -    MarkupEnv of string * string | Verbatim of string
     1.9 +  datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
    1.10 +  val output_tokens: (token * string) list -> string
    1.11 +  val isabelle_file: string -> string
    1.12    val old_symbol_source: string -> Symbol.symbol list -> string
    1.13 -  val token_source: token list -> string
    1.14    val theory_entry: string -> string
    1.15 +  val modes: string list
    1.16    val setup: (theory -> theory) list
    1.17  end;
    1.18  
    1.19 @@ -62,9 +63,9 @@
    1.20  
    1.21  datatype token =
    1.22    Basic of T.token |
    1.23 -  Markup of string * string |
    1.24 -  MarkupEnv of string * string |
    1.25 -  Verbatim of string;
    1.26 +  Markup of string |
    1.27 +  MarkupEnv of string |
    1.28 +  Verbatim;
    1.29  
    1.30  
    1.31  val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    1.32 @@ -73,7 +74,7 @@
    1.33    implode (#1 (Library.take_suffix Symbol.is_blank
    1.34      (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
    1.35  
    1.36 -fun output_tok (Basic tok) =
    1.37 +fun output_tok (Basic tok, _) =
    1.38        let val s = T.val_of tok in
    1.39          if invisible_token tok then ""
    1.40          else if T.is_kind T.Command tok then
    1.41 @@ -86,10 +87,10 @@
    1.42          else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
    1.43          else output_syms s
    1.44        end
    1.45 -  | output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
    1.46 -  | output_tok (MarkupEnv (cmd, txt)) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
    1.47 +  | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
    1.48 +  | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
    1.49        strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
    1.50 -  | output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n";
    1.51 +  | output_tok (Verbatim, txt) = "%\n" ^ strip_blanks txt ^ "\n";
    1.52  
    1.53  
    1.54  val output_tokens = implode o map output_tok;
    1.55 @@ -97,12 +98,16 @@
    1.56  
    1.57  (* theory presentation *)
    1.58  
    1.59 -val isabelle_env = enclose "\\begin{isabelle}%\n" "\\end{isabelle}%\n";
    1.60 +val isabelle_file = enclose
    1.61 +  "\\begin{isabelle}%\n"
    1.62 +  "\\end{isabelle}%\n\
    1.63 +  \%%% Local Variables:\n\
    1.64 +  \%%% mode: latex\n\
    1.65 +  \%%% TeX-master: \"root\"\n\
    1.66 +  \%%% End:\n%";
    1.67  
    1.68  fun old_symbol_source name syms =
    1.69 -  isabelle_env ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
    1.70 -
    1.71 -val token_source = isabelle_env o output_tokens;
    1.72 +  isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
    1.73  
    1.74  fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
    1.75  
    1.76 @@ -110,6 +115,7 @@
    1.77  (* print mode *)
    1.78  
    1.79  val latexN = "latex";
    1.80 +val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN];
    1.81  
    1.82  fun latex_output str =
    1.83    let val syms = Symbol.explode str