src/Pure/Thy/latex.ML
changeset 8460 274426d1adbc
parent 8192 45a7027136e3
child 8499 8958ece3bbdf
     1.1 --- a/src/Pure/Thy/latex.ML	Wed Mar 15 18:22:39 2000 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Wed Mar 15 18:24:27 2000 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Simple LaTeX presentation primitives (based on outer lexical syntax).
     1.8 +LaTeX presentation primitives (based on outer lexical syntax).
     1.9  *)
    1.10  
    1.11  signature LATEX =
    1.12 @@ -88,12 +88,21 @@
    1.13  
    1.14  (* theory presentation *)
    1.15  
    1.16 -val isabelle_simple = enclose "\\begin{isabellesimple}%\n" "\\end{isabellesimple}%\n";
    1.17 +val isabelle_env = enclose "\\begin{isabelle}%\n" "\\end{isabelle}%\n";
    1.18  
    1.19 -val old_symbol_source = isabelle_simple o output_symbols;
    1.20 -val token_source = isabelle_simple o output_tokens;
    1.21 +val old_symbol_source = isabelle_env o output_symbols;
    1.22 +val token_source = isabelle_env o output_tokens;
    1.23  
    1.24  fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
    1.25  
    1.26  
    1.27 +(* print mode *)
    1.28 +
    1.29 +fun latex_output str =
    1.30 +  let val syms = Symbol.explode str
    1.31 +  in (output_symbols syms, real (Symbol.length syms)) end;
    1.32 +
    1.33 +val _ = Symbol.add_mode "latex" latex_output;
    1.34 +
    1.35 +
    1.36  end;