src/Pure/Thy/latex.ML
changeset 7726 2c7fc0ba1e12
child 7745 131005d3a62d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Oct 05 15:33:35 1999 +0200
     1.3 @@ -0,0 +1,88 @@
     1.4 +(*  Title:      Pure/Thy/latex.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Simple LaTeX presentation primitives (based on outer lexical syntax).
     1.9 +*)
    1.10 +
    1.11 +signature LATEX =
    1.12 +sig
    1.13 +  val token_source: OuterLex.token list -> string
    1.14 +  val theory_entry: string -> string
    1.15 +end;
    1.16 +
    1.17 +structure Latex: LATEX =
    1.18 +struct
    1.19 +
    1.20 +
    1.21 +(* symbol output *)
    1.22 +
    1.23 +local
    1.24 +
    1.25 +val output_chr = fn
    1.26 +  " " => "~" |
    1.27 +  "\n" => "\\isanewline\n" |
    1.28 +  "$" => "\\$" |
    1.29 +  "&" => "\\&" |
    1.30 +  "%" => "\\%" |
    1.31 +  "#" => "\\#" |
    1.32 +  "_" => "\\_" |
    1.33 +  "{" => "{\\textbraceleft}" |
    1.34 +  "}" => "{\\textbraceright}" |
    1.35 +  "~" => "{\\textasciitilde}" |
    1.36 +  "^" => "{\\textasciicircum}" |
    1.37 +(*  "\"" => "{\\textquotedblleft}" |    (* FIXME !? *)*)
    1.38 +  "\\" => "{\\textbackslash}" |
    1.39 +(*  "|" => "{\\textbar}" |
    1.40 +  "<" => "{\\textless}" |
    1.41 +  ">" => "{\\textgreater}" |  *)
    1.42 +  c => c;
    1.43 +
    1.44 +in
    1.45 +
    1.46 +(* FIXME replace \<forall> etc. *)
    1.47 +val output_symbol = implode o map output_chr o explode;
    1.48 +val output_symbols = map output_symbol;
    1.49 +
    1.50 +end;
    1.51 +
    1.52 +
    1.53 +(* token output *)
    1.54 +
    1.55 +local
    1.56 +
    1.57 +structure T = OuterLex;
    1.58 +
    1.59 +fun output_tok tok =
    1.60 +  let
    1.61 +    val out = output_symbol;
    1.62 +    val s = T.val_of tok;
    1.63 +  in
    1.64 +    if T.is_kind T.Command tok then "\\isacommand{" ^ out s ^ "}"
    1.65 +    else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ out s ^ "}"
    1.66 +    else if T.is_kind T.String tok then out (quote s)
    1.67 +    else if T.is_kind T.Verbatim tok then "\\isatext{" ^ s ^ "}"
    1.68 +    else out s
    1.69 +  end;
    1.70 +
    1.71 +(*adhoc tuning of tokens*)
    1.72 +fun invisible_token tok =
    1.73 +  T.is_kind T.Command tok andalso T.val_of tok mem_string ["text", "txt"] orelse
    1.74 +  T.keyword_with (equal ";") tok orelse T.is_kind T.Comment tok;
    1.75 +
    1.76 +in
    1.77 +
    1.78 +val output_tokens = map output_tok o filter_out invisible_token;
    1.79 +
    1.80 +end;
    1.81 +
    1.82 +
    1.83 +(* theory presentation *)
    1.84 +
    1.85 +fun token_source toks =
    1.86 +  "\\begin{isabellesimple}\n" ^ implode (output_tokens toks) ^ "\\end{isabellesimple}\n";
    1.87 +
    1.88 +fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
    1.89 +
    1.90 +
    1.91 +end;