src/Pure/Thy/latex.ML
changeset 8192 45a7027136e3
parent 8117 0a6173c9b2d0
child 8460 274426d1adbc
     1.1 --- a/src/Pure/Thy/latex.ML	Fri Feb 04 21:44:04 2000 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Fri Feb 04 21:44:38 2000 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  signature LATEX =
     1.5  sig
     1.6    datatype token = Basic of OuterLex.token | Markup of string * string | Verbatim of string
     1.7 +  val old_symbol_source: Symbol.symbol list -> string
     1.8    val token_source: token list -> string
     1.9    val theory_entry: string -> string
    1.10  end;
    1.11 @@ -46,7 +47,8 @@
    1.12  
    1.13  in
    1.14  
    1.15 -val output_syms = implode o map output_sym o Symbol.explode;
    1.16 +val output_symbols = implode o map output_sym;
    1.17 +val output_syms = output_symbols o Symbol.explode;
    1.18  
    1.19  end;
    1.20  
    1.21 @@ -86,8 +88,10 @@
    1.22  
    1.23  (* theory presentation *)
    1.24  
    1.25 -fun token_source toks =
    1.26 -  "\\begin{isabellesimple}%\n" ^ output_tokens toks ^ "\\end{isabellesimple}\n";
    1.27 +val isabelle_simple = enclose "\\begin{isabellesimple}%\n" "\\end{isabellesimple}%\n";
    1.28 +
    1.29 +val old_symbol_source = isabelle_simple o output_symbols;
    1.30 +val token_source = isabelle_simple o output_tokens;
    1.31  
    1.32  fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
    1.33