src/Pure/Syntax/syn_ext.ML
changeset 2364 821f44a0abba
parent 2254 2888b4c1db7f
child 2382 e7c2bce815ba
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue Dec 10 12:55:37 1996 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue Dec 10 12:56:33 1996 +0100
     1.3 @@ -160,9 +160,10 @@
     1.4  fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) =
     1.5    let
     1.6      fun err msg =
     1.7 -      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for "
     1.8 -                ^ quote const);
     1.9 +      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
    1.10          error msg);
    1.11 +    fun post_err () = error ("The error(s) above occurred in mixfix annotation " ^
    1.12 +      quote sy ^ " for " ^ quote const);
    1.13  
    1.14      fun check_pri p =
    1.15        if p >= 0 andalso p <= max_pri then ()
    1.16 @@ -186,13 +187,6 @@
    1.17        fun scan_delim_char ("'" :: c :: cs) =
    1.18              if is_blank c then raise LEXICAL_ERROR else (c, cs)
    1.19          | scan_delim_char ["'"] = err "trailing escape character"
    1.20 -        | scan_delim_char ("\\" :: "<" :: cs) =
    1.21 -            let
    1.22 -              val (ch_name, cs') = (scan_id -- $$ ">" >> #1) cs
    1.23 -                handle LEXICAL_ERROR => err "malformed symbolic char specification";
    1.24 -              val c = the (SymbolFont.char ch_name)
    1.25 -                handle OPTION _ => err ("unknown symbolic char name: " ^ quote ch_name);
    1.26 -            in (c, cs') end
    1.27          | scan_delim_char (chs as c :: cs) =
    1.28              if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
    1.29          | scan_delim_char [] = raise LEXICAL_ERROR;
    1.30 @@ -246,16 +240,21 @@
    1.31            else a
    1.32        | unify_logtypes _ a = a;
    1.33  
    1.34 -    val raw_symbs = scan_symbs (explode sy);
    1.35 +
    1.36 +    val sy_chars =
    1.37 +      SymbolFont.read_charnames (explode sy) handle ERROR => post_err ();
    1.38 +    val raw_symbs = scan_symbs sy_chars;
    1.39      val (symbs, lhs) = add_args raw_symbs typ pris;
    1.40 -    val copy_prod = lhs mem ["prop", "logic"]
    1.41 -          andalso const <> ""
    1.42 -          andalso not (null symbs)
    1.43 -          andalso not (exists is_delim symbs);
    1.44 -    val lhs' = if convert andalso not copy_prod then
    1.45 -                 (if lhs mem logtypes then logic
    1.46 -                  else if lhs = "prop" then sprop else lhs)
    1.47 -               else lhs;
    1.48 +    val copy_prod =
    1.49 +      lhs mem ["prop", "logic"]
    1.50 +        andalso const <> ""
    1.51 +        andalso not (null symbs)
    1.52 +        andalso not (exists is_delim symbs);
    1.53 +    val lhs' =
    1.54 +      if convert andalso not copy_prod then
    1.55 +       (if lhs mem logtypes then logic
    1.56 +        else if lhs = "prop" then sprop else lhs)
    1.57 +      else lhs;
    1.58      val symbs' = map (unify_logtypes copy_prod) symbs;
    1.59      val xprod = XProd (lhs', symbs', const, pri);
    1.60    in
    1.61 @@ -340,4 +339,3 @@
    1.62    ([], []);
    1.63  
    1.64  end;
    1.65 -