--- a/src/Pure/Syntax/syntax_ext.ML Fri Apr 01 18:32:52 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Fri Apr 01 18:43:54 2016 +0200
@@ -178,9 +178,6 @@
in
-fun show_props props =
- commas_quote (map #1 props) ^ Position.here_list (map (#2 o #2) props);
-
fun read_properties ss =
let
val props =
@@ -188,9 +185,10 @@
(props, []) => props
| (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos));
val _ =
- (case duplicates (eq_fst op =) props of
+ (case AList.group (op =) props |> filter (fn (_, [_]) => false | _ => true) of
[] => ()
- | dups => error ("Duplicate properties: " ^ show_props dups));
+ | dups => error ("Duplicate properties: " ^ commas_quote (map #1 dups) ^
+ Position.here_list (map #2 (maps #2 dups))));
in props end;
val get_string = get_property "" I;
@@ -221,7 +219,8 @@
val markup = (markup_name, map (apsnd #1) markup_props);
val _ =
if markup_name = "" andalso not (null markup_props) then
- error ("Markup name required for block properties: " ^ show_props markup_props)
+ error ("Markup name required for block properties: " ^
+ commas_quote (map #1 markup_props) ^ Position.here_list (map (#2 o #2) markup_props))
else ();
val consistent = get_bool Markup.consistentN props;