src/Pure/Thy/latex.ML
author wenzelm
Wed Oct 06 00:35:05 1999 +0200 (1999-10-06)
changeset 7752 7ee322caf59c
parent 7745 131005d3a62d
child 7756 f9f8660de23f
permissions -rw-r--r--
accomodate markup commands;
wenzelm@7726
     1
(*  Title:      Pure/Thy/latex.ML
wenzelm@7726
     2
    ID:         $Id$
wenzelm@7726
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@7726
     4
wenzelm@7726
     5
Simple LaTeX presentation primitives (based on outer lexical syntax).
wenzelm@7726
     6
*)
wenzelm@7726
     7
wenzelm@7726
     8
signature LATEX =
wenzelm@7726
     9
sig
wenzelm@7752
    10
  val token_source: (OuterLex.token * string option) list -> string
wenzelm@7726
    11
  val theory_entry: string -> string
wenzelm@7726
    12
end;
wenzelm@7726
    13
wenzelm@7726
    14
structure Latex: LATEX =
wenzelm@7726
    15
struct
wenzelm@7726
    16
wenzelm@7726
    17
wenzelm@7726
    18
(* symbol output *)
wenzelm@7726
    19
wenzelm@7726
    20
val output_chr = fn
wenzelm@7726
    21
  " " => "~" |
wenzelm@7726
    22
  "\n" => "\\isanewline\n" |
wenzelm@7726
    23
  "$" => "\\$" |
wenzelm@7726
    24
  "&" => "\\&" |
wenzelm@7726
    25
  "%" => "\\%" |
wenzelm@7726
    26
  "#" => "\\#" |
wenzelm@7726
    27
  "_" => "\\_" |
wenzelm@7726
    28
  "{" => "{\\textbraceleft}" |
wenzelm@7726
    29
  "}" => "{\\textbraceright}" |
wenzelm@7726
    30
  "~" => "{\\textasciitilde}" |
wenzelm@7726
    31
  "^" => "{\\textasciicircum}" |
wenzelm@7752
    32
  "\"" => "{\"}" |
wenzelm@7752
    33
(*  "\\" => "{\\textbackslash}" |  FIXME *)
wenzelm@7752
    34
  "\\" => "\\verb,\\," |
wenzelm@7752
    35
  "|" => "{|}" |
wenzelm@7752
    36
  "<" => "{<}" |
wenzelm@7752
    37
  ">" => "{>}" |
wenzelm@7726
    38
  c => c;
wenzelm@7726
    39
wenzelm@7726
    40
wenzelm@7726
    41
(* FIXME replace \<forall> etc. *)
wenzelm@7752
    42
val output_sym = implode o map output_chr o explode;
wenzelm@7752
    43
val output_symbols = map output_sym;
wenzelm@7726
    44
wenzelm@7726
    45
wenzelm@7726
    46
(* token output *)
wenzelm@7726
    47
wenzelm@7726
    48
structure T = OuterLex;
wenzelm@7726
    49
wenzelm@7752
    50
fun output_tok (tok, Some s) = "\\isamarkup" ^ T.val_of tok ^ "{" ^ s ^ "}"
wenzelm@7752
    51
  | output_tok (tok, None) =
wenzelm@7752
    52
      let val s = T.val_of tok in
wenzelm@7752
    53
        if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym s ^ "}"
wenzelm@7752
    54
        else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym s ^ "}"
wenzelm@7752
    55
        else if T.is_kind T.String tok then output_sym (quote s)
wenzelm@7752
    56
        else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
wenzelm@7752
    57
        else output_sym s
wenzelm@7752
    58
      end;
wenzelm@7745
    59
wenzelm@7752
    60
val output_tokens = map output_tok;
wenzelm@7726
    61
wenzelm@7726
    62
wenzelm@7726
    63
(* theory presentation *)
wenzelm@7726
    64
wenzelm@7726
    65
fun token_source toks =
wenzelm@7726
    66
  "\\begin{isabellesimple}\n" ^ implode (output_tokens toks) ^ "\\end{isabellesimple}\n";
wenzelm@7726
    67
wenzelm@7726
    68
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
wenzelm@7726
    69
wenzelm@7726
    70
wenzelm@7726
    71
end;