src/Pure/Thy/latex.ML
author wenzelm
Tue, 05 Oct 1999 15:33:35 +0200
changeset 7726 2c7fc0ba1e12
child 7745 131005d3a62d
permissions -rw-r--r--
Simple LaTeX presentation primitives (based on outer lexical syntax).
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
    ID:         $Id$
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     4
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     5
Simple LaTeX presentation primitives (based on outer lexical syntax).
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
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     8
signature LATEX =
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
     9
sig
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    10
  val token_source: OuterLex.token list -> string
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    11
  val theory_entry: string -> string
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    12
end;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    13
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    14
structure Latex: LATEX =
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    15
struct
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    16
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    17
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    18
(* symbol output *)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    19
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    20
local
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    21
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    22
val output_chr = fn
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    23
  " " => "~" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    24
  "\n" => "\\isanewline\n" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    25
  "$" => "\\$" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    26
  "&" => "\\&" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    27
  "%" => "\\%" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    28
  "#" => "\\#" |
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
  "{" => "{\\textbraceleft}" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    31
  "}" => "{\\textbraceright}" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    32
  "~" => "{\\textasciitilde}" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    33
  "^" => "{\\textasciicircum}" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    34
(*  "\"" => "{\\textquotedblleft}" |    (* FIXME !? *)*)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    35
  "\\" => "{\\textbackslash}" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    36
(*  "|" => "{\\textbar}" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    37
  "<" => "{\\textless}" |
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    38
  ">" => "{\\textgreater}" |  *)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    39
  c => c;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    40
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    41
in
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    42
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    43
(* FIXME replace \<forall> etc. *)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    44
val output_symbol = implode o map output_chr o explode;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    45
val output_symbols = map output_symbol;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    46
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    47
end;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    48
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    49
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    50
(* token output *)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    51
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    52
local
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    53
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    54
structure T = OuterLex;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    55
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    56
fun output_tok tok =
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    57
  let
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    58
    val out = output_symbol;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    59
    val s = T.val_of tok;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    60
  in
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    61
    if T.is_kind T.Command tok then "\\isacommand{" ^ out s ^ "}"
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    62
    else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ out s ^ "}"
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    63
    else if T.is_kind T.String tok then out (quote s)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    64
    else if T.is_kind T.Verbatim tok then "\\isatext{" ^ s ^ "}"
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    65
    else out s
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    66
  end;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    67
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    68
(*adhoc tuning of tokens*)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    69
fun invisible_token tok =
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    70
  T.is_kind T.Command tok andalso T.val_of tok mem_string ["text", "txt"] orelse
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    71
  T.keyword_with (equal ";") tok orelse T.is_kind T.Comment tok;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    72
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    73
in
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    74
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    75
val output_tokens = map output_tok o filter_out invisible_token;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    76
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    77
end;
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    78
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    79
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    80
(* theory presentation *)
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    81
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    82
fun token_source toks =
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    83
  "\\begin{isabellesimple}\n" ^ implode (output_tokens toks) ^ "\\end{isabellesimple}\n";
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    84
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    85
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    86
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    87
2c7fc0ba1e12 Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm
parents:
diff changeset
    88
end;