# HG changeset patch
# User wenzelm
# Date 971214284 -7200
# Node ID 4a7a1091cf6561f0973a3b9b7897f09d9c27cbb2
# Parent  76f0f0f1c97183869622d6c8b8d5c0c8c843c5a3
fully enclose "\isadigit{...}";
\<^foo> produces "\isactrlfoo ";

diff -r 76f0f0f1c971 -r 4a7a1091cf65 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Oct 10 23:43:47 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Oct 10 23:44:44 2000 +0200
@@ -61,13 +61,13 @@
   "|" => "{\\isacharbar}" |
   "}" => "{\\isacharbraceright}" |
   "~" => "{\\isachartilde}" |
-  c => if Symbol.is_digit c then enclose "\\isadigit{" "}" c else c;
+  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
-      cs as "\\" :: "<" :: "^" :: _ => implode (map output_chr cs)
+      "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
     | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
     | _ => sys_error "output_sym");