src/Pure/Thy/latex.ML
author wenzelm
Fri Mar 17 16:30:45 2000 +0100 (2000-03-17)
changeset 8499 8958ece3bbdf
parent 8460 274426d1adbc
child 8660 e5048a26e1d8
permissions -rw-r--r--
old_symbol_source: include header;
     1 (*  Title:      Pure/Thy/latex.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 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 old_symbol_source: string -> Symbol.symbol list -> string
    12   val token_source: token list -> string
    13   val theory_entry: string -> string
    14 end;
    15 
    16 structure Latex: LATEX =
    17 struct
    18 
    19 
    20 (* symbol output *)
    21 
    22 local
    23 
    24 val output_chr = fn
    25   " " => "~" |
    26   "\n" => "\\isanewline\n" |
    27   "$" => "\\$" |
    28   "&" => "\\&" |
    29   "%" => "\\%" |
    30   "#" => "\\#" |
    31   "_" => "\\_" |
    32   "{" => "{\\isabraceleft}" |
    33   "}" => "{\\isabraceright}" |
    34   "~" => "{\\isatilde}" |
    35   "^" => "{\\isacircum}" |
    36   "\"" => "{\"}" |
    37   "\\" => "{\\isabackslash}" |
    38   c => c;
    39 
    40 fun output_sym s =
    41   if size s = 1 then output_chr s
    42   else
    43     (case explode s of
    44       cs as "\\" :: "<" :: "^" :: _ => implode (map output_chr cs)
    45     | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
    46     | _ => sys_error "output_sym");
    47 
    48 in
    49 
    50 val output_symbols = implode o map output_sym;
    51 val output_syms = output_symbols o Symbol.explode;
    52 
    53 end;
    54 
    55 
    56 (* token output *)
    57 
    58 structure T = OuterLex;
    59 
    60 datatype token = Basic of T.token | Markup of string * string | Verbatim of string;
    61 
    62 
    63 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    64 
    65 fun strip_blanks s =
    66   implode (#1 (Library.take_suffix Symbol.is_blank
    67     (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
    68 
    69 fun output_tok (Basic tok) =
    70       let val s = T.val_of tok in
    71         if invisible_token tok then ""
    72         else if T.is_kind T.Command tok then
    73           if s = "{{" then "{\\isabeginblock}"
    74           else if s = "}}" then "{\\isaendblock}"
    75           else "\\isacommand{" ^ output_syms s ^ "}"
    76         else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
    77           "\\isakeyword{" ^ output_syms s ^ "}"
    78         else if T.is_kind T.String tok then output_syms (quote s)
    79         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
    80         else output_syms s
    81       end
    82   | output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
    83   | output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n";
    84 
    85 
    86 val output_tokens = implode o map output_tok;
    87 
    88 
    89 (* theory presentation *)
    90 
    91 val isabelle_env = enclose "\\begin{isabelle}%\n" "\\end{isabelle}%\n";
    92 
    93 fun old_symbol_source name syms =
    94   isabelle_env ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
    95 
    96 val token_source = isabelle_env o output_tokens;
    97 
    98 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
    99 
   100 
   101 (* print mode *)
   102 
   103 fun latex_output str =
   104   let val syms = Symbol.explode str
   105   in (output_symbols syms, real (Symbol.length syms)) end;
   106 
   107 val _ = Symbol.add_mode "latex" latex_output;
   108 
   109 
   110 end;