# HG changeset patch
# User wenzelm
# Date 1513423000 -3600
# Node ID 16519cd83ed4c9ee4c18c92b587e8ad04ca57cd1
# Parent  ad538f6c5d2fcff2db8284dd9998de1e033c47d4
clarified signature;

diff -r ad538f6c5d2f -r 16519cd83ed4 src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Thu Dec 14 18:42:39 2017 +0100
+++ b/src/Pure/General/completion.ML	Sat Dec 16 12:16:40 2017 +0100
@@ -13,6 +13,9 @@
   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 =
@@ -64,4 +67,30 @@
   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;
diff -r ad538f6c5d2f -r 16519cd83ed4 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Thu Dec 14 18:42:39 2017 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Sat Dec 16 12:16:40 2017 +0100
@@ -42,19 +42,7 @@
 val _ = Theory.setup
  (ML_Antiquotation.value \<^binding>\<open>system_option\<close>
     (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
-      let
-        val markup =
-          Options.default_markup (name, pos) handle ERROR msg =>
-            let
-              val completion =
-                Completion.make (name, pos) (fn completed =>
-                    Options.names (Options.default ())
-                    |> filter completed
-                    |> map (fn a => (a, ("system_option", a))));
-              val report = Markup.markup_report (Completion.reported_text completion);
-            in error (msg ^ report) end;
-        val _ = Context_Position.report ctxt pos markup;
-      in ML_Syntax.print_string name end)) #>
+      (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #>
 
   ML_Antiquotation.value \<^binding>\<open>theory\<close>
     (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
diff -r ad538f6c5d2f -r 16519cd83ed4 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Thu Dec 14 18:42:39 2017 +0100
+++ b/src/Pure/System/options.ML	Sat Dec 16 12:16:40 2017 +0100
@@ -29,7 +29,6 @@
   val update: string -> string -> T -> T
   val decode: XML.body -> T
   val default: unit -> T
-  val default_markup: string * Position.T -> Markup.T
   val default_typ: string -> string
   val default_bool: string -> bool
   val default_int: string -> int
@@ -189,7 +188,6 @@
     SOME options => options
   | NONE => err_no_default ());
 
-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;