equal
deleted
inserted
replaced
4 LaTeX presentation elements -- based on outer lexical syntax. |
4 LaTeX presentation elements -- based on outer lexical syntax. |
5 *) |
5 *) |
6 |
6 |
7 signature LATEX = |
7 signature LATEX = |
8 sig |
8 sig |
|
9 val output_ascii: string -> string |
9 val output_known_symbols: (string -> bool) * (string -> bool) -> |
10 val output_known_symbols: (string -> bool) * (string -> bool) -> |
10 Symbol.symbol list -> string |
11 Symbol.symbol list -> string |
11 val output_symbols: Symbol.symbol list -> string |
12 val output_symbols: Symbol.symbol list -> string |
12 val output_basic: Token.T -> string |
13 val output_basic: Token.T -> string |
13 val output_markup: string -> string -> string |
14 val output_markup: string -> string -> string |
27 val modes: string list |
28 val modes: string list |
28 end; |
29 end; |
29 |
30 |
30 structure Latex: LATEX = |
31 structure Latex: LATEX = |
31 struct |
32 struct |
|
33 |
|
34 (* literal ASCII *) |
|
35 |
|
36 val output_ascii = |
|
37 translate_string |
|
38 (fn " " => "\\ " |
|
39 | "\t" => "\\ " |
|
40 | "\n" => "\\isanewline\n" |
|
41 | s => |
|
42 if exists_string (fn s' => s = s') "#$%^&_{}~\\" |
|
43 then enclose "{\\char`\\" "}" s else s); |
|
44 |
32 |
45 |
33 (* symbol output *) |
46 (* symbol output *) |
34 |
47 |
35 local |
48 local |
36 |
49 |