src/Pure/Thy/latex.ML
author wenzelm
Mon Jun 26 00:23:17 2000 +0200 (2000-06-26)
changeset 9144 20a70ef9c320
parent 9135 3aa95ab3f02d
child 9505 09c75c801dde
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/Thy/latex.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 LaTeX presentation primitives (based on outer lexical syntax).
     7 *)
     8 
     9 signature LATEX =
    10 sig
    11   datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
    12   val output_tokens: (token * string) list -> string
    13   val isabelle_file: string -> string
    14   val old_symbol_source: string -> Symbol.symbol list -> string
    15   val theory_entry: string -> string
    16   val modes: string list
    17   val setup: (theory -> theory) list
    18 end;
    19 
    20 structure Latex: LATEX =
    21 struct
    22 
    23 
    24 (* symbol output *)
    25 
    26 local
    27 
    28 val output_chr = fn
    29   " " => "~" |
    30   "\n" => "\\isanewline\n" |
    31   "$" => "\\$" |
    32   "&" => "\\&" |
    33   "%" => "\\%" |
    34   "#" => "\\#" |
    35   "_" => "\\_" |
    36   "{" => "{\\isabraceleft}" |
    37   "}" => "{\\isabraceright}" |
    38   "~" => "{\\isatilde}" |
    39   "^" => "{\\isacircum}" |
    40   "\"" => "{\"}" |
    41   "\\" => "{\\isabackslash}" |
    42   c => c;
    43 
    44 fun output_sym s =
    45   if size s = 1 then output_chr s
    46   else
    47     (case explode s of
    48       cs as "\\" :: "<" :: "^" :: _ => implode (map output_chr cs)
    49     | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
    50     | _ => sys_error "output_sym");
    51 
    52 in
    53 
    54 val output_symbols = implode o map output_sym;
    55 val output_syms = output_symbols o Symbol.explode;
    56 
    57 end;
    58 
    59 
    60 (* token output *)
    61 
    62 structure T = OuterLex;
    63 
    64 datatype token =
    65   Basic of T.token |
    66   Markup of string |
    67   MarkupEnv of string |
    68   Verbatim;
    69 
    70 
    71 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    72 
    73 fun strip_blanks s =
    74   implode (#1 (Library.take_suffix Symbol.is_blank
    75     (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
    76 
    77 fun output_tok (Basic tok, _) =
    78       let val s = T.val_of tok in
    79         if invisible_token tok then ""
    80         else if T.is_kind T.Command tok then
    81           if s = "{" then "{\\isabeginblock}"
    82           else if s = "}" then "{\\isaendblock}"
    83           else "\\isacommand{" ^ output_syms s ^ "}"
    84         else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
    85           "\\isakeyword{" ^ output_syms s ^ "}"
    86         else if T.is_kind T.String tok then output_syms (quote s)
    87         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
    88         else output_syms s
    89       end
    90   | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
    91   | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
    92       strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
    93   | output_tok (Verbatim, txt) = "%\n" ^ strip_blanks txt ^ "\n";
    94 
    95 
    96 val output_tokens = implode o map output_tok;
    97 
    98 
    99 (* theory presentation *)
   100 
   101 val isabelle_file = enclose
   102   "\\begin{isabelle}%\n"
   103   "\\end{isabelle}%\n\
   104   \%%% Local Variables:\n\
   105   \%%% mode: latex\n\
   106   \%%% TeX-master: \"root\"\n\
   107   \%%% End:\n";
   108 
   109 fun old_symbol_source name syms =
   110   isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
   111 
   112 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
   113 
   114 
   115 (* print mode *)
   116 
   117 val latexN = "latex";
   118 val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN];
   119 
   120 fun latex_output str =
   121   let val syms = Symbol.explode str
   122   in (output_symbols syms, real (Symbol.length syms)) end;
   123 
   124 val token_translation = map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
   125 
   126 val _ = Symbol.add_mode latexN latex_output;
   127 val setup = [Theory.add_tokentrfuns token_translation];
   128 
   129 
   130 end;