src/Pure/Thy/latex.ML
author wenzelm
Wed, 13 Dec 2017 16:18:40 +0100
changeset 67194 1c0a6a957114
parent 67189 725897bbabef
child 67195 6be90977f882
permissions -rw-r--r--
positions as postlude: avoid intrusion of odd %-forms into main tex source;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/latex.ML
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     3
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 14992
diff changeset
     4
LaTeX presentation elements -- based on outer lexical syntax.
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     5
*)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     6
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     7
signature LATEX =
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     8
sig
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
     9
  type text
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    10
  val string: string -> text
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    11
  val text: string * Position.T -> text
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    12
  val block: text list -> text
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    13
  val enclose_body: string -> string -> text list -> text list
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    14
  val output_text: text list -> string
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    15
  val output_positions: Position.T -> text list -> string
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    16
  val output_name: string -> string
58716
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    17
  val output_ascii: string -> string
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
    18
  val latex_control: Symbol.symbol
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
    19
  val is_latex_control: Symbol.symbol -> bool
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
    20
  val embed_raw: string -> string
14924
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
    21
  val output_known_symbols: (string -> bool) * (string -> bool) ->
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
    22
    Symbol.symbol list -> string
11719
49c14348a42b Exported output_symbols.
berghofe
parents: 11012
diff changeset
    23
  val output_symbols: Symbol.symbol list -> string
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    24
  val output_syms: string -> string
61455
0e4c257358cf clarified modules;
wenzelm
parents: 61435
diff changeset
    25
  val output_token: Token.T -> string
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    26
  val begin_delim: string -> string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    27
  val end_delim: string -> string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    28
  val begin_tag: string -> string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    29
  val end_tag: string -> string
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    30
  val environment_block: string -> text list -> text
61462
e16649b70107 clarified Latex.environment;
wenzelm
parents: 61455
diff changeset
    31
  val environment: string -> string -> string
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    32
  val isabelle_body: string -> text list -> text list
14924
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
    33
  val symbol_source: (string -> bool) * (string -> bool) ->
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
    34
    string -> Symbol.symbol list -> string
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    35
  val theory_entry: string -> string
66021
08ab52fb9db5 tuned signature;
wenzelm
parents: 66020
diff changeset
    36
  val latexN: string
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    37
end;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    38
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    39
structure Latex: LATEX =
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    40
struct
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    41
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    42
(* text with positions *)
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    43
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    44
abstype text = Text of string * Position.T | Block of text list
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    45
with
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    46
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    47
fun string s = Text (s, Position.none);
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    48
val text = Text;
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    49
val block = Block;
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    50
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    51
fun output_text texts =
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    52
  let
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    53
    fun output (Text (s, _)) = Buffer.add s
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    54
      | output (Block body) = fold output body;
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    55
  in Buffer.empty |> fold output texts |> Buffer.content end;
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    56
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    57
fun output_positions file_pos texts =
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    58
  let
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    59
    fun position (a, b) = enclose "%:%" "%:%" (a ^ "=" ^ b);
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    60
    fun output (Text (s, pos)) (positions, line) =
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    61
          let
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    62
            val positions' =
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    63
              (case Position.line_of pos of
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    64
                NONE => positions
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    65
              | SOME l => position (apply2 Value.print_int (line, l)) :: positions);
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    66
            val line' = fold_string (fn c => fn n => if c = "\n" then n + 1 else n) s line;
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    67
          in (positions', line') end
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    68
      | output (Block body) res = fold output body res;
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    69
  in
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    70
    (case Position.file_of file_pos of
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    71
      NONE => ""
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    72
    | SOME file =>
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    73
        ([position (Markup.fileN, file), "\\endinput"], 1)
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    74
        |> fold output texts |> #1 |> rev |> cat_lines)
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    75
  end;
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    76
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    77
end;
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    78
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    79
fun enclose_body bg en body = string bg :: body @ [string en];
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    80
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    81
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    82
(* output name for LaTeX macros *)
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    83
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    84
val output_name =
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    85
  translate_string
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    86
    (fn "_" => "UNDERSCORE"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    87
      | "'" => "PRIME"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    88
      | "0" => "ZERO"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    89
      | "1" => "ONE"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    90
      | "2" => "TWO"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    91
      | "3" => "THREE"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    92
      | "4" => "FOUR"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    93
      | "5" => "FIVE"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    94
      | "6" => "SIX"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    95
      | "7" => "SEVEN"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    96
      | "8" => "EIGHT"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    97
      | "9" => "NINE"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    98
      | s => s);
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    99
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
   100
fun enclose_name bg en = enclose bg en o output_name;
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
   101
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
   102
61455
0e4c257358cf clarified modules;
wenzelm
parents: 61435
diff changeset
   103
(* output verbatim ASCII *)
58716
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
   104
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
   105
val output_ascii =
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
   106
  translate_string
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
   107
    (fn " " => "\\ "
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
   108
      | "\t" => "\\ "
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
   109
      | "\n" => "\\isanewline\n"
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
   110
      | s =>
61578
6623c81cb15a avoid ligatures;
wenzelm
parents: 61516
diff changeset
   111
          if exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~"
58716
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
   112
          then enclose "{\\char`\\" "}" s else s);
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
   113
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
   114
61455
0e4c257358cf clarified modules;
wenzelm
parents: 61435
diff changeset
   115
(* output symbols *)
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   116
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   117
val latex_control = "\<^latex>";
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   118
fun is_latex_control s = s = latex_control;
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   119
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   120
val embed_raw = prefix latex_control o cartouche;
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   121
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   122
local
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   123
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   124
val char_table =
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   125
  Symtab.make
63590
4854f7ee0987 proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents: 61595
diff changeset
   126
   [("\007", "{\\isacharbell}"),
4854f7ee0987 proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents: 61595
diff changeset
   127
    ("!", "{\\isacharbang}"),
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   128
    ("\"", "{\\isachardoublequote}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   129
    ("#", "{\\isacharhash}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   130
    ("$", "{\\isachardollar}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   131
    ("%", "{\\isacharpercent}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   132
    ("&", "{\\isacharampersand}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   133
    ("'", "{\\isacharprime}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   134
    ("(", "{\\isacharparenleft}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   135
    (")", "{\\isacharparenright}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   136
    ("*", "{\\isacharasterisk}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   137
    ("+", "{\\isacharplus}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   138
    (",", "{\\isacharcomma}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   139
    ("-", "{\\isacharminus}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   140
    (".", "{\\isachardot}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   141
    ("/", "{\\isacharslash}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   142
    (":", "{\\isacharcolon}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   143
    (";", "{\\isacharsemicolon}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   144
    ("<", "{\\isacharless}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   145
    ("=", "{\\isacharequal}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   146
    (">", "{\\isachargreater}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   147
    ("?", "{\\isacharquery}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   148
    ("@", "{\\isacharat}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   149
    ("[", "{\\isacharbrackleft}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   150
    ("\\", "{\\isacharbackslash}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   151
    ("]", "{\\isacharbrackright}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   152
    ("^", "{\\isacharcircum}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   153
    ("_", "{\\isacharunderscore}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   154
    ("`", "{\\isacharbackquote}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   155
    ("{", "{\\isacharbraceleft}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   156
    ("|", "{\\isacharbar}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   157
    ("}", "{\\isacharbraceright}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   158
    ("~", "{\\isachartilde}")];
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   159
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   160
fun output_chr " " = "\\ "
43709
717e96cf9527 discontinued special treatment of hard tabulators;
wenzelm
parents: 43485
diff changeset
   161
  | output_chr "\t" = "\\ "
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   162
  | output_chr "\n" = "\\isanewline\n"
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   163
  | output_chr c =
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   164
      (case Symtab.lookup char_table c of
49320
94bd2fb83d11 discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
wenzelm
parents: 48628
diff changeset
   165
        SOME s => s
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   166
      | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   167
14924
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
   168
val output_chrs = translate_string output_chr;
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
   169
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
   170
fun output_known_sym (known_sym, known_ctrl) sym =
14874
23c73484312f Symbol.decode;
wenzelm
parents: 14840
diff changeset
   171
  (case Symbol.decode sym of
23c73484312f Symbol.decode;
wenzelm
parents: 14840
diff changeset
   172
    Symbol.Char s => output_chr s
37533
d775bd70f571 explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents: 36959
diff changeset
   173
  | Symbol.UTF8 s => s
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
   174
  | Symbol.Sym s => if known_sym s then enclose_name "{\\isasym" "}" s else output_chrs sym
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
   175
  | Symbol.Control s => if known_ctrl s then enclose_name "\\isactrl" " " s else output_chrs sym
43485
33a24212a72d more tolerant Symbol.decode;
wenzelm
parents: 42290
diff changeset
   176
  | Symbol.Malformed s => error (Symbol.malformed_msg s)
33a24212a72d more tolerant Symbol.decode;
wenzelm
parents: 42290
diff changeset
   177
  | Symbol.EOF => error "Bad EOF symbol");
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   178
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   179
val scan_latex_length =
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   180
  Scan.many1 (fn (s, _) => Symbol.not_eof s andalso not (is_latex_control s))
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   181
    >> (Symbol.length o map Symbol_Pos.symbol) ||
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   182
  Scan.one (is_latex_control o Symbol_Pos.symbol) --
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   183
    Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   184
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   185
fun scan_latex known =
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   186
  Scan.one (is_latex_control o Symbol_Pos.symbol) |--
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   187
    Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) ||
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   188
  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol);
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   189
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   190
fun read scan syms =
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   191
  Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   192
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   193
in
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   194
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   195
fun length_symbols syms =
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   196
  fold Integer.add (these (read scan_latex_length syms)) 0;
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   197
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   198
fun output_known_symbols known syms =
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   199
  if exists is_latex_control syms then
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   200
    (case read (scan_latex known) syms of
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   201
      SOME ss => implode ss
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   202
    | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   203
  else implode (map (output_known_sym known) syms);
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   204
14924
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
   205
val output_symbols = output_known_symbols (K true, K true);
8192
45a7027136e3 added old_symbol_source;
wenzelm
parents: 8117
diff changeset
   206
val output_syms = output_symbols o Symbol.explode;
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   207
27874
f0364f1c0ecf antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents: 27809
diff changeset
   208
val output_syms_antiq =
30589
cbe27c4ef417 Antiquote.Text: keep full position information;
wenzelm
parents: 30573
diff changeset
   209
  (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
61473
34d1913f0b20 clarified control antiquotations: decode control symbol to get name;
wenzelm
parents: 61471
diff changeset
   210
    | Antiquote.Control {name = (name, _), body, ...} =>
34d1913f0b20 clarified control antiquotations: decode control symbol to get name;
wenzelm
parents: 61471
diff changeset
   211
        "\\isaantiqcontrol{" ^ output_symbols (Symbol.explode name) ^ "}" ^
34d1913f0b20 clarified control antiquotations: decode control symbol to get name;
wenzelm
parents: 61471
diff changeset
   212
        output_symbols (map Symbol_Pos.symbol body)
34d1913f0b20 clarified control antiquotations: decode control symbol to get name;
wenzelm
parents: 61471
diff changeset
   213
    | Antiquote.Antiq {body, ...} =>
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   214
        enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
61473
34d1913f0b20 clarified control antiquotations: decode control symbol to get name;
wenzelm
parents: 61471
diff changeset
   215
          (output_symbols (map Symbol_Pos.symbol body)));
22648
8c6b4f7548e3 output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents: 19265
diff changeset
   216
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   217
end;
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   218
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   219
61455
0e4c257358cf clarified modules;
wenzelm
parents: 61435
diff changeset
   220
(* output token *)
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   221
61455
0e4c257358cf clarified modules;
wenzelm
parents: 61435
diff changeset
   222
fun output_token tok =
67173
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   223
  let
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   224
    val s = Token.content_of tok;
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   225
    val output =
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   226
      if Token.is_kind Token.Comment tok then ""
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   227
      else if Token.is_command tok then
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   228
        "\\isacommand{" ^ output_syms s ^ "}"
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   229
      else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   230
        "\\isakeyword{" ^ output_syms s ^ "}"
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   231
      else if Token.is_kind Token.String tok then
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   232
        enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   233
      else if Token.is_kind Token.Alt_String tok then
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   234
        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   235
      else if Token.is_kind Token.Verbatim tok then
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   236
        let
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   237
          val ants = Antiquote.read (Token.input_of tok);
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   238
          val out = implode (map output_syms_antiq ants);
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   239
        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   240
      else if Token.is_kind Token.Cartouche tok then
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   241
        enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   242
      else output_syms s;
67184
ecc786cb3b7b more robust range on preceding comment-line;
wenzelm
parents: 67175
diff changeset
   243
  in output end
67173
e746db6db903 more explicit latex errors;
wenzelm
parents: 67145
diff changeset
   244
  handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   245
61404
a433fecc5ce2 allow control symbols within markup body;
wenzelm
parents: 59809
diff changeset
   246
61455
0e4c257358cf clarified modules;
wenzelm
parents: 61435
diff changeset
   247
(* tags *)
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   248
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
   249
val begin_delim = enclose_name "%\n\\isadelim" "\n";
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
   250
val end_delim = enclose_name "%\n\\endisadelim" "\n";
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
   251
val begin_tag = enclose_name "%\n\\isatag" "\n";
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
   252
fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
11860
36ba0d4a836c flag_markup;
wenzelm
parents: 11719
diff changeset
   253
36ba0d4a836c flag_markup;
wenzelm
parents: 11719
diff changeset
   254
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   255
(* theory presentation *)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   256
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   257
fun environment_delim name =
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   258
 ("%\n\\begin{" ^ output_name name ^ "}%\n",
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   259
  "%\n\\end{" ^ output_name name ^ "}");
61462
e16649b70107 clarified Latex.environment;
wenzelm
parents: 61455
diff changeset
   260
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   261
fun environment_block name = environment_delim name |-> enclose_body #> block;
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   262
fun environment name = environment_delim name |-> enclose;
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   263
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   264
fun isabelle_body_delim name =
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   265
 ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n",
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   266
  "%\n\\end{isabellebody}%\n");
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   267
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   268
fun isabelle_body name = isabelle_body_delim name |-> enclose_body;
9707
067c25edd1bd added tex_trailer;
wenzelm
parents: 9668
diff changeset
   269
58870
e2c0d8ef29cb more flexibile \setisabellecontext, independently of header;
wenzelm
parents: 58861
diff changeset
   270
fun symbol_source known name syms =
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   271
  isabelle_body_delim name
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
   272
  |-> enclose
58870
e2c0d8ef29cb more flexibile \setisabellecontext, independently of header;
wenzelm
parents: 58861
diff changeset
   273
    ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
e2c0d8ef29cb more flexibile \setisabellecontext, independently of header;
wenzelm
parents: 58861
diff changeset
   274
      output_known_symbols known syms);
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   275
9038
63d20536971f session.tex: nsert blank lines in order to guarantee new paragraphs
wenzelm
parents: 8965
diff changeset
   276
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   277
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   278
8460
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   279
(* print mode *)
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   280
8965
d46b36785c70 proper token_translation for latex mode;
wenzelm
parents: 8896
diff changeset
   281
val latexN = "latex";
d46b36785c70 proper token_translation for latex mode;
wenzelm
parents: 8896
diff changeset
   282
8460
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   283
fun latex_output str =
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   284
  let val syms = Symbol.explode str
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   285
  in (output_symbols syms, length_symbols syms) end;
19265
cae36e16f3c0 Output.add_mode: keyword component;
wenzelm
parents: 17218
diff changeset
   286
23621
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   287
fun latex_markup (s, _) =
59123
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59081
diff changeset
   288
  if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59081
diff changeset
   289
  then ("\\isacommand{", "}")
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59081
diff changeset
   290
  else if s = Markup.keyword2N
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59081
diff changeset
   291
  then ("\\isakeyword{", "}")
29325
a205acc94356 Markup.no_output;
wenzelm
parents: 28375
diff changeset
   292
  else Markup.no_output;
10955
36741b4fe109 setuo indent: \isaindent;
wenzelm
parents: 10393
diff changeset
   293
23621
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   294
fun latex_indent "" _ = ""
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   295
  | latex_indent s _ = enclose "\\isaindent{" "}" s;
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   296
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   297
val _ = Output.add_mode latexN latex_output embed_raw;
23703
1b6a2c119151 Markup.add_mode;
wenzelm
parents: 23621
diff changeset
   298
val _ = Markup.add_mode latexN latex_markup;
1b6a2c119151 Markup.add_mode;
wenzelm
parents: 23621
diff changeset
   299
val _ = Pretty.add_mode latexN latex_indent;
8460
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   300
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   301
end;