src/Pure/Thy/latex.ML
author wenzelm
Sun, 05 Dec 2021 16:26:03 +0100
changeset 74882 947bb3e09a88
parent 74881 1e84ae3e886e
child 74883 f32ac01aef5e
permissions -rw-r--r--
prefer symbolic Latex.environment (typeset in Isabelle/Scala);
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
73754
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
     2
    Author:     Makarius
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     3
73754
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
     4
LaTeX output of theory sources.
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
73780
466fae6bf22e compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents: 73779
diff changeset
     9
  type text = XML.body
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    10
  val text: string * Position.T -> text
73780
466fae6bf22e compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents: 73779
diff changeset
    11
  val string: string -> text
466fae6bf22e compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents: 73779
diff changeset
    12
  val block: text -> XML.tree
74784
d2522bb4db1b symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents: 74781
diff changeset
    13
  val output: text -> text
74790
3ce6fb9db485 more symbolic latex_output via XML;
wenzelm
parents: 74786
diff changeset
    14
  val macro0: string -> text
3ce6fb9db485 more symbolic latex_output via XML;
wenzelm
parents: 74786
diff changeset
    15
  val macro: string -> text -> text
3ce6fb9db485 more symbolic latex_output via XML;
wenzelm
parents: 74786
diff changeset
    16
  val environment: string -> text -> text
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    17
  val output_name: string -> string
58716
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    18
  val output_ascii: string -> string
71899
9a12eb655f67 tuned signature;
wenzelm
parents: 69346
diff changeset
    19
  val output_ascii_breakable: string -> string -> string
11719
49c14348a42b Exported output_symbols.
berghofe
parents: 11012
diff changeset
    20
  val output_symbols: Symbol.symbol list -> string
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    21
  val output_syms: string -> string
67461
aad5c0982c3d tuned signature;
wenzelm
parents: 67428
diff changeset
    22
  val symbols: Symbol_Pos.T list -> text
aad5c0982c3d tuned signature;
wenzelm
parents: 67428
diff changeset
    23
  val symbols_output: Symbol_Pos.T list -> text
73780
466fae6bf22e compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents: 73779
diff changeset
    24
  val isabelle_body: string -> text -> text
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    25
  val theory_entry: string -> string
73754
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
    26
  type index_item = {text: text, like: string}
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
    27
  type index_entry = {items: index_item list, def: bool}
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
    28
  val index_entry: index_entry -> text
73763
eccc4a13216d clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents: 73754
diff changeset
    29
  val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
66021
08ab52fb9db5 tuned signature;
wenzelm
parents: 66020
diff changeset
    30
  val latexN: string
69346
3c29edccf739 expose latex mode operations, to facilitate adhoc changes to it;
wenzelm
parents: 67462
diff changeset
    31
  val latex_output: string -> string * int
3c29edccf739 expose latex mode operations, to facilitate adhoc changes to it;
wenzelm
parents: 67462
diff changeset
    32
  val latex_markup: string * Properties.T -> Markup.output
3c29edccf739 expose latex mode operations, to facilitate adhoc changes to it;
wenzelm
parents: 67462
diff changeset
    33
  val latex_indent: string -> int -> string
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    34
end;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    35
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    36
structure Latex: LATEX =
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    37
struct
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    38
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    39
(* text with positions *)
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    40
73780
466fae6bf22e compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents: 73779
diff changeset
    41
type text = XML.body;
73754
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
    42
74779
5fca489a6ac1 tuned output --- less redundancy;
wenzelm
parents: 73780
diff changeset
    43
fun text (s, pos) =
5fca489a6ac1 tuned output --- less redundancy;
wenzelm
parents: 73780
diff changeset
    44
  if s = "" then []
5fca489a6ac1 tuned output --- less redundancy;
wenzelm
parents: 73780
diff changeset
    45
  else if pos = Position.none then [XML.Text s]
5fca489a6ac1 tuned output --- less redundancy;
wenzelm
parents: 73780
diff changeset
    46
  else [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])];
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    47
73780
466fae6bf22e compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents: 73779
diff changeset
    48
fun string s = text (s, Position.none);
466fae6bf22e compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents: 73779
diff changeset
    49
466fae6bf22e compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents: 73779
diff changeset
    50
fun block body = XML.Elem (Markup.document_latex, body);
67195
6be90977f882 avoid redundant positions;
wenzelm
parents: 67194
diff changeset
    51
74784
d2522bb4db1b symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents: 74781
diff changeset
    52
fun output body = [XML.Elem (Markup.latex_output, body)];
d2522bb4db1b symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents: 74781
diff changeset
    53
74790
3ce6fb9db485 more symbolic latex_output via XML;
wenzelm
parents: 74786
diff changeset
    54
fun macro0 name = [XML.Elem (Markup.latex_macro0 name, [])];
3ce6fb9db485 more symbolic latex_output via XML;
wenzelm
parents: 74786
diff changeset
    55
fun macro name body = [XML.Elem (Markup.latex_macro name, body)];
3ce6fb9db485 more symbolic latex_output via XML;
wenzelm
parents: 74786
diff changeset
    56
fun environment name body = [XML.Elem (Markup.latex_environment name, body)];
3ce6fb9db485 more symbolic latex_output via XML;
wenzelm
parents: 74786
diff changeset
    57
67194
1c0a6a957114 positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents: 67189
diff changeset
    58
67145
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    59
(* output name for LaTeX macros *)
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    60
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    61
val output_name =
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    62
  translate_string
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    63
    (fn "_" => "UNDERSCORE"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    64
      | "'" => "PRIME"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    65
      | "0" => "ZERO"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    66
      | "1" => "ONE"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    67
      | "2" => "TWO"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    68
      | "3" => "THREE"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    69
      | "4" => "FOUR"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    70
      | "5" => "FIVE"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    71
      | "6" => "SIX"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    72
      | "7" => "SEVEN"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    73
      | "8" => "EIGHT"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    74
      | "9" => "NINE"
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    75
      | s => s);
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    76
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    77
fun enclose_name bg en = enclose bg en o output_name;
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    78
e77c5bfca9aa name mangling for Latex macros;
wenzelm
parents: 66021
diff changeset
    79
61455
0e4c257358cf clarified modules;
wenzelm
parents: 61435
diff changeset
    80
(* output verbatim ASCII *)
58716
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    81
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    82
val output_ascii =
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    83
  translate_string
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    84
    (fn " " => "\\ "
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    85
      | "\t" => "\\ "
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    86
      | "\n" => "\\isanewline\n"
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    87
      | s =>
72315
8162ca81ea8a suppress ligatures more robustly, notably for lualatex;
wenzelm
parents: 71899
diff changeset
    88
          s
8162ca81ea8a suppress ligatures more robustly, notably for lualatex;
wenzelm
parents: 71899
diff changeset
    89
          |> exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~" ? enclose "{\\char`\\" "}"
8162ca81ea8a suppress ligatures more robustly, notably for lualatex;
wenzelm
parents: 71899
diff changeset
    90
          |> suffix "{\\kern0pt}");
58716
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    91
71899
9a12eb655f67 tuned signature;
wenzelm
parents: 69346
diff changeset
    92
fun output_ascii_breakable sep =
9a12eb655f67 tuned signature;
wenzelm
parents: 69346
diff changeset
    93
  space_explode sep
9a12eb655f67 tuned signature;
wenzelm
parents: 69346
diff changeset
    94
  #> map output_ascii
9a12eb655f67 tuned signature;
wenzelm
parents: 69346
diff changeset
    95
  #> space_implode (output_ascii sep ^ "\\discretionary{}{}{}");
9a12eb655f67 tuned signature;
wenzelm
parents: 69346
diff changeset
    96
58716
23a380cc45f4 official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents: 55828
diff changeset
    97
61455
0e4c257358cf clarified modules;
wenzelm
parents: 61435
diff changeset
    98
(* output symbols *)
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    99
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   100
local
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   101
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   102
val char_table =
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   103
  Symtab.make
63590
4854f7ee0987 proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents: 61595
diff changeset
   104
   [("\007", "{\\isacharbell}"),
4854f7ee0987 proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents: 61595
diff changeset
   105
    ("!", "{\\isacharbang}"),
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   106
    ("\"", "{\\isachardoublequote}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   107
    ("#", "{\\isacharhash}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   108
    ("$", "{\\isachardollar}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   109
    ("%", "{\\isacharpercent}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   110
    ("&", "{\\isacharampersand}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   111
    ("'", "{\\isacharprime}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   112
    ("(", "{\\isacharparenleft}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   113
    (")", "{\\isacharparenright}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   114
    ("*", "{\\isacharasterisk}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   115
    ("+", "{\\isacharplus}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   116
    (",", "{\\isacharcomma}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   117
    ("-", "{\\isacharminus}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   118
    (".", "{\\isachardot}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   119
    ("/", "{\\isacharslash}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   120
    (":", "{\\isacharcolon}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   121
    (";", "{\\isacharsemicolon}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   122
    ("<", "{\\isacharless}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   123
    ("=", "{\\isacharequal}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   124
    (">", "{\\isachargreater}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   125
    ("?", "{\\isacharquery}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   126
    ("@", "{\\isacharat}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   127
    ("[", "{\\isacharbrackleft}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   128
    ("\\", "{\\isacharbackslash}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   129
    ("]", "{\\isacharbrackright}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   130
    ("^", "{\\isacharcircum}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   131
    ("_", "{\\isacharunderscore}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   132
    ("`", "{\\isacharbackquote}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   133
    ("{", "{\\isacharbraceleft}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   134
    ("|", "{\\isacharbar}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   135
    ("}", "{\\isacharbraceright}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   136
    ("~", "{\\isachartilde}")];
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   137
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   138
fun output_chr " " = "\\ "
43709
717e96cf9527 discontinued special treatment of hard tabulators;
wenzelm
parents: 43485
diff changeset
   139
  | 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
   140
  | 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
   141
  | output_chr c =
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   142
      (case Symtab.lookup char_table c of
72315
8162ca81ea8a suppress ligatures more robustly, notably for lualatex;
wenzelm
parents: 71899
diff changeset
   143
        SOME s => s ^ "{\\kern0pt}"
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   144
      | 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
   145
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   146
fun output_sym sym =
14874
23c73484312f Symbol.decode;
wenzelm
parents: 14840
diff changeset
   147
  (case Symbol.decode sym of
23c73484312f Symbol.decode;
wenzelm
parents: 14840
diff changeset
   148
    Symbol.Char s => output_chr s
37533
d775bd70f571 explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents: 36959
diff changeset
   149
  | Symbol.UTF8 s => s
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   150
  | Symbol.Sym s => enclose_name "{\\isasym" "}" s
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   151
  | Symbol.Control s => enclose_name "\\isactrl" " " s
43485
33a24212a72d more tolerant Symbol.decode;
wenzelm
parents: 42290
diff changeset
   152
  | Symbol.Malformed s => error (Symbol.malformed_msg s)
33a24212a72d more tolerant Symbol.decode;
wenzelm
parents: 42290
diff changeset
   153
  | Symbol.EOF => error "Bad EOF symbol");
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   154
67428
dd8e40f46962 clarified signature;
wenzelm
parents: 67358
diff changeset
   155
open Basic_Symbol_Pos;
dd8e40f46962 clarified signature;
wenzelm
parents: 67358
diff changeset
   156
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   157
val scan_latex_length =
67428
dd8e40f46962 clarified signature;
wenzelm
parents: 67358
diff changeset
   158
  Scan.many1 (fn (s, _) => s <> Symbol.latex andalso Symbol.not_eof s)
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   159
    >> (Symbol.length o map Symbol_Pos.symbol) ||
67428
dd8e40f46962 clarified signature;
wenzelm
parents: 67358
diff changeset
   160
  $$ Symbol.latex -- Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   161
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   162
val scan_latex =
67428
dd8e40f46962 clarified signature;
wenzelm
parents: 67358
diff changeset
   163
  $$ Symbol.latex |-- Symbol_Pos.scan_cartouche_content "Embedded LaTeX: "
dd8e40f46962 clarified signature;
wenzelm
parents: 67358
diff changeset
   164
    >> (implode o map Symbol_Pos.symbol) ||
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   165
  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol);
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   166
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   167
fun read scan syms =
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   168
  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
   169
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   170
in
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   171
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   172
fun length_symbols syms =
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   173
  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
   174
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   175
fun output_symbols syms =
67428
dd8e40f46962 clarified signature;
wenzelm
parents: 67358
diff changeset
   176
  if member (op =) syms Symbol.latex then
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   177
    (case read scan_latex syms of
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   178
      SOME ss => implode ss
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   179
    | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   180
  else implode (map output_sym syms);
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63590
diff changeset
   181
8192
45a7027136e3 added old_symbol_source;
wenzelm
parents: 8117
diff changeset
   182
val output_syms = output_symbols o Symbol.explode;
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   183
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   184
end;
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   185
67461
aad5c0982c3d tuned signature;
wenzelm
parents: 67428
diff changeset
   186
fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
aad5c0982c3d tuned signature;
wenzelm
parents: 67428
diff changeset
   187
fun symbols_output syms =
aad5c0982c3d tuned signature;
wenzelm
parents: 67428
diff changeset
   188
  text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
aad5c0982c3d tuned signature;
wenzelm
parents: 67428
diff changeset
   189
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   190
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   191
(* theory presentation *)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   192
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   193
fun isabelle_body name =
74881
1e84ae3e886e tuned signature;
wenzelm
parents: 74826
diff changeset
   194
  XML.enclose
67263
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   195
   ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
449a989f42cd discontinued 'display_drafts' command;
wenzelm
parents: 67197
diff changeset
   196
   "%\n\\end{isabellebody}%\n";
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   197
9038
63d20536971f session.tex: nsert blank lines in order to guarantee new paragraphs
wenzelm
parents: 8965
diff changeset
   198
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   199
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   200
73754
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
   201
(* index entries *)
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
   202
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
   203
type index_item = {text: text, like: string};
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
   204
type index_entry = {items: index_item list, def: bool};
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
   205
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
   206
fun index_item (item: index_item) =
74786
543f932f64b8 more symbolic latex output;
wenzelm
parents: 74784
diff changeset
   207
  XML.wrap_elem ((Markup.latex_index_item, #text item), XML.string (#like item));
73754
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
   208
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
   209
fun index_entry (entry: index_entry) =
74786
543f932f64b8 more symbolic latex output;
wenzelm
parents: 74784
diff changeset
   210
  [XML.Elem (Markup.latex_index_entry (if #def entry then "isaindexdef" else "isaindexref"),
543f932f64b8 more symbolic latex output;
wenzelm
parents: 74784
diff changeset
   211
    map index_item (#items entry))];
73754
cd7eb3cdab4c support for index entries;
wenzelm
parents: 72315
diff changeset
   212
73763
eccc4a13216d clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents: 73754
diff changeset
   213
fun index_binding NONE = I
eccc4a13216d clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents: 73754
diff changeset
   214
  | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));
eccc4a13216d clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents: 73754
diff changeset
   215
eccc4a13216d clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents: 73754
diff changeset
   216
fun index_variants setup binding =
eccc4a13216d clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents: 73754
diff changeset
   217
  fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
eccc4a13216d clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents: 73754
diff changeset
   218
eccc4a13216d clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
wenzelm
parents: 73754
diff changeset
   219
8460
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   220
(* print mode *)
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   221
8965
d46b36785c70 proper token_translation for latex mode;
wenzelm
parents: 8896
diff changeset
   222
val latexN = "latex";
d46b36785c70 proper token_translation for latex mode;
wenzelm
parents: 8896
diff changeset
   223
8460
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   224
fun latex_output str =
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   225
  let val syms = Symbol.explode str
64526
01920e390645 embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
wenzelm
parents: 63936
diff changeset
   226
  in (output_symbols syms, length_symbols syms) end;
19265
cae36e16f3c0 Output.add_mode: keyword component;
wenzelm
parents: 17218
diff changeset
   227
69346
3c29edccf739 expose latex mode operations, to facilitate adhoc changes to it;
wenzelm
parents: 67462
diff changeset
   228
fun latex_markup (s, _: Properties.T) =
59123
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59081
diff changeset
   229
  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
   230
  then ("\\isacommand{", "}")
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59081
diff changeset
   231
  else if s = Markup.keyword2N
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59081
diff changeset
   232
  then ("\\isakeyword{", "}")
29325
a205acc94356 Markup.no_output;
wenzelm
parents: 28375
diff changeset
   233
  else Markup.no_output;
10955
36741b4fe109 setuo indent: \isaindent;
wenzelm
parents: 10393
diff changeset
   234
23621
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   235
fun latex_indent "" _ = ""
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   236
  | latex_indent s _ = enclose "\\isaindent{" "}" s;
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   237
67428
dd8e40f46962 clarified signature;
wenzelm
parents: 67358
diff changeset
   238
val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
23703
1b6a2c119151 Markup.add_mode;
wenzelm
parents: 23621
diff changeset
   239
val _ = Markup.add_mode latexN latex_markup;
1b6a2c119151 Markup.add_mode;
wenzelm
parents: 23621
diff changeset
   240
val _ = Pretty.add_mode latexN latex_indent;
8460
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   241
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   242
end;