# HG changeset patch
# User wenzelm
# Date 1459514942 -7200
# Node ID 2461a58b3587e00cb484ccf0b5d3148003e464c6
# Parent  70b9c7d4ed7fd5034e4c74802122fa79a38e6159
clarified treatment of properties;
tuned messages;

diff -r 70b9c7d4ed7f -r 2461a58b3587 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Apr 01 14:38:54 2016 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Apr 01 14:49:02 2016 +0200
@@ -8,6 +8,7 @@
 sig
   val parse_bool: string -> bool
   val print_bool: bool -> string
+  val parse_nat: string -> int
   val parse_int: string -> int
   val print_int: int -> string
   val parse_real: string -> real
@@ -67,6 +68,7 @@
   val docN: string val doc: string -> T
   val markupN: string val get_markup: Properties.T -> string
   val consistentN: string val get_consistent: Properties.T -> bool
+  val block_properties: string list
   val indentN: string val get_indent: Properties.T -> int
   val widthN: string
   val blockN: string val block: bool -> int -> T
@@ -228,23 +230,32 @@
 
 fun parse_bool "true" = true
   | parse_bool "false" = false
-  | parse_bool s = raise Fail ("Bad boolean: " ^ quote s);
+  | parse_bool s = raise Fail ("Bad boolean " ^ quote s);
 
 val print_bool = Bool.toString;
 
+
+fun parse_nat s =
+  let val i = Int.fromString s in
+    if is_none i orelse the i < 0
+    then raise Fail ("Bad natural number " ^ quote s)
+    else the i
+  end;
+
 fun parse_int s =
   let val i = Int.fromString s in
     if is_none i orelse String.isPrefix "~" s
-    then raise Fail ("Bad integer: " ^ quote s)
+    then raise Fail ("Bad integer " ^ quote s)
     else the i
   end;
 
 val print_int = signed_string_of_int;
 
+
 fun parse_real s =
   (case Real.fromString s of
     SOME x => x
-  | NONE => raise Fail ("Bad real: " ^ quote s));
+  | NONE => raise Fail ("Bad real " ^ quote s));
 
 fun print_real x =
   let val s = signed_string_of_real x in
@@ -385,13 +396,16 @@
 (* pretty printing *)
 
 val markupN = "markup";
+val consistentN = "consistent";
+val indentN = "indent";
+
+val block_properties = [markupN, consistentN, indentN];
+
 fun get_markup props = the_default "" (Properties.get props markupN);
 
-val consistentN = "consistent";
 fun get_consistent props =
   the_default false (Option.map parse_bool (Properties.get props consistentN));
 
-val indentN = "indent";
 fun get_indent props =
   the_default 0 (Option.map parse_int (Properties.get props indentN));
 
diff -r 70b9c7d4ed7f -r 2461a58b3587 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 14:38:54 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 14:49:02 2016 +0200
@@ -143,6 +143,59 @@
 val typ_to_nonterm1 = typ_to_nt "logic";
 
 
+(* properties *)
+
+local
+
+open Basic_Symbol_Pos;
+
+val err_prefix = "Error in mixfix block properties: ";
+val !!! = Symbol_Pos.!!! (fn () => err_prefix ^ "expected identifier or numeral or cartouche");
+
+val scan_atom =
+  Symbol_Pos.scan_ident ||
+  ($$$ "-" @@@ (Symbol_Pos.scan_float || Symbol_Pos.scan_nat)) ||
+  Symbol_Pos.scan_float || Symbol_Pos.scan_nat ||
+  Symbol_Pos.scan_cartouche_content err_prefix;
+
+val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol);
+val scan_item =
+  scan_blanks |-- scan_atom --| scan_blanks
+    >> (fn ss => (Symbol_Pos.content ss, #1 (Symbol_Pos.range ss)));
+
+val scan_prop =
+  scan_item -- Scan.optional ($$ "=" |-- !!! scan_item >> #1) "true"
+    >> (fn ((x, pos), y) => (x, (y, pos)));
+
+val scan_end = Scan.ahead (Scan.one Symbol_Pos.is_eof) >> K ("", Position.none) || !!! Scan.fail;
+
+fun get_property default parse name props =
+  (case AList.lookup (op =) props name of
+    NONE => default
+  | SOME (s, pos) =>
+      (parse s handle Fail msg => error (msg ^ " for property " ^ quote name ^ Position.here pos)));
+
+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 = the (Scan.read Symbol_Pos.stopper (Scan.repeat1 scan_prop --| scan_end) ss);
+    val _ =
+      (case duplicates (eq_fst op =) props of
+        [] => ()
+      | dups => error ("Duplicate properties: " ^ show_props dups));
+  in props end;
+
+val get_string = get_property "" I;
+val get_bool = get_property false Markup.parse_bool;
+val get_nat = get_property 0 Markup.parse_nat;
+
+end;
+
+
 (* read mixfix annotations *)
 
 local
@@ -153,40 +206,21 @@
 fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol);
 fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol);
 
-(*block properties*)
-local
-  val err_prefix = "Error in mixfix block properties: ";
-  val !!! = Symbol_Pos.!!! (fn () => err_prefix ^ "expected identifier or numeral or cartouche");
-
-  val scan_atom =
-    Symbol_Pos.scan_ident ||
-    ($$$ "-" @@@ (Symbol_Pos.scan_float || Symbol_Pos.scan_nat)) ||
-    Symbol_Pos.scan_float || Symbol_Pos.scan_nat ||
-    Symbol_Pos.scan_cartouche_content err_prefix;
-
-  val scan_blanks = scan_many Symbol.is_blank;
-  val scan_item = scan_blanks |-- scan_atom --| scan_blanks >> Symbol_Pos.content;
+fun read_block_properties ss =
+  let
+    val props = read_properties ss;
 
-  val scan_prop = scan_item -- Scan.optional ($$ "=" |-- !!! scan_item) "true";
-  val scan_end = Scan.ahead (Scan.one Symbol_Pos.is_eof) >> K "" || !!! Scan.fail;
-in
-  fun read_block_properties ss =
-    let
-      fun err msg = error (msg ^ Position.here (#1 (Symbol_Pos.range ss)));
-      val props = the (Scan.read Symbol_Pos.stopper (Scan.repeat1 scan_prop --| scan_end) ss);
+    val markup_name = get_string Markup.markupN props;
+    val markup_props = fold (AList.delete (op =)) Markup.block_properties props;
+    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)
+      else ();
 
-      val markup_name = Markup.get_markup props;
-      val markup_props =
-        fold Properties.remove [Markup.markupN, Markup.consistentN, Markup.indentN] props;
-      val _ =
-        if markup_name = "" andalso not (null markup_props) then
-          err ("Markup name required for block properties: " ^ commas_quote (map #1 markup_props))
-        else ();
-
-      val consistent = Markup.get_consistent props handle Fail msg => err msg;
-      val indent = Markup.get_indent props handle Fail msg => err msg;
-    in Bg {markup = (markup_name, markup_props), consistent = consistent, indent = indent} end;
-end;
+    val consistent = get_bool Markup.consistentN props;
+    val indent = get_nat Markup.indentN props;
+  in Bg {markup = markup, consistent = consistent, indent = indent} end;
 
 val read_block_indent =
   map Symbol_Pos.symbol #> (fn ss =>