src/Pure/Thy/latex.ML
author wenzelm
Thu Oct 07 17:20:58 1999 +0200 (1999-10-07)
changeset 7789 57d20133224e
parent 7756 f9f8660de23f
child 7800 8ee919e42174
permissions -rw-r--r--
verbatim markup tokens;
     1 (*  Title:      Pure/Thy/latex.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Simple LaTeX presentation primitives (based on outer lexical syntax).
     6 *)
     7 
     8 signature LATEX =
     9 sig
    10   datatype token = Basic of OuterLex.token | Markup of string * string | Verbatim of string
    11   val token_source: token list -> string
    12   val theory_entry: string -> string
    13 end;
    14 
    15 structure Latex: LATEX =
    16 struct
    17 
    18 
    19 (* symbol output *)
    20 
    21 val output_chr = fn
    22   " " => "~" |
    23   "\n" => "\\isanewline\n" |
    24   "$" => "\\$" |
    25   "&" => "\\&" |
    26   "%" => "\\%" |
    27   "#" => "\\#" |
    28   "_" => "\\_" |
    29   "{" => "{\\textbraceleft}" |
    30   "}" => "{\\textbraceright}" |
    31   "~" => "{\\textasciitilde}" |
    32   "^" => "{\\textasciicircum}" |
    33   "\"" => "{\"}" |
    34   "\\" => "\\verb,\\," |
    35   c => c;
    36 
    37 val output_chr' = fn
    38   "\\" => "{\\textbackslash}" |
    39   "|" => "{\\textbar}" |
    40   "<" => "{\\textless}" |
    41   ">" => "{\\textgreater}" |
    42   c => output_chr c;
    43 
    44 
    45 (* FIXME replace \<forall> etc. *)
    46 val output_sym = implode o map output_chr o explode;
    47 val output_sym' = implode o map output_chr' o explode;
    48 
    49 
    50 (* token output *)
    51 
    52 structure T = OuterLex;
    53 
    54 datatype token = Basic of T.token | Markup of string * string | Verbatim of string;
    55 
    56 
    57 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    58 
    59 fun strip_blanks s =
    60   implode (#1 (Library.take_suffix Symbol.is_blank
    61     (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
    62 
    63 fun output_tok (Basic tok) =
    64       let val s = T.val_of tok in
    65         if invisible_token tok then ""
    66         else if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym' s ^ "}"
    67         else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym' s ^ "}"
    68         else if T.is_kind T.String tok then output_sym (quote s)
    69         else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
    70         else output_sym s
    71       end
    72   | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n"
    73   | output_tok (Verbatim txt) = "\n" ^ txt ^ "\n";
    74 
    75 
    76 val output_tokens = implode o map output_tok;
    77 
    78 
    79 (* theory presentation *)
    80 
    81 fun token_source toks =
    82   "\\begin{isabellesimple}\n" ^ output_tokens toks ^ "\\end{isabellesimple}\n";
    83 
    84 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
    85 
    86 
    87 end;