src/Pure/Thy/latex.ML
changeset 7900 e62973fccc97
parent 7852 d28dff7ac48d
child 7973 0d801c6e4dc0
     1.1 --- a/src/Pure/Thy/latex.ML	Thu Oct 21 18:42:38 1999 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Thu Oct 21 18:43:06 1999 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4  
     1.5  (* symbol output *)
     1.6  
     1.7 +local
     1.8 +
     1.9  val output_chr = fn
    1.10    " " => "~" |
    1.11    "\n" => "\\isanewline\n" |
    1.12 @@ -34,8 +36,19 @@
    1.13    "\\" => "{\\isabackslash}" |
    1.14    c => c;
    1.15  
    1.16 -(* FIXME replace \<forall> etc. *)
    1.17 -val output_sym = implode o map output_chr o explode;
    1.18 +fun output_sym s =
    1.19 +  if size s = 1 then output_chr s
    1.20 +  else
    1.21 +    (case explode s of
    1.22 +      cs as "\\" :: "<" :: "^" :: _ => implode (map output_chr cs)
    1.23 +    | "\\" :: "<" :: cs => "{\\isasymbol" ^ implode (#1 (Library.split_last cs)) ^ "}"
    1.24 +    | _ => sys_error "output_sym");
    1.25 +
    1.26 +in
    1.27 +
    1.28 +val output_syms = implode o map output_sym o Symbol.explode;
    1.29 +
    1.30 +end;
    1.31  
    1.32  
    1.33  (* token output *)
    1.34 @@ -57,12 +70,12 @@
    1.35          else if T.is_kind T.Command tok then
    1.36            if s = "{{" then "{\\isabeginblock}"
    1.37            else if s = "}}" then "{\\isaendblock}"
    1.38 -          else "\\isacommand{" ^ output_sym s ^ "}"
    1.39 +          else "\\isacommand{" ^ output_syms s ^ "}"
    1.40          else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
    1.41 -          "\\isakeyword{" ^ output_sym s ^ "}"
    1.42 -        else if T.is_kind T.String tok then output_sym (quote s)
    1.43 -        else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
    1.44 -        else output_sym s
    1.45 +          "\\isakeyword{" ^ output_syms s ^ "}"
    1.46 +        else if T.is_kind T.String tok then output_syms (quote s)
    1.47 +        else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
    1.48 +        else output_syms s
    1.49        end
    1.50    | output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
    1.51    | output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n";