src/Pure/Thy/latex.ML
author wenzelm
Tue Feb 11 17:44:29 2014 +0100 (2014-02-11)
changeset 55431 e0f20a44ff9d
parent 55033 8e8243975860
child 55744 4a4e5686e091
permissions -rw-r--r--
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;
wenzelm@7726
     1
(*  Title:      Pure/Thy/latex.ML
wenzelm@7726
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@7726
     3
wenzelm@15801
     4
LaTeX presentation elements -- based on outer lexical syntax.
wenzelm@7726
     5
*)
wenzelm@7726
     6
wenzelm@7726
     7
signature LATEX =
wenzelm@7726
     8
sig
wenzelm@14924
     9
  val output_known_symbols: (string -> bool) * (string -> bool) ->
wenzelm@14924
    10
    Symbol.symbol list -> string
berghofe@11719
    11
  val output_symbols: Symbol.symbol list -> string
wenzelm@36959
    12
  val output_basic: Token.T -> string
wenzelm@17081
    13
  val output_markup: string -> string -> string
wenzelm@17081
    14
  val output_markup_env: string -> string -> string
wenzelm@17081
    15
  val output_verbatim: string -> string
wenzelm@17081
    16
  val markup_true: string
wenzelm@17081
    17
  val markup_false: string
wenzelm@17081
    18
  val begin_delim: string -> string
wenzelm@17081
    19
  val end_delim: string -> string
wenzelm@17081
    20
  val begin_tag: string -> string
wenzelm@17081
    21
  val end_tag: string -> string
wenzelm@9707
    22
  val tex_trailer: string
wenzelm@9916
    23
  val isabelle_file: string -> string -> string
wenzelm@14924
    24
  val symbol_source: (string -> bool) * (string -> bool) ->
wenzelm@14924
    25
    string -> Symbol.symbol list -> string
wenzelm@7726
    26
  val theory_entry: string -> string
wenzelm@9135
    27
  val modes: string list
wenzelm@7726
    28
end;
wenzelm@7726
    29
wenzelm@7726
    30
structure Latex: LATEX =
wenzelm@7726
    31
struct
wenzelm@7726
    32
wenzelm@7726
    33
(* symbol output *)
wenzelm@7726
    34
wenzelm@7900
    35
local
wenzelm@7900
    36
wenzelm@40402
    37
val char_table =
wenzelm@40402
    38
  Symtab.make
wenzelm@40402
    39
   [("!", "{\\isacharbang}"),
wenzelm@40402
    40
    ("\"", "{\\isachardoublequote}"),
wenzelm@40402
    41
    ("#", "{\\isacharhash}"),
wenzelm@40402
    42
    ("$", "{\\isachardollar}"),
wenzelm@40402
    43
    ("%", "{\\isacharpercent}"),
wenzelm@40402
    44
    ("&", "{\\isacharampersand}"),
wenzelm@40402
    45
    ("'", "{\\isacharprime}"),
wenzelm@40402
    46
    ("(", "{\\isacharparenleft}"),
wenzelm@40402
    47
    (")", "{\\isacharparenright}"),
wenzelm@40402
    48
    ("*", "{\\isacharasterisk}"),
wenzelm@40402
    49
    ("+", "{\\isacharplus}"),
wenzelm@40402
    50
    (",", "{\\isacharcomma}"),
wenzelm@40402
    51
    ("-", "{\\isacharminus}"),
wenzelm@40402
    52
    (".", "{\\isachardot}"),
wenzelm@40402
    53
    ("/", "{\\isacharslash}"),
wenzelm@40402
    54
    (":", "{\\isacharcolon}"),
wenzelm@40402
    55
    (";", "{\\isacharsemicolon}"),
wenzelm@40402
    56
    ("<", "{\\isacharless}"),
wenzelm@40402
    57
    ("=", "{\\isacharequal}"),
wenzelm@40402
    58
    (">", "{\\isachargreater}"),
wenzelm@40402
    59
    ("?", "{\\isacharquery}"),
wenzelm@40402
    60
    ("@", "{\\isacharat}"),
wenzelm@40402
    61
    ("[", "{\\isacharbrackleft}"),
wenzelm@40402
    62
    ("\\", "{\\isacharbackslash}"),
wenzelm@40402
    63
    ("]", "{\\isacharbrackright}"),
wenzelm@40402
    64
    ("^", "{\\isacharcircum}"),
wenzelm@40402
    65
    ("_", "{\\isacharunderscore}"),
wenzelm@40402
    66
    ("`", "{\\isacharbackquote}"),
wenzelm@40402
    67
    ("{", "{\\isacharbraceleft}"),
wenzelm@40402
    68
    ("|", "{\\isacharbar}"),
wenzelm@40402
    69
    ("}", "{\\isacharbraceright}"),
wenzelm@40402
    70
    ("~", "{\\isachartilde}")];
wenzelm@40402
    71
wenzelm@40402
    72
fun output_chr " " = "\\ "
wenzelm@43709
    73
  | output_chr "\t" = "\\ "
wenzelm@40402
    74
  | output_chr "\n" = "\\isanewline\n"
wenzelm@40402
    75
  | output_chr c =
wenzelm@40402
    76
      (case Symtab.lookup char_table c of
wenzelm@49320
    77
        SOME s => s
wenzelm@40402
    78
      | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
wenzelm@7726
    79
wenzelm@14924
    80
val output_chrs = translate_string output_chr;
wenzelm@14924
    81
wenzelm@14924
    82
fun output_known_sym (known_sym, known_ctrl) sym =
wenzelm@14874
    83
  (case Symbol.decode sym of
wenzelm@14874
    84
    Symbol.Char s => output_chr s
wenzelm@37533
    85
  | Symbol.UTF8 s => s
wenzelm@49320
    86
  | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
wenzelm@49320
    87
  | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
wenzelm@40523
    88
  | Symbol.Raw s => s
wenzelm@43485
    89
  | Symbol.Malformed s => error (Symbol.malformed_msg s)
wenzelm@43485
    90
  | Symbol.EOF => error "Bad EOF symbol");
wenzelm@7900
    91
wenzelm@7900
    92
in
wenzelm@7900
    93
wenzelm@14924
    94
val output_known_symbols = implode oo (map o output_known_sym);
wenzelm@14924
    95
val output_symbols = output_known_symbols (K true, K true);
wenzelm@8192
    96
val output_syms = output_symbols o Symbol.explode;
wenzelm@7900
    97
wenzelm@27874
    98
val output_syms_antiq =
wenzelm@30589
    99
  (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
wenzelm@27874
   100
    | Antiquote.Antiq (ss, _) =>
wenzelm@40402
   101
        enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
wenzelm@53167
   102
          (output_symbols (map Symbol_Pos.symbol ss)));
wenzelm@22648
   103
wenzelm@7900
   104
end;
wenzelm@7726
   105
wenzelm@7726
   106
wenzelm@7726
   107
(* token output *)
wenzelm@7726
   108
wenzelm@36959
   109
val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment;
wenzelm@7756
   110
wenzelm@17081
   111
fun output_basic tok =
wenzelm@36959
   112
  let val s = Token.content_of tok in
wenzelm@17081
   113
    if invisible_token tok then ""
wenzelm@46811
   114
    else if Token.is_command tok then
wenzelm@17081
   115
      "\\isacommand{" ^ output_syms s ^ "}"
wenzelm@50238
   116
    else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
wenzelm@17081
   117
      "\\isakeyword{" ^ output_syms s ^ "}"
wenzelm@36959
   118
    else if Token.is_kind Token.String tok then
wenzelm@49320
   119
      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
wenzelm@36959
   120
    else if Token.is_kind Token.AltString tok then
wenzelm@49320
   121
      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
wenzelm@36959
   122
    else if Token.is_kind Token.Verbatim tok then
wenzelm@27874
   123
      let
wenzelm@36959
   124
        val (txt, pos) = Token.source_position_of tok;
wenzelm@30642
   125
        val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
wenzelm@27874
   126
        val out = implode (map output_syms_antiq ants);
wenzelm@49320
   127
      in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
wenzelm@55033
   128
    else if Token.is_kind Token.Cartouche tok then
wenzelm@55033
   129
      enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
wenzelm@17081
   130
    else output_syms s
wenzelm@17081
   131
  end;
wenzelm@17081
   132
wenzelm@17081
   133
fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n";
wenzelm@7745
   134
wenzelm@17081
   135
fun output_markup_env cmd txt =
wenzelm@17081
   136
  "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
wenzelm@17081
   137
  Symbol.strip_blanks txt ^
wenzelm@17081
   138
  "%\n\\end{isamarkup" ^ cmd ^ "}%\n";
wenzelm@7756
   139
wenzelm@17081
   140
fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
wenzelm@7726
   141
wenzelm@17081
   142
val markup_true = "\\isamarkuptrue%\n";
wenzelm@17081
   143
val markup_false = "\\isamarkupfalse%\n";
wenzelm@7726
   144
wenzelm@17081
   145
val begin_delim = enclose "%\n\\isadelim" "\n";
wenzelm@17081
   146
val end_delim = enclose "%\n\\endisadelim" "\n";
wenzelm@17081
   147
val begin_tag = enclose "%\n\\isatag" "\n";
wenzelm@17081
   148
fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
wenzelm@11860
   149
wenzelm@11860
   150
wenzelm@7726
   151
(* theory presentation *)
wenzelm@7726
   152
wenzelm@9707
   153
val tex_trailer =
wenzelm@9707
   154
  "%%% Local Variables:\n\
wenzelm@9135
   155
  \%%% mode: latex\n\
wenzelm@9135
   156
  \%%% TeX-master: \"root\"\n\
wenzelm@9144
   157
  \%%% End:\n";
wenzelm@8192
   158
wenzelm@9916
   159
fun isabelle_file name txt =
wenzelm@9916
   160
  "%\n\\begin{isabellebody}%\n\
wenzelm@10247
   161
  \\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
wenzelm@9916
   162
  "\\end{isabellebody}%\n" ^ tex_trailer;
wenzelm@9707
   163
wenzelm@14924
   164
fun symbol_source known name syms = isabelle_file name
wenzelm@14924
   165
  ("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
wenzelm@14924
   166
    output_known_symbols known syms);
wenzelm@7726
   167
wenzelm@9038
   168
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
wenzelm@7726
   169
wenzelm@7726
   170
wenzelm@8460
   171
(* print mode *)
wenzelm@8460
   172
wenzelm@8965
   173
val latexN = "latex";
wenzelm@17218
   174
val modes = [latexN, Symbol.xsymbolsN];
wenzelm@8965
   175
wenzelm@8460
   176
fun latex_output str =
wenzelm@8460
   177
  let val syms = Symbol.explode str
wenzelm@23621
   178
  in (output_symbols syms, Symbol.length syms) end;
wenzelm@19265
   179
wenzelm@23621
   180
fun latex_markup (s, _) =
wenzelm@50201
   181
  if s = Markup.commandN orelse s = Markup.keyword1N
wenzelm@49554
   182
    then ("\\isacommand{", "}")
wenzelm@50201
   183
  else if s = Markup.keywordN orelse s = Markup.keyword2N
wenzelm@49554
   184
    then ("\\isakeyword{", "}")
wenzelm@29325
   185
  else Markup.no_output;
wenzelm@10955
   186
wenzelm@23621
   187
fun latex_indent "" _ = ""
wenzelm@23621
   188
  | latex_indent s _ = enclose "\\isaindent{" "}" s;
wenzelm@23621
   189
wenzelm@23621
   190
val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
wenzelm@23703
   191
val _ = Markup.add_mode latexN latex_markup;
wenzelm@23703
   192
val _ = Pretty.add_mode latexN latex_indent;
wenzelm@8460
   193
wenzelm@7726
   194
end;