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