added old_symbol_source;
authorwenzelm
Fri Feb 04 21:44:38 2000 +0100 (2000-02-04)
changeset 819245a7027136e3
parent 8191 6483e7132a70
child 8193 33e4ec7a2daa
added old_symbol_source;
tuned;
src/Pure/Thy/latex.ML
src/Pure/Thy/present.ML
     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  
     2.1 --- a/src/Pure/Thy/present.ML	Fri Feb 04 21:44:04 2000 +0100
     2.2 +++ b/src/Pure/Thy/present.ML	Fri Feb 04 21:44:38 2000 +0100
     2.3 @@ -16,11 +16,12 @@
     2.4    val init: bool -> string -> string list -> string -> Url.T option * bool -> unit
     2.5    val finish: unit -> unit
     2.6    val init_theory: string -> unit
     2.7 -  val verbatim_source: string -> (unit -> string list) -> unit
     2.8 +  val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
     2.9    type token
    2.10    val basic_token: OuterLex.token -> token
    2.11    val markup_token: string * string -> token
    2.12    val verbatim_token: string -> token
    2.13 +  val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
    2.14    val token_source: string -> (unit -> token list) -> unit
    2.15    val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
    2.16    val result: string -> string -> thm -> unit
    2.17 @@ -364,6 +365,9 @@
    2.18  val markup_token = Latex.Markup;
    2.19  val verbatim_token = Latex.Verbatim;
    2.20  
    2.21 +fun old_symbol_source name mk_text =
    2.22 +  with_session () (fn _ => add_tex_source name (Latex.old_symbol_source (mk_text ())));
    2.23 +
    2.24  fun token_source name mk_toks =
    2.25    with_session () (fn _ => add_tex_source name (Latex.token_source (mk_toks ())));
    2.26