src/Pure/Thy/latex.ML
author wenzelm
Mon, 29 Aug 2011 21:55:49 +0200
changeset 44574 24444588fddd
parent 43709 717e96cf9527
child 45666 d83797ef0d2d
permissions -rw-r--r--
actual auto loading of required files; eliminated File_Store in favour of Thy_Load; tuned;
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
14924
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
     9
  val output_known_symbols: (string -> bool) * (string -> bool) ->
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
    10
    Symbol.symbol list -> string
11719
49c14348a42b Exported output_symbols.
berghofe
parents: 11012
diff changeset
    11
  val output_symbols: Symbol.symbol list -> string
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 30642
diff changeset
    12
  val output_basic: Token.T -> string
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    13
  val output_markup: string -> string -> string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    14
  val output_markup_env: string -> string -> string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    15
  val output_verbatim: string -> string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    16
  val markup_true: string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    17
  val markup_false: string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    18
  val begin_delim: string -> string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    19
  val end_delim: string -> string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    20
  val begin_tag: string -> string
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
    21
  val end_tag: string -> string
9707
067c25edd1bd added tex_trailer;
wenzelm
parents: 9668
diff changeset
    22
  val tex_trailer: string
9916
4a703366494b define \isabellecontext;
wenzelm
parents: 9749
diff changeset
    23
  val isabelle_file: string -> string -> string
14924
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
    24
  val symbol_source: (string -> bool) * (string -> bool) ->
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
    25
    string -> Symbol.symbol list -> string
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    26
  val theory_entry: string -> string
9135
3aa95ab3f02d adapted to improved presentation;
wenzelm
parents: 9038
diff changeset
    27
  val modes: string list
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    28
end;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    29
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    30
structure Latex: LATEX =
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    31
struct
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    32
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    33
(* literal text *)
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    34
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    35
local
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    36
  val hex = Int.fmt StringCvt.HEX;
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    37
  fun hex_byte c = hex (ord c div 16) ^ hex (ord c mod 16);
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    38
in
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    39
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    40
fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}";
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    41
fun enclose_literal txt arg = enclose "{" "}" (literal txt ^ arg);
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    42
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    43
end;
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    44
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    45
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    46
(* symbol output *)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    47
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
    48
local
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
    49
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    50
val char_table =
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    51
  Symtab.make
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    52
   [("!", "{\\isacharbang}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    53
    ("\"", "{\\isachardoublequote}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    54
    ("#", "{\\isacharhash}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    55
    ("$", "{\\isachardollar}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    56
    ("%", "{\\isacharpercent}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    57
    ("&", "{\\isacharampersand}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    58
    ("'", "{\\isacharprime}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    59
    ("(", "{\\isacharparenleft}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    60
    (")", "{\\isacharparenright}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    61
    ("*", "{\\isacharasterisk}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    62
    ("+", "{\\isacharplus}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    63
    (",", "{\\isacharcomma}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    64
    ("-", "{\\isacharminus}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    65
    (".", "{\\isachardot}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    66
    ("/", "{\\isacharslash}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    67
    (":", "{\\isacharcolon}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    68
    (";", "{\\isacharsemicolon}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    69
    ("<", "{\\isacharless}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    70
    ("=", "{\\isacharequal}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    71
    (">", "{\\isachargreater}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    72
    ("?", "{\\isacharquery}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    73
    ("@", "{\\isacharat}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    74
    ("[", "{\\isacharbrackleft}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    75
    ("\\", "{\\isacharbackslash}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    76
    ("]", "{\\isacharbrackright}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    77
    ("^", "{\\isacharcircum}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    78
    ("_", "{\\isacharunderscore}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    79
    ("`", "{\\isacharbackquote}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    80
    ("{", "{\\isacharbraceleft}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    81
    ("|", "{\\isacharbar}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    82
    ("}", "{\\isacharbraceright}"),
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    83
    ("~", "{\\isachartilde}")];
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    84
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    85
fun output_chr " " = "\\ "
43709
717e96cf9527 discontinued special treatment of hard tabulators;
wenzelm
parents: 43485
diff changeset
    86
  | 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
    87
  | 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
    88
  | output_chr c =
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    89
      (case Symtab.lookup char_table c of
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    90
        SOME s => enclose_literal c s
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    91
      | 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
    92
14924
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
    93
val output_chrs = translate_string output_chr;
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
    94
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
    95
fun output_known_sym (known_sym, known_ctrl) sym =
14874
23c73484312f Symbol.decode;
wenzelm
parents: 14840
diff changeset
    96
  (case Symbol.decode sym of
23c73484312f Symbol.decode;
wenzelm
parents: 14840
diff changeset
    97
    Symbol.Char s => output_chr s
37533
d775bd70f571 explicit treatment of UTF8 character sequences as Isabelle symbols;
wenzelm
parents: 36959
diff changeset
    98
  | Symbol.UTF8 s => s
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
    99
  | Symbol.Sym s =>
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   100
      if known_sym s then enclose_literal sym (enclose "{\\isasym" "}" s)
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   101
      else output_chrs sym
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   102
  | Symbol.Ctrl s =>
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   103
      if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   104
      else output_chrs sym
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 40402
diff changeset
   105
  | Symbol.Raw s => s
43485
33a24212a72d more tolerant Symbol.decode;
wenzelm
parents: 42290
diff changeset
   106
  | Symbol.Malformed s => error (Symbol.malformed_msg s)
33a24212a72d more tolerant Symbol.decode;
wenzelm
parents: 42290
diff changeset
   107
  | Symbol.EOF => error "Bad EOF symbol");
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   108
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   109
in
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   110
14924
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
   111
val output_known_symbols = implode oo (map o output_known_sym);
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
   112
val output_symbols = output_known_symbols (K true, K true);
8192
45a7027136e3 added old_symbol_source;
wenzelm
parents: 8117
diff changeset
   113
val output_syms = output_symbols o Symbol.explode;
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   114
27874
f0364f1c0ecf antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents: 27809
diff changeset
   115
val output_syms_antiq =
30589
cbe27c4ef417 Antiquote.Text: keep full position information;
wenzelm
parents: 30573
diff changeset
   116
  (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
27874
f0364f1c0ecf antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents: 27809
diff changeset
   117
    | Antiquote.Antiq (ss, _) =>
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   118
        enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   119
          (output_symbols (map Symbol_Pos.symbol ss))
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   120
    | Antiquote.Open _ => enclose_literal "\\<lbrace>" "{\\isaantiqopen}"
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   121
    | Antiquote.Close _ => enclose_literal "\\<rbrace>" "{\\isaantiqclose}");
22648
8c6b4f7548e3 output_basic: added isaantiq markup (only inside verbatim tokens);
wenzelm
parents: 19265
diff changeset
   122
7900
e62973fccc97 output \isasymbols;
wenzelm
parents: 7852
diff changeset
   123
end;
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   124
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   125
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   126
(* token output *)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   127
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 30642
diff changeset
   128
val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment;
7756
f9f8660de23f improved presentation;
wenzelm
parents: 7752
diff changeset
   129
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   130
fun output_basic tok =
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 30642
diff changeset
   131
  let val s = Token.content_of tok in
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   132
    if invisible_token tok then ""
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 30642
diff changeset
   133
    else if Token.is_kind Token.Command tok then
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   134
      "\\isacommand{" ^ output_syms s ^ "}"
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40523
diff changeset
   135
    else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   136
      "\\isakeyword{" ^ output_syms s ^ "}"
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 30642
diff changeset
   137
    else if Token.is_kind Token.String tok then
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   138
      output_syms s |> enclose
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   139
        (enclose_literal "\"" "{\\isachardoublequoteopen}")
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   140
        (enclose_literal "\"" "{\\isachardoublequoteclose}")
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 30642
diff changeset
   141
    else if Token.is_kind Token.AltString tok then
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   142
      output_syms s |> enclose
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   143
        (enclose_literal "`" "{\\isacharbackquoteopen}")
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   144
        (enclose_literal "`" "{\\isacharbackquoteclose}")
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 30642
diff changeset
   145
    else if Token.is_kind Token.Verbatim tok then
27874
f0364f1c0ecf antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents: 27809
diff changeset
   146
      let
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 30642
diff changeset
   147
        val (txt, pos) = Token.source_position_of tok;
30642
0c9f9c49d5df simplified Antiquote.read (again);
wenzelm
parents: 30613
diff changeset
   148
        val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
27874
f0364f1c0ecf antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
wenzelm
parents: 27809
diff changeset
   149
        val out = implode (map output_syms_antiq ants);
40402
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   150
      in
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   151
        out |> enclose
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   152
          (enclose_literal "{*" "{\\isacharverbatimopen}")
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   153
          (enclose_literal "*}" "{\\isacharverbatimclose}")
b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents: 39666
diff changeset
   154
      end
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   155
    else output_syms s
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   156
  end;
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   157
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   158
fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n";
7745
131005d3a62d strip_blanks;
wenzelm
parents: 7726
diff changeset
   159
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   160
fun output_markup_env cmd txt =
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   161
  "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   162
  Symbol.strip_blanks txt ^
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   163
  "%\n\\end{isamarkup" ^ cmd ^ "}%\n";
7756
f9f8660de23f improved presentation;
wenzelm
parents: 7752
diff changeset
   164
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   165
fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   166
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   167
val markup_true = "\\isamarkuptrue%\n";
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   168
val markup_false = "\\isamarkupfalse%\n";
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   169
17081
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   170
val begin_delim = enclose "%\n\\isadelim" "\n";
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   171
val end_delim = enclose "%\n\\endisadelim" "\n";
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   172
val begin_tag = enclose "%\n\\isatag" "\n";
e19963723262 eliminated datatype token;
wenzelm
parents: 15801
diff changeset
   173
fun end_tag tg = enclose "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
11860
36ba0d4a836c flag_markup;
wenzelm
parents: 11719
diff changeset
   174
36ba0d4a836c flag_markup;
wenzelm
parents: 11719
diff changeset
   175
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   176
(* theory presentation *)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   177
9707
067c25edd1bd added tex_trailer;
wenzelm
parents: 9668
diff changeset
   178
val tex_trailer =
067c25edd1bd added tex_trailer;
wenzelm
parents: 9668
diff changeset
   179
  "%%% Local Variables:\n\
9135
3aa95ab3f02d adapted to improved presentation;
wenzelm
parents: 9038
diff changeset
   180
  \%%% mode: latex\n\
3aa95ab3f02d adapted to improved presentation;
wenzelm
parents: 9038
diff changeset
   181
  \%%% TeX-master: \"root\"\n\
9144
wenzelm
parents: 9135
diff changeset
   182
  \%%% End:\n";
8192
45a7027136e3 added old_symbol_source;
wenzelm
parents: 8117
diff changeset
   183
9916
4a703366494b define \isabellecontext;
wenzelm
parents: 9749
diff changeset
   184
fun isabelle_file name txt =
4a703366494b define \isabellecontext;
wenzelm
parents: 9749
diff changeset
   185
  "%\n\\begin{isabellebody}%\n\
10247
33e542b4934c \isabellecontext: output_syms;
wenzelm
parents: 10184
diff changeset
   186
  \\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
9916
4a703366494b define \isabellecontext;
wenzelm
parents: 9749
diff changeset
   187
  "\\end{isabellebody}%\n" ^ tex_trailer;
9707
067c25edd1bd added tex_trailer;
wenzelm
parents: 9668
diff changeset
   188
14924
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
   189
fun symbol_source known name syms = isabelle_file name
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
   190
  ("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
2be4cbe27a27 added output_known_symbols; tuned;
wenzelm
parents: 14879
diff changeset
   191
    output_known_symbols known syms);
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   192
9038
63d20536971f session.tex: nsert blank lines in order to guarantee new paragraphs
wenzelm
parents: 8965
diff changeset
   193
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   194
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   195
8460
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   196
(* print mode *)
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   197
8965
d46b36785c70 proper token_translation for latex mode;
wenzelm
parents: 8896
diff changeset
   198
val latexN = "latex";
17218
64242b791c19 removed obsolete 'symbols' mode;
wenzelm
parents: 17186
diff changeset
   199
val modes = [latexN, Symbol.xsymbolsN];
8965
d46b36785c70 proper token_translation for latex mode;
wenzelm
parents: 8896
diff changeset
   200
8460
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   201
fun latex_output str =
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   202
  let val syms = Symbol.explode str
23621
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   203
  in (output_symbols syms, Symbol.length syms) end;
19265
cae36e16f3c0 Output.add_mode: keyword component;
wenzelm
parents: 17218
diff changeset
   204
23621
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   205
fun latex_markup (s, _) =
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   206
  if s = Markup.keywordN then ("\\isakeyword{", "}")
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   207
  else if s = Markup.commandN then ("\\isacommand{", "}")
29325
a205acc94356 Markup.no_output;
wenzelm
parents: 28375
diff changeset
   208
  else Markup.no_output;
10955
36741b4fe109 setuo indent: \isaindent;
wenzelm
parents: 10393
diff changeset
   209
23621
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   210
fun latex_indent "" _ = ""
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   211
  | latex_indent s _ = enclose "\\isaindent{" "}" s;
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   212
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22648
diff changeset
   213
val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
23703
1b6a2c119151 Markup.add_mode;
wenzelm
parents: 23621
diff changeset
   214
val _ = Markup.add_mode latexN latex_markup;
1b6a2c119151 Markup.add_mode;
wenzelm
parents: 23621
diff changeset
   215
val _ = Pretty.add_mode latexN latex_indent;
8460
274426d1adbc tuned comments;
wenzelm
parents: 8192
diff changeset
   216
7726
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
   217
end;