--- a/src/Pure/Thy/latex.ML Sun Nov 07 22:42:49 2010 +0100
+++ b/src/Pure/Thy/latex.ML Sun Nov 07 22:51:16 2010 +0100
@@ -30,47 +30,64 @@
structure Latex: LATEX =
struct
+(* literal text *)
+
+local
+ val hex = Int.fmt StringCvt.HEX;
+ fun hex_byte c = hex (ord c div 16) ^ hex (ord c mod 16);
+in
+
+fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}";
+fun enclose_literal txt arg = enclose "{" "}" (literal txt ^ arg);
+
+end;
+
(* symbol output *)
local
-val output_chr = fn
- " " => "\\ " |
- "\n" => "\\isanewline\n" |
- "!" => "{\\isacharbang}" |
- "\"" => "{\\isachardoublequote}" |
- "#" => "{\\isacharhash}" |
- "$" => "{\\isachardollar}" |
- "%" => "{\\isacharpercent}" |
- "&" => "{\\isacharampersand}" |
- "'" => "{\\isacharprime}" |
- "(" => "{\\isacharparenleft}" |
- ")" => "{\\isacharparenright}" |
- "*" => "{\\isacharasterisk}" |
- "+" => "{\\isacharplus}" |
- "," => "{\\isacharcomma}" |
- "-" => "{\\isacharminus}" |
- "." => "{\\isachardot}" |
- "/" => "{\\isacharslash}" |
- ":" => "{\\isacharcolon}" |
- ";" => "{\\isacharsemicolon}" |
- "<" => "{\\isacharless}" |
- "=" => "{\\isacharequal}" |
- ">" => "{\\isachargreater}" |
- "?" => "{\\isacharquery}" |
- "@" => "{\\isacharat}" |
- "[" => "{\\isacharbrackleft}" |
- "\\" => "{\\isacharbackslash}" |
- "]" => "{\\isacharbrackright}" |
- "^" => "{\\isacharcircum}" |
- "_" => "{\\isacharunderscore}" |
- "`" => "{\\isacharbackquote}" |
- "{" => "{\\isacharbraceleft}" |
- "|" => "{\\isacharbar}" |
- "}" => "{\\isacharbraceright}" |
- "~" => "{\\isachartilde}" |
- c => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c;
+val char_table =
+ Symtab.make
+ [("!", "{\\isacharbang}"),
+ ("\"", "{\\isachardoublequote}"),
+ ("#", "{\\isacharhash}"),
+ ("$", "{\\isachardollar}"),
+ ("%", "{\\isacharpercent}"),
+ ("&", "{\\isacharampersand}"),
+ ("'", "{\\isacharprime}"),
+ ("(", "{\\isacharparenleft}"),
+ (")", "{\\isacharparenright}"),
+ ("*", "{\\isacharasterisk}"),
+ ("+", "{\\isacharplus}"),
+ (",", "{\\isacharcomma}"),
+ ("-", "{\\isacharminus}"),
+ (".", "{\\isachardot}"),
+ ("/", "{\\isacharslash}"),
+ (":", "{\\isacharcolon}"),
+ (";", "{\\isacharsemicolon}"),
+ ("<", "{\\isacharless}"),
+ ("=", "{\\isacharequal}"),
+ (">", "{\\isachargreater}"),
+ ("?", "{\\isacharquery}"),
+ ("@", "{\\isacharat}"),
+ ("[", "{\\isacharbrackleft}"),
+ ("\\", "{\\isacharbackslash}"),
+ ("]", "{\\isacharbrackright}"),
+ ("^", "{\\isacharcircum}"),
+ ("_", "{\\isacharunderscore}"),
+ ("`", "{\\isacharbackquote}"),
+ ("{", "{\\isacharbraceleft}"),
+ ("|", "{\\isacharbar}"),
+ ("}", "{\\isacharbraceright}"),
+ ("~", "{\\isachartilde}")];
+
+fun output_chr " " = "\\ "
+ | output_chr "\n" = "\\isanewline\n"
+ | output_chr c =
+ (case Symtab.lookup char_table c of
+ SOME s => enclose_literal c s
+ | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
val output_chrs = translate_string output_chr;
@@ -78,8 +95,12 @@
(case Symbol.decode sym of
Symbol.Char s => output_chr s
| Symbol.UTF8 s => s
- | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
- | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
+ | Symbol.Sym s =>
+ if known_sym s then enclose_literal sym (enclose "{\\isasym" "}" s)
+ else output_chrs sym
+ | Symbol.Ctrl s =>
+ if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s
+ else output_chrs sym
| Symbol.Raw s => s);
in
@@ -91,9 +112,10 @@
val output_syms_antiq =
(fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
| Antiquote.Antiq (ss, _) =>
- enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
- | Antiquote.Open _ => "{\\isaantiqopen}"
- | Antiquote.Close _ => "{\\isaantiqclose}");
+ enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
+ (output_symbols (map Symbol_Pos.symbol ss))
+ | Antiquote.Open _ => enclose_literal "\\<lbrace>" "{\\isaantiqopen}"
+ | Antiquote.Close _ => enclose_literal "\\<rbrace>" "{\\isaantiqclose}");
end;
@@ -110,15 +132,23 @@
else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then
"\\isakeyword{" ^ output_syms s ^ "}"
else if Token.is_kind Token.String tok then
- enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
+ output_syms s |> enclose
+ (enclose_literal "\"" "{\\isachardoublequoteopen}")
+ (enclose_literal "\"" "{\\isachardoublequoteclose}")
else if Token.is_kind Token.AltString tok then
- enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
+ output_syms s |> enclose
+ (enclose_literal "`" "{\\isacharbackquoteopen}")
+ (enclose_literal "`" "{\\isacharbackquoteclose}")
else if Token.is_kind Token.Verbatim tok then
let
val (txt, pos) = Token.source_position_of tok;
val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
val out = implode (map output_syms_antiq ants);
- in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
+ in
+ out |> enclose
+ (enclose_literal "{*" "{\\isacharverbatimopen}")
+ (enclose_literal "*}" "{\\isacharverbatimclose}")
+ end
else output_syms s
end;