handle raw symbols; Output.add_mode;
authorwenzelm
Sat May 29 15:08:21 2004 +0200 (2004-05-29)
changeset 14840dc23ff2629e2
parent 14839 c994f1c57fc7
child 14841 37fc364a60c3
handle raw symbols; Output.add_mode;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Sat May 29 15:08:08 2004 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Sat May 29 15:08:21 2004 +0200
     1.3 @@ -66,13 +66,13 @@
     1.4    c => if Symbol.is_digit c then enclose "{\\isadigit{" "}}" c else c;
     1.5  
     1.6  fun output_sym s =
     1.7 -  if size s = 1 then output_chr s
     1.8 -  else
     1.9 -    (case explode s of
    1.10 -      "\\" :: "<" :: "^" :: "r"::"a"::"w"::":"::cs => implode (#1 (Library.split_last cs)) 
    1.11 -    | "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
    1.12 -    | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
    1.13 -    | _ => sys_error "output_sym");
    1.14 +  if Symbol.is_char s then output_chr s
    1.15 +  else if Symbol.is_raw s then Symbol.decode_raw s
    1.16 +  else if String.isPrefix "\\<^" s then
    1.17 +    enclose "\\isactrl" " " (String.substring (s, 3, size s - 4))
    1.18 +  else if String.isPrefix "\\<" s then
    1.19 +    enclose "{\\isasym" "}" (String.substring (s, 2, size s - 3))
    1.20 +  else sys_error "output_sym";
    1.21  
    1.22  in
    1.23  
    1.24 @@ -154,7 +154,7 @@
    1.25  val token_translation =
    1.26    map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
    1.27  
    1.28 -val _ = Symbol.add_mode latexN (latex_output, latex_indent o #1);
    1.29 +val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.default_raw);
    1.30  val setup = [Theory.add_tokentrfuns token_translation];
    1.31  
    1.32