# HG changeset patch
# User wenzelm
# Date 1085836101 -7200
# Node ID dc23ff2629e2566dab1975337b110f94502ee53e
# Parent  c994f1c57fc7c1d52c4cbc99b010b6312743b952
handle raw symbols; Output.add_mode;

diff -r c994f1c57fc7 -r dc23ff2629e2 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat May 29 15:08:08 2004 +0200
+++ b/src/Pure/Thy/latex.ML	Sat May 29 15:08:21 2004 +0200
@@ -66,13 +66,13 @@
   c => if Symbol.is_digit c then enclose "{\\isadigit{" "}}" c else c;
 
 fun output_sym s =
-  if size s = 1 then output_chr s
-  else
-    (case explode s of
-      "\\" :: "<" :: "^" :: "r"::"a"::"w"::":"::cs => implode (#1 (Library.split_last cs)) 
-    | "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
-    | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
-    | _ => sys_error "output_sym");
+  if Symbol.is_char s then output_chr s
+  else if Symbol.is_raw s then Symbol.decode_raw s
+  else if String.isPrefix "\\<^" s then
+    enclose "\\isactrl" " " (String.substring (s, 3, size s - 4))
+  else if String.isPrefix "\\<" s then
+    enclose "{\\isasym" "}" (String.substring (s, 2, size s - 3))
+  else sys_error "output_sym";
 
 in
 
@@ -154,7 +154,7 @@
 val token_translation =
   map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
 
-val _ = Symbol.add_mode latexN (latex_output, latex_indent o #1);
+val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.default_raw);
 val setup = [Theory.add_tokentrfuns token_translation];