src/Pure/Thy/latex.ML

strip_blanks;

(*  Title:      Pure/Thy/latex.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Simple LaTeX presentation primitives (based on outer lexical syntax).
*)

signature LATEX =
sig
  val token_source: OuterLex.token list -> string
  val theory_entry: string -> string
end;

structure Latex: LATEX =
struct


(* symbol output *)

local

val output_chr = fn
  " " => "~" |
  "\n" => "\\isanewline\n" |
  "$" => "\\$" |
  "&" => "\\&" |
  "%" => "\\%" |
  "#" => "\\#" |
  "_" => "\\_" |
  "{" => "{\\textbraceleft}" |
  "}" => "{\\textbraceright}" |
  "~" => "{\\textasciitilde}" |
  "^" => "{\\textasciicircum}" |
(*  "\"" => "{\\textquotedblleft}" |    (* FIXME !? *)*)
  "\\" => "{\\textbackslash}" |
(*  "|" => "{\\textbar}" |
  "<" => "{\\textless}" |
  ">" => "{\\textgreater}" |  *)
  c => c;

in

(* FIXME replace \<forall> etc. *)
val output_symbol = implode o map output_chr o explode;
val output_symbols = map output_symbol;

end;


(* token output *)

local

structure T = OuterLex;

fun strip_blanks s =
  implode (#1 (Library.take_suffix Symbol.is_blank
    (#2 (Library.take_prefix Symbol.is_blank (explode s)))));

fun output_tok tok =
  let
    val out = output_symbol;
    val s = T.val_of tok;
  in
    if T.is_kind T.Command tok then "\\isacommand{" ^ out s ^ "}"
    else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ out s ^ "}"
    else if T.is_kind T.String tok then out (quote s)
    else if T.is_kind T.Verbatim tok then "\\isatext{" ^ strip_blanks s ^ "}"
    else out s
  end;

(*adhoc tuning of tokens*)
fun invisible_token tok =
  T.is_kind T.Command tok andalso T.val_of tok mem_string ["text", "txt"] orelse
  T.keyword_with (equal ";") tok orelse T.is_kind T.Comment tok;

in

val output_tokens = map output_tok o filter_out invisible_token;

end;


(* theory presentation *)

fun token_source toks =
  "\\begin{isabellesimple}\n" ^ implode (output_tokens toks) ^ "\\end{isabellesimple}\n";

fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";


end;