src/Pure/Thy/latex.ML
author wenzelm
Tue Jun 06 13:13:25 2017 +0200 (2017-06-06)
changeset 66020 a31760eee09d
parent 64526 01920e390645
child 66021 08ab52fb9db5
permissions -rw-r--r--
discontinued obsolete print mode;
     1 (*  Title:      Pure/Thy/latex.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 LaTeX presentation elements -- based on outer lexical syntax.
     5 *)
     6 
     7 signature LATEX =
     8 sig
     9   val output_ascii: string -> string
    10   val latex_control: Symbol.symbol
    11   val is_latex_control: Symbol.symbol -> bool
    12   val embed_raw: string -> string
    13   val output_known_symbols: (string -> bool) * (string -> bool) ->
    14     Symbol.symbol list -> string
    15   val output_symbols: Symbol.symbol list -> string
    16   val output_token: Token.T -> string
    17   val begin_delim: string -> string
    18   val end_delim: string -> string
    19   val begin_tag: string -> string
    20   val end_tag: string -> string
    21   val environment: string -> string -> string
    22   val tex_trailer: string
    23   val isabelle_theory: string -> string -> string
    24   val symbol_source: (string -> bool) * (string -> bool) ->
    25     string -> Symbol.symbol list -> string
    26   val theory_entry: string -> string
    27   val modes: string list
    28 end;
    29 
    30 structure Latex: LATEX =
    31 struct
    32 
    33 (* output verbatim ASCII *)
    34 
    35 val output_ascii =
    36   translate_string
    37     (fn " " => "\\ "
    38       | "\t" => "\\ "
    39       | "\n" => "\\isanewline\n"
    40       | s =>
    41           if exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~"
    42           then enclose "{\\char`\\" "}" s else s);
    43 
    44 
    45 (* output symbols *)
    46 
    47 val latex_control = "\<^latex>";
    48 fun is_latex_control s = s = latex_control;
    49 
    50 val embed_raw = prefix latex_control o cartouche;
    51 
    52 local
    53 
    54 val char_table =
    55   Symtab.make
    56    [("\007", "{\\isacharbell}"),
    57     ("!", "{\\isacharbang}"),
    58     ("\"", "{\\isachardoublequote}"),
    59     ("#", "{\\isacharhash}"),
    60     ("$", "{\\isachardollar}"),
    61     ("%", "{\\isacharpercent}"),
    62     ("&", "{\\isacharampersand}"),
    63     ("'", "{\\isacharprime}"),
    64     ("(", "{\\isacharparenleft}"),
    65     (")", "{\\isacharparenright}"),
    66     ("*", "{\\isacharasterisk}"),
    67     ("+", "{\\isacharplus}"),
    68     (",", "{\\isacharcomma}"),
    69     ("-", "{\\isacharminus}"),
    70     (".", "{\\isachardot}"),
    71     ("/", "{\\isacharslash}"),
    72     (":", "{\\isacharcolon}"),
    73     (";", "{\\isacharsemicolon}"),
    74     ("<", "{\\isacharless}"),
    75     ("=", "{\\isacharequal}"),
    76     (">", "{\\isachargreater}"),
    77     ("?", "{\\isacharquery}"),
    78     ("@", "{\\isacharat}"),
    79     ("[", "{\\isacharbrackleft}"),
    80     ("\\", "{\\isacharbackslash}"),
    81     ("]", "{\\isacharbrackright}"),
    82     ("^", "{\\isacharcircum}"),
    83     ("_", "{\\isacharunderscore}"),
    84     ("`", "{\\isacharbackquote}"),
    85     ("{", "{\\isacharbraceleft}"),
    86     ("|", "{\\isacharbar}"),
    87     ("}", "{\\isacharbraceright}"),
    88     ("~", "{\\isachartilde}")];
    89 
    90 fun output_chr " " = "\\ "
    91   | output_chr "\t" = "\\ "
    92   | output_chr "\n" = "\\isanewline\n"
    93   | output_chr c =
    94       (case Symtab.lookup char_table c of
    95         SOME s => s
    96       | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
    97 
    98 val output_chrs = translate_string output_chr;
    99 
   100 fun output_known_sym (known_sym, known_ctrl) sym =
   101   (case Symbol.decode sym of
   102     Symbol.Char s => output_chr s
   103   | Symbol.UTF8 s => s
   104   | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
   105   | Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
   106   | Symbol.Malformed s => error (Symbol.malformed_msg s)
   107   | Symbol.EOF => error "Bad EOF symbol");
   108 
   109 val scan_latex_length =
   110   Scan.many1 (fn (s, _) => Symbol.not_eof s andalso not (is_latex_control s))
   111     >> (Symbol.length o map Symbol_Pos.symbol) ||
   112   Scan.one (is_latex_control o Symbol_Pos.symbol) --
   113     Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
   114 
   115 fun scan_latex known =
   116   Scan.one (is_latex_control o Symbol_Pos.symbol) |--
   117     Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) ||
   118   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol);
   119 
   120 fun read scan syms =
   121   Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
   122 
   123 in
   124 
   125 fun length_symbols syms =
   126   fold Integer.add (these (read scan_latex_length syms)) 0;
   127 
   128 fun output_known_symbols known syms =
   129   if exists is_latex_control syms then
   130     (case read (scan_latex known) syms of
   131       SOME ss => implode ss
   132     | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
   133   else implode (map (output_known_sym known) syms);
   134 
   135 val output_symbols = output_known_symbols (K true, K true);
   136 val output_syms = output_symbols o Symbol.explode;
   137 
   138 val output_syms_antiq =
   139   (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
   140     | Antiquote.Control {name = (name, _), body, ...} =>
   141         "\\isaantiqcontrol{" ^ output_symbols (Symbol.explode name) ^ "}" ^
   142         output_symbols (map Symbol_Pos.symbol body)
   143     | Antiquote.Antiq {body, ...} =>
   144         enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
   145           (output_symbols (map Symbol_Pos.symbol body)));
   146 
   147 end;
   148 
   149 
   150 (* output token *)
   151 
   152 fun output_token tok =
   153   let val s = Token.content_of tok in
   154     if Token.is_kind Token.Comment tok then ""
   155     else if Token.is_command tok then
   156       "\\isacommand{" ^ output_syms s ^ "}"
   157     else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
   158       "\\isakeyword{" ^ output_syms s ^ "}"
   159     else if Token.is_kind Token.String tok then
   160       enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
   161     else if Token.is_kind Token.Alt_String tok then
   162       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
   163     else if Token.is_kind Token.Verbatim tok then
   164       let
   165         val ants = Antiquote.read (Token.input_of tok);
   166         val out = implode (map output_syms_antiq ants);
   167       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
   168     else if Token.is_kind Token.Cartouche tok then
   169       enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
   170     else output_syms s
   171   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
   172 
   173 
   174 (* tags *)
   175 
   176 val begin_delim = enclose "%\n\\isadelim" "\n";
   177 val end_delim = enclose "%\n\\endisadelim" "\n";
   178 val begin_tag = enclose "%\n\\isatag" "\n";
   179 fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
   180 
   181 
   182 (* theory presentation *)
   183 
   184 fun environment name =
   185   enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}");
   186 
   187 val tex_trailer =
   188   "%%% Local Variables:\n\
   189   \%%% mode: latex\n\
   190   \%%% TeX-master: \"root\"\n\
   191   \%%% End:\n";
   192 
   193 fun isabelle_theory name txt =
   194   "%\n\\begin{isabellebody}%\n\
   195   \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
   196   "%\n\\end{isabellebody}%\n" ^ tex_trailer;
   197 
   198 fun symbol_source known name syms =
   199   isabelle_theory name
   200     ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
   201       output_known_symbols known syms);
   202 
   203 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
   204 
   205 
   206 (* print mode *)
   207 
   208 val latexN = "latex";
   209 val modes = [latexN];
   210 
   211 fun latex_output str =
   212   let val syms = Symbol.explode str
   213   in (output_symbols syms, length_symbols syms) end;
   214 
   215 fun latex_markup (s, _) =
   216   if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
   217   then ("\\isacommand{", "}")
   218   else if s = Markup.keyword2N
   219   then ("\\isakeyword{", "}")
   220   else Markup.no_output;
   221 
   222 fun latex_indent "" _ = ""
   223   | latex_indent s _ = enclose "\\isaindent{" "}" s;
   224 
   225 val _ = Output.add_mode latexN latex_output embed_raw;
   226 val _ = Markup.add_mode latexN latex_markup;
   227 val _ = Pretty.add_mode latexN latex_indent;
   228 
   229 end;