src/Pure/System/options.ML

   val realT: string
   val stringT: string
   val unknownT: string
   type T
   val empty: T
+  val names: T -> string list
   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

 
 datatype T = Options of {pos: Position.T, typ: string, value: string} Symtab.table;
 
 val empty = Options Symtab.empty;
 
+fun names (Options tab) = sort_strings (Symtab.keys tab);
+
 
 (* check *)
 
 fun check_name (Options tab) name =
   let val opt = Symtab.lookup tab name in