--- a/src/Pure/Thy/latex.ML Wed Oct 06 18:12:05 1999 +0200
+++ b/src/Pure/Thy/latex.ML Wed Oct 06 18:12:35 1999 +0200
@@ -7,7 +7,8 @@
signature LATEX =
sig
- val token_source: (OuterLex.token * string option) list -> string
+ datatype token = Basic of OuterLex.token | Markup of string * string
+ val token_source: token list -> string
val theory_entry: string -> string
end;
@@ -30,40 +31,54 @@
"~" => "{\\textasciitilde}" |
"^" => "{\\textasciicircum}" |
"\"" => "{\"}" |
-(* "\\" => "{\\textbackslash}" | FIXME *)
"\\" => "\\verb,\\," |
- "|" => "{|}" |
- "<" => "{<}" |
- ">" => "{>}" |
c => c;
+val output_chr' = fn
+ "\\" => "{\\textbackslash}" |
+ "|" => "{\\textbar}" |
+ "<" => "{\\textless}" |
+ ">" => "{\\textgreater}" |
+ c => output_chr c;
+
(* FIXME replace \<forall> etc. *)
val output_sym = implode o map output_chr o explode;
-val output_symbols = map output_sym;
+val output_sym' = implode o map output_chr' o explode;
(* token output *)
structure T = OuterLex;
-fun output_tok (tok, Some s) = "\\isamarkup" ^ T.val_of tok ^ "{" ^ s ^ "}"
- | output_tok (tok, None) =
+datatype token = Basic of T.token | Markup of string * string;
+
+
+val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
+
+fun strip_blanks s =
+ implode (#1 (Library.take_suffix Symbol.is_blank
+ (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
+
+fun output_tok (Basic tok) =
let val s = T.val_of tok in
- if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym s ^ "}"
- else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym s ^ "}"
+ if invisible_token tok then ""
+ else if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym' s ^ "}"
+ else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym' s ^ "}"
else if T.is_kind T.String tok then output_sym (quote s)
else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
else output_sym s
- end;
+ end
+ | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n";
-val output_tokens = map output_tok;
+
+val output_tokens = implode o map output_tok;
(* theory presentation *)
fun token_source toks =
- "\\begin{isabellesimple}\n" ^ implode (output_tokens toks) ^ "\\end{isabellesimple}\n";
+ "\\begin{isabellesimple}\n" ^ output_tokens toks ^ "\\end{isabellesimple}\n";
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";