5 Simple LaTeX presentation primitives (based on outer lexical syntax). |
5 Simple LaTeX presentation primitives (based on outer lexical syntax). |
6 *) |
6 *) |
7 |
7 |
8 signature LATEX = |
8 signature LATEX = |
9 sig |
9 sig |
10 val token_source: OuterLex.token list -> string |
10 val token_source: (OuterLex.token * string option) list -> string |
11 val theory_entry: string -> string |
11 val theory_entry: string -> string |
12 end; |
12 end; |
13 |
13 |
14 structure Latex: LATEX = |
14 structure Latex: LATEX = |
15 struct |
15 struct |
16 |
16 |
17 |
17 |
18 (* symbol output *) |
18 (* symbol output *) |
19 |
|
20 local |
|
21 |
19 |
22 val output_chr = fn |
20 val output_chr = fn |
23 " " => "~" | |
21 " " => "~" | |
24 "\n" => "\\isanewline\n" | |
22 "\n" => "\\isanewline\n" | |
25 "$" => "\\$" | |
23 "$" => "\\$" | |
29 "_" => "\\_" | |
27 "_" => "\\_" | |
30 "{" => "{\\textbraceleft}" | |
28 "{" => "{\\textbraceleft}" | |
31 "}" => "{\\textbraceright}" | |
29 "}" => "{\\textbraceright}" | |
32 "~" => "{\\textasciitilde}" | |
30 "~" => "{\\textasciitilde}" | |
33 "^" => "{\\textasciicircum}" | |
31 "^" => "{\\textasciicircum}" | |
34 (* "\"" => "{\\textquotedblleft}" | (* FIXME !? *)*) |
32 "\"" => "{\"}" | |
35 "\\" => "{\\textbackslash}" | |
33 (* "\\" => "{\\textbackslash}" | FIXME *) |
36 (* "|" => "{\\textbar}" | |
34 "\\" => "\\verb,\\," | |
37 "<" => "{\\textless}" | |
35 "|" => "{|}" | |
38 ">" => "{\\textgreater}" | *) |
36 "<" => "{<}" | |
|
37 ">" => "{>}" | |
39 c => c; |
38 c => c; |
40 |
39 |
41 in |
|
42 |
40 |
43 (* FIXME replace \<forall> etc. *) |
41 (* FIXME replace \<forall> etc. *) |
44 val output_symbol = implode o map output_chr o explode; |
42 val output_sym = implode o map output_chr o explode; |
45 val output_symbols = map output_symbol; |
43 val output_symbols = map output_sym; |
46 |
|
47 end; |
|
48 |
44 |
49 |
45 |
50 (* token output *) |
46 (* token output *) |
51 |
47 |
52 local |
|
53 |
|
54 structure T = OuterLex; |
48 structure T = OuterLex; |
55 |
49 |
56 fun strip_blanks s = |
50 fun output_tok (tok, Some s) = "\\isamarkup" ^ T.val_of tok ^ "{" ^ s ^ "}" |
57 implode (#1 (Library.take_suffix Symbol.is_blank |
51 | output_tok (tok, None) = |
58 (#2 (Library.take_prefix Symbol.is_blank (explode s))))); |
52 let val s = T.val_of tok in |
|
53 if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym s ^ "}" |
|
54 else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym s ^ "}" |
|
55 else if T.is_kind T.String tok then output_sym (quote s) |
|
56 else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s) |
|
57 else output_sym s |
|
58 end; |
59 |
59 |
60 fun output_tok tok = |
60 val output_tokens = map output_tok; |
61 let |
|
62 val out = output_symbol; |
|
63 val s = T.val_of tok; |
|
64 in |
|
65 if T.is_kind T.Command tok then "\\isacommand{" ^ out s ^ "}" |
|
66 else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ out s ^ "}" |
|
67 else if T.is_kind T.String tok then out (quote s) |
|
68 else if T.is_kind T.Verbatim tok then "\\isatext{" ^ strip_blanks s ^ "}" |
|
69 else out s |
|
70 end; |
|
71 |
|
72 (*adhoc tuning of tokens*) |
|
73 fun invisible_token tok = |
|
74 T.is_kind T.Command tok andalso T.val_of tok mem_string ["text", "txt"] orelse |
|
75 T.keyword_with (equal ";") tok orelse T.is_kind T.Comment tok; |
|
76 |
|
77 in |
|
78 |
|
79 val output_tokens = map output_tok o filter_out invisible_token; |
|
80 |
|
81 end; |
|
82 |
61 |
83 |
62 |
84 (* theory presentation *) |
63 (* theory presentation *) |
85 |
64 |
86 fun token_source toks = |
65 fun token_source toks = |