# HG changeset patch
# User wenzelm
# Date 850218993 -3600
# Node ID 821f44a0abbae4a59bb3c2400e80a2277e000779
# Parent  963285471dc5bcb85800f31a80a52aca3389f8ee
mfix_to_xprod: now uses read_charnames;

diff -r 963285471dc5 -r 821f44a0abba src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Tue Dec 10 12:55:37 1996 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Tue Dec 10 12:56:33 1996 +0100
@@ -160,9 +160,10 @@
 fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) =
   let
     fun err msg =
-      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for "
-                ^ quote const);
+      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
         error msg);
+    fun post_err () = error ("The error(s) above occurred in mixfix annotation " ^
+      quote sy ^ " for " ^ quote const);
 
     fun check_pri p =
       if p >= 0 andalso p <= max_pri then ()
@@ -186,13 +187,6 @@
       fun scan_delim_char ("'" :: c :: cs) =
             if is_blank c then raise LEXICAL_ERROR else (c, cs)
         | scan_delim_char ["'"] = err "trailing escape character"
-        | scan_delim_char ("\\" :: "<" :: cs) =
-            let
-              val (ch_name, cs') = (scan_id -- $$ ">" >> #1) cs
-                handle LEXICAL_ERROR => err "malformed symbolic char specification";
-              val c = the (SymbolFont.char ch_name)
-                handle OPTION _ => err ("unknown symbolic char name: " ^ quote ch_name);
-            in (c, cs') end
         | scan_delim_char (chs as c :: cs) =
             if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
         | scan_delim_char [] = raise LEXICAL_ERROR;
@@ -246,16 +240,21 @@
           else a
       | unify_logtypes _ a = a;
 
-    val raw_symbs = scan_symbs (explode sy);
+
+    val sy_chars =
+      SymbolFont.read_charnames (explode sy) handle ERROR => post_err ();
+    val raw_symbs = scan_symbs sy_chars;
     val (symbs, lhs) = add_args raw_symbs typ pris;
-    val copy_prod = lhs mem ["prop", "logic"]
-          andalso const <> ""
-          andalso not (null symbs)
-          andalso not (exists is_delim symbs);
-    val lhs' = if convert andalso not copy_prod then
-                 (if lhs mem logtypes then logic
-                  else if lhs = "prop" then sprop else lhs)
-               else lhs;
+    val copy_prod =
+      lhs mem ["prop", "logic"]
+        andalso const <> ""
+        andalso not (null symbs)
+        andalso not (exists is_delim symbs);
+    val lhs' =
+      if convert andalso not copy_prod then
+       (if lhs mem logtypes then logic
+        else if lhs = "prop" then sprop else lhs)
+      else lhs;
     val symbs' = map (unify_logtypes copy_prod) symbs;
     val xprod = XProd (lhs', symbs', const, pri);
   in
@@ -340,4 +339,3 @@
   ([], []);
 
 end;
-