24 "$" => "\\$" | |
24 "$" => "\\$" | |
25 "&" => "\\&" | |
25 "&" => "\\&" | |
26 "%" => "\\%" | |
26 "%" => "\\%" | |
27 "#" => "\\#" | |
27 "#" => "\\#" | |
28 "_" => "\\_" | |
28 "_" => "\\_" | |
29 "{" => "{\\textbraceleft}" | |
29 "{" => "{\\isabraceleft}" | |
30 "}" => "{\\textbraceright}" | |
30 "}" => "{\\isabraceright}" | |
31 "~" => "{\\textasciitilde}" | |
31 "~" => "{\\isatilde}" | |
32 "^" => "{\\textasciicircum}" | |
32 "^" => "{\\isacircum}" | |
33 "\"" => "{\"}" | |
33 "\"" => "{\"}" | |
34 "\\" => "\\verb,\\," | |
34 "\\" => "{\\isabackslash}" | |
35 c => c; |
35 c => c; |
36 |
|
37 val output_chr' = fn |
|
38 "\\" => "{\\textbackslash}" | |
|
39 "|" => "{\\textbar}" | |
|
40 "<" => "{\\textless}" | |
|
41 ">" => "{\\textgreater}" | |
|
42 c => output_chr c; |
|
43 |
|
44 |
36 |
45 (* FIXME replace \<forall> etc. *) |
37 (* FIXME replace \<forall> etc. *) |
46 val output_sym = implode o map output_chr o explode; |
38 val output_sym = implode o map output_chr o explode; |
47 val output_sym' = implode o map output_chr' o explode; |
|
48 |
39 |
49 |
40 |
50 (* token output *) |
41 (* token output *) |
51 |
42 |
52 structure T = OuterLex; |
43 structure T = OuterLex; |
61 (#2 (Library.take_prefix Symbol.is_blank (explode s))))); |
52 (#2 (Library.take_prefix Symbol.is_blank (explode s))))); |
62 |
53 |
63 fun output_tok (Basic tok) = |
54 fun output_tok (Basic tok) = |
64 let val s = T.val_of tok in |
55 let val s = T.val_of tok in |
65 if invisible_token tok then "" |
56 if invisible_token tok then "" |
66 else if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym' s ^ "}" |
57 else if T.is_kind T.Command tok then |
67 else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym' s ^ "}" |
58 if s = "{{" then "{\\isabeginblock}" |
|
59 else if s = "}}" then "{\\isaendblock}" |
|
60 else "\\isacommand{" ^ output_sym s ^ "}" |
|
61 else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then |
|
62 "\\isakeyword{" ^ output_sym s ^ "}" |
68 else if T.is_kind T.String tok then output_sym (quote s) |
63 else if T.is_kind T.String tok then output_sym (quote s) |
69 else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s) |
64 else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s) |
70 else output_sym s |
65 else output_sym s |
71 end |
66 end |
72 | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n" |
67 | output_tok (Markup (cmd, txt)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n" |
73 | output_tok (Verbatim txt) = "\n" ^ txt ^ "\n"; |
68 | output_tok (Verbatim txt) = "\n" ^ strip_blanks txt ^ "\n"; |
74 |
69 |
75 |
70 |
76 val output_tokens = implode o map output_tok; |
71 val output_tokens = implode o map output_tok; |
77 |
72 |
78 |
73 |