src/Pure/Thy/latex.ML
author wenzelm
Mon Jan 10 17:08:41 2000 +0100 (2000-01-10)
changeset 8117 0a6173c9b2d0
parent 7973 0d801c6e4dc0
child 8192 45a7027136e3
permissions -rw-r--r--
isabellesimple: avoid paragraph;
     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 local
    22 
    23 val output_chr = fn
    24   " " => "~" |
    25   "\n" => "\\isanewline\n" |
    26   "$" => "\\$" |
    27   "&" => "\\&" |
    28   "%" => "\\%" |
    29   "#" => "\\#" |
    30   "_" => "\\_" |
    31   "{" => "{\\isabraceleft}" |
    32   "}" => "{\\isabraceright}" |
    33   "~" => "{\\isatilde}" |
    34   "^" => "{\\isacircum}" |
    35   "\"" => "{\"}" |
    36   "\\" => "{\\isabackslash}" |
    37   c => c;
    38 
    39 fun output_sym s =
    40   if size s = 1 then output_chr s
    41   else
    42     (case explode s of
    43       cs as "\\" :: "<" :: "^" :: _ => implode (map output_chr cs)
    44     | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
    45     | _ => sys_error "output_sym");
    46 
    47 in
    48 
    49 val output_syms = implode o map output_sym o Symbol.explode;
    50 
    51 end;
    52 
    53 
    54 (* token output *)
    55 
    56 structure T = OuterLex;
    57 
    58 datatype token = Basic of T.token | Markup of string * string | Verbatim of string;
    59 
    60 
    61 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    62 
    63 fun strip_blanks s =
    64   implode (#1 (Library.take_suffix Symbol.is_blank
    65     (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
    66 
    67 fun output_tok (Basic tok) =
    68       let val s = T.val_of tok in
    69         if invisible_token tok then ""
    70         else if T.is_kind T.Command tok then
    71           if s = "{{" then "{\\isabeginblock}"
    72           else if s = "}}" then "{\\isaendblock}"
    73           else "\\isacommand{" ^ output_syms s ^ "}"
    74         else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
    75           "\\isakeyword{" ^ output_syms s ^ "}"
    76         else if T.is_kind T.String tok then output_syms (quote s)
    77         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
    78         else output_syms s
    79       end
    80   | output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
    81   | output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n";
    82 
    83 
    84 val output_tokens = implode o map output_tok;
    85 
    86 
    87 (* theory presentation *)
    88 
    89 fun token_source toks =
    90   "\\begin{isabellesimple}%\n" ^ output_tokens toks ^ "\\end{isabellesimple}\n";
    91 
    92 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
    93 
    94 
    95 end;