src/Pure/System/options.ML

   val realT: string
   val stringT: string
   val unknownT: string
   type T
   val empty: T
-  val position: T -> string -> Position.T
+  val markup: T -> string * Position.T -> Markup.T
   val typ: T -> string -> string
   val bool: T -> string -> bool
   val int: T -> string -> int
   val real: T -> string -> real
   val string: T -> string -> string

   val put_string: string -> 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_markup: string * Position.T -> Markup.T
   val default_typ: string -> string
   val default_bool: string -> bool
   val default_int: string -> int
   val default_real: string -> real
   val default_string: string -> string

     if #typ opt = typ then opt
     else error ("Ill-typed system option " ^ quote name ^ " : " ^ #typ opt ^ " vs. " ^ typ)
   end;
 
 
-(* declaration *)
-
-fun position options name = #pos (check_name options name);
+(* markup *)
+
+fun markup options (name, pos) =
+  let
+    val opt =
+      check_name options name
+        handle ERROR msg => error (msg ^ Position.here pos);
+    val props = Position.def_properties_of (#pos opt);
+  in Markup.properties props (Markup.entity Markup.system_optionN name) end;
+
+
+(* typ *)
+
 fun typ options name = #typ (check_name options name);
 
 
 (* basic operations *)
 

 fun default () =
   (case Synchronized.value global_default of
     SOME options => options
   | NONE => err_no_default ());
 
-fun default_position name = position (default ()) name;
+fun default_markup arg = markup (default ()) arg;
 fun default_typ name = typ (default ()) name;
 fun default_bool name = bool (default ()) name;
 fun default_int name = int (default ()) name;
 fun default_real name = real (default ()) name;
 fun default_string name = string (default ()) name;