more positions and markup;

--- a/src/Pure/ML/ml_antiquotations.ML	Tue Apr 08 13:24:08 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Tue Apr 08 14:15:48 2014 +0200
@@ -8,9 +8,17 @@
 struct
 
 val _ = Theory.setup
- (ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
-    (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
-     ML_Syntax.print_string name))) #>
+ (ML_Antiquotation.value @{binding option}
+    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+      let
+        val def_pos =
+          Options.default_position name
+            handle ERROR msg => error (msg ^ Position.here pos);
+        val markup =
+          Markup.properties (Position.def_properties_of def_pos)
+            (Markup.entity Markup.system_optionN name);
+        val _ = Context_Position.report ctxt pos markup;
+      in ML_Syntax.print_string name end)) #>
 
   ML_Antiquotation.value @{binding theory}
     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>

--- a/src/Pure/PIDE/markup.ML	Tue Apr 08 13:24:08 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Apr 08 14:15:48 2014 +0200
@@ -63,6 +63,7 @@
   val fbreakN: string val fbreak: T
   val itemN: string val item: T
   val hiddenN: string val hidden: T
+  val system_optionN: string
   val theoryN: string
   val classN: string
   val type_nameN: string
@@ -358,7 +359,9 @@
 val (hiddenN, hidden) = markup_elem "hidden";
 
 
-(* logical entities *)
+(* formal entities *)
+
+val system_optionN = "system_option";
 
 val theoryN = "theory";
 val classN = "class";

--- a/src/Pure/System/options.ML	Tue Apr 08 13:24:08 2014 +0200
+++ b/src/Pure/System/options.ML	Tue Apr 08 14:15:48 2014 +0200
@@ -13,6 +13,7 @@
   val unknownT: string
   type T
   val empty: T
+  val position: T -> string -> Position.T
   val typ: T -> string -> string
   val bool: T -> string -> bool
   val int: T -> string -> int
@@ -22,10 +23,11 @@
   val put_int: string -> int -> T -> T
   val put_real: string -> real -> T -> T
   val put_string: string -> string -> T -> T
-  val declare: {name: string, typ: string, value: string} -> T -> T
+  val declare: {pos: Position.T, name: string, typ: string, value: string} -> T -> T
   val update: string -> string -> T -> T
   val decode: XML.body -> T
   val default: unit -> T
+  val default_position: string -> Position.T
   val default_typ: string -> string
   val default_bool: string -> bool
   val default_int: string -> int
@@ -53,7 +55,7 @@
 val stringT = "string";
 val unknownT = "unknown";
 
-datatype T = Options of {typ: string, value: string} Symtab.table;
+datatype T = Options of {pos: Position.T, typ: string, value: string} Symtab.table;
 
 val empty = Options Symtab.empty;
 
@@ -73,8 +75,9 @@
   end;
 
 
-(* typ *)
+(* declaration *)
 
+fun position options name = #pos (check_name options name);
 fun typ options name = #typ (check_name options name);
 
 
@@ -82,7 +85,7 @@
 
 fun put T print name x (options as Options tab) =
   let val opt = check_type options name T
-  in Options (Symtab.update (name, {typ = #typ opt, value = print x}) tab) end;
+  in Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = print x}) tab) end;
 
 fun get T parse options name =
   let val opt = check_type options name T in
@@ -118,29 +121,39 @@
     else ()
   end;
 
-fun declare {name, typ, value} (Options tab) =
+fun declare {pos, name, typ, value} (Options tab) =
   let
-    val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
-      handle Symtab.DUP _ => error ("Duplicate declaration of system option " ^ quote name);
+    val options' =
+      (case Symtab.lookup tab name of
+        SOME other =>
+          error ("Duplicate declaration of system option " ^ quote name ^ Position.here pos ^
+            Position.here (#pos other))
+      | NONE => Options (Symtab.update (name, {pos = pos, typ = typ, value = value}) tab));
     val _ =
       typ = boolT orelse typ = intT orelse typ = realT orelse typ = stringT orelse
-        error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ);
+        error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ ^
+          Position.here pos);
     val _ = check_value options' name;
   in options' end;
 
 fun update name value (options as Options tab) =
   let
     val opt = check_name options name;
-    val options' = Options (Symtab.update (name, {typ = #typ opt, value = value}) tab);
+    val options' =
+      Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = value}) tab);
     val _ = check_value options' name;
   in options' end;
 
 
 (* decode *)
 
-fun decode body =
-  fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
-    (let open XML.Decode in list (triple string string string) end body) empty;
+fun decode_opt body =
+  let open XML.Decode
+  in list (pair properties (pair string (pair string string))) end body
+  |> map (fn (props, (name, (typ, value))) =>
+      {pos = Position.of_properties props, name = name, typ = typ, value = value});
+
+fun decode body = fold declare (decode_opt body) empty;
 
 
 
@@ -160,6 +173,7 @@
     SOME options => options
   | NONE => err_no_default ());
 
+fun default_position name = position (default ()) name;
 fun default_typ name = typ (default ()) name;
 fun default_bool name = bool (default ()) name;
 fun default_int name = int (default ()) name;

--- a/src/Pure/System/options.scala	Tue Apr 08 13:24:08 2014 +0200
+++ b/src/Pure/System/options.scala	Tue Apr 08 14:15:48 2014 +0200
@@ -29,8 +29,15 @@
   case object String extends Type
   case object Unknown extends Type
 
-  case class Opt(public: Boolean, name: String, typ: Type, value: String, default_value: String,
-    description: String, section: String)
+  case class Opt(
+    public: Boolean,
+    pos: Position.T,
+    name: String,
+    typ: Type,
+    value: String,
+    default_value: String,
+    description: String,
+    section: String)
   {
     private def print(default: Boolean): String =
     {
@@ -88,8 +95,8 @@
         { case _ ~ a => (options: Options) => options.set_section(a) } |
       opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
-        { case a ~ _ ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
-            (options: Options) => options.declare(a.isDefined, b, c, d, e) }
+        { case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
+            (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
     }
 
     val prefs_entry: Parser[Options => Options] =
@@ -260,11 +267,18 @@
     }
   }
 
-  def declare(public: Boolean, name: String, typ_name: String, value: String, description: String)
-    : Options =
+  def declare(
+    public: Boolean,
+    pos: Position.T,
+    name: String,
+    typ_name: String,
+    value: String,
+    description: String): Options =
   {
     options.get(name) match {
-      case Some(_) => error("Duplicate declaration of option " + quote(name))
+      case Some(other) =>
+        error("Duplicate declaration of option " + quote(name) + Position.here(pos) +
+          Position.here(other.pos))
       case None =>
         val typ =
           typ_name match {
@@ -272,9 +286,11 @@
             case "int" => Options.Int
             case "real" => Options.Real
             case "string" => Options.String
-            case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
+            case _ =>
+              error("Unknown type for option " + quote(name) + " : " + quote(typ_name) +
+                Position.here(pos))
           }
-        val opt = Options.Opt(public, name, typ, value, value, description, section)
+        val opt = Options.Opt(public, pos, name, typ, value, value, description, section)
         (new Options(options + (name -> opt), section)).check_value(name)
     }
   }
@@ -282,10 +298,10 @@
   def add_permissive(name: String, value: String): Options =
   {
     if (options.isDefinedAt(name)) this + (name, value)
-    else
-      new Options(
-        options +
-          (name -> Options.Opt(false, name, Options.Unknown, value, value, "", "")), section)
+    else {
+      val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, "", "")
+      new Options(options + (name -> opt), section)
+    }
   }
 
   def + (name: String, value: String): Options =
@@ -330,11 +346,11 @@
   def encode: XML.Body =
   {
     val opts =
-      for ((name, opt) <- options.toList; if !opt.unknown)
-        yield (name, opt.typ.print, opt.value)
+      for ((_, opt) <- options.toList; if !opt.unknown)
+        yield (opt.pos, (opt.name, (opt.typ.print, opt.value)))
 
-    import XML.Encode.{string => str, _}
-    list(triple(str, str, str))(opts)
+    import XML.Encode.{string => string_, _}
+    list(pair(properties, pair(string_, pair(string_, string_))))(opts)
   }