src/Pure/General/completion.ML

   val none: T
   val make: string * Position.T -> ((string -> bool) -> (string * (string * string)) list) -> T
   val encode: T -> XML.body
   val reported_text: T -> string
   val suppress_abbrevs: string -> Markup.T list
+  val check_option: Options.T -> Proof.context -> string * Position.T -> string
+  val check_option_value:
+    Proof.context -> string * Position.T -> string * Position.T -> Options.T -> string * Options.T
 end;
 
 structure Completion: COMPLETION =
 struct
 

 fun suppress_abbrevs s =
   if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) <= 1 orelse s = "::")
   then [Markup.no_completion]
   else [];
 
+
+(* system options *)
+
+fun check_option options ctxt (name, pos) =
+  let
+    val markup =
+      Options.markup options (name, pos) handle ERROR msg =>
+        let
+          val completion =
+            make (name, pos) (fn completed =>
+                Options.names options
+                |> filter completed
+                |> map (fn a => (a, ("system_option", a))));
+          val report = Markup.markup_report (reported_text completion);
+        in error (msg ^ report) end;
+    val _ = Context_Position.report ctxt pos markup;
+  in name end;
+
+fun check_option_value ctxt (name, pos) (value, pos') options =
+  let
+    val _ = check_option options ctxt (name, pos);
+    val options' =
+      Options.update name value options
+        handle ERROR msg => error (msg ^ Position.here pos');
+  in (name, options') end;
+
 end;