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