src/Pure/Thy/latex.ML
changeset 7756 f9f8660de23f
parent 7752 7ee322caf59c
child 7789 57d20133224e
     1.1 --- a/src/Pure/Thy/latex.ML	Wed Oct 06 18:12:05 1999 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Wed Oct 06 18:12:35 1999 +0200
     1.3 @@ -7,7 +7,8 @@
     1.4  
     1.5  signature LATEX =
     1.6  sig
     1.7 -  val token_source: (OuterLex.token * string option) list -> string
     1.8 +  datatype token = Basic of OuterLex.token | Markup of string * string
     1.9 +  val token_source: token list -> string
    1.10    val theory_entry: string -> string
    1.11  end;
    1.12  
    1.13 @@ -30,40 +31,54 @@
    1.14    "~" => "{\\textasciitilde}" |
    1.15    "^" => "{\\textasciicircum}" |
    1.16    "\"" => "{\"}" |
    1.17 -(*  "\\" => "{\\textbackslash}" |  FIXME *)
    1.18    "\\" => "\\verb,\\," |
    1.19 -  "|" => "{|}" |
    1.20 -  "<" => "{<}" |
    1.21 -  ">" => "{>}" |
    1.22    c => c;
    1.23  
    1.24 +val output_chr' = fn
    1.25 +  "\\" => "{\\textbackslash}" |
    1.26 +  "|" => "{\\textbar}" |
    1.27 +  "<" => "{\\textless}" |
    1.28 +  ">" => "{\\textgreater}" |
    1.29 +  c => output_chr c;
    1.30 +
    1.31  
    1.32  (* FIXME replace \<forall> etc. *)
    1.33  val output_sym = implode o map output_chr o explode;
    1.34 -val output_symbols = map output_sym;
    1.35 +val output_sym' = implode o map output_chr' o explode;
    1.36  
    1.37  
    1.38  (* token output *)
    1.39  
    1.40  structure T = OuterLex;
    1.41  
    1.42 -fun output_tok (tok, Some s) = "\\isamarkup" ^ T.val_of tok ^ "{" ^ s ^ "}"
    1.43 -  | output_tok (tok, None) =
    1.44 +datatype token = Basic of T.token | Markup of string * string;
    1.45 +
    1.46 +
    1.47 +val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    1.48 +
    1.49 +fun strip_blanks s =
    1.50 +  implode (#1 (Library.take_suffix Symbol.is_blank
    1.51 +    (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
    1.52 +
    1.53 +fun output_tok (Basic tok) =
    1.54        let val s = T.val_of tok in
    1.55 -        if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym s ^ "}"
    1.56 -        else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym s ^ "}"
    1.57 +        if invisible_token tok then ""
    1.58 +        else if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym' s ^ "}"
    1.59 +        else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym' s ^ "}"
    1.60          else if T.is_kind T.String tok then output_sym (quote s)
    1.61          else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
    1.62          else output_sym s
    1.63 -      end;
    1.64 +      end
    1.65 +  | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n";
    1.66  
    1.67 -val output_tokens = map output_tok;
    1.68 +
    1.69 +val output_tokens = implode o map output_tok;
    1.70  
    1.71  
    1.72  (* theory presentation *)
    1.73  
    1.74  fun token_source toks =
    1.75 -  "\\begin{isabellesimple}\n" ^ implode (output_tokens toks) ^ "\\end{isabellesimple}\n";
    1.76 +  "\\begin{isabellesimple}\n" ^ output_tokens toks ^ "\\end{isabellesimple}\n";
    1.77  
    1.78  fun theory_entry name = "\\input{" ^ name ^ ".tex}\n";
    1.79