# HG changeset patch # User berghofe # Date 1002732073 -7200 # Node ID 49c14348a42b8818a33e8dc3c9d1e766982caf74 # Parent 92706a69daccdf59de6afe2864bd0f60ae6ff598 Exported output_symbols. diff -r 92706a69dacc -r 49c14348a42b src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Wed Oct 10 18:40:46 2001 +0200 +++ b/src/Pure/Thy/latex.ML Wed Oct 10 18:41:13 2001 +0200 @@ -8,6 +8,7 @@ signature LATEX = sig + val output_symbols: Symbol.symbol list -> string datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim val output_tokens: (token * string) list -> string val tex_trailer: string