# HG changeset patch
# User wenzelm
# Date 1427290780 -3600
# Node ID 675d0c692c41f8ea8b6b759638cb995f92f8387b
# Parent  6b0d9e8ac227689a1c6ae12b294a3356e86607a7
semantic completion for @{system_option};

diff -r 6b0d9e8ac227 -r 675d0c692c41 src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Wed Mar 25 13:45:52 2015 +0100
+++ b/src/Pure/General/completion.ML	Wed Mar 25 14:39:40 2015 +0100
@@ -9,6 +9,7 @@
   type T
   val names: Position.T -> (string * (string * string)) list -> T
   val none: T
+  val make: string * Position.T -> ((string -> bool) -> (string * (string * string)) list) -> T
   val reported_text: T -> string
   val suppress_abbrevs: string -> Markup.T list
 end;
@@ -16,12 +17,12 @@
 structure Completion: COMPLETION =
 struct
 
+(* completion of names *)
+
 abstype T =
   Completion of {pos: Position.T, total: int, names: (string * (string * string)) list}
 with
 
-(* completion of names *)
-
 fun dest (Completion args) = args;
 
 fun names pos names =
@@ -34,6 +35,11 @@
 
 val none = names Position.none [];
 
+fun make (name, pos) make_names =
+  if Position.is_reported pos andalso name <> "" andalso name <> "_"
+  then names pos (make_names (String.isPrefix (Name.clean name)))
+  else none;
+
 fun reported_text completion =
   let val {pos, total, names} = dest completion in
     if Position.is_reported pos andalso not (null names) then
diff -r 6b0d9e8ac227 -r 675d0c692c41 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Mar 25 13:45:52 2015 +0100
+++ b/src/Pure/General/name_space.ML	Wed Mar 25 14:39:40 2015 +0100
@@ -232,7 +232,7 @@
 (* completion *)
 
 fun completion context space (xname, pos) =
-  if Position.is_reported pos andalso xname <> "" andalso xname <> "_" then
+  Completion.make (xname, pos) (fn completed =>
     let
       fun result_ord ((xname1, (_, name1)), (xname2, (_, name2))) =
         (case bool_ord (apply2 Long_Name.is_local (name2, name1)) of
@@ -241,21 +241,18 @@
               EQUAL => string_ord (xname1, xname2)
             | ord => ord)
         | ord => ord);
-      val x = Name.clean xname;
       val Name_Space {kind, internals, ...} = space;
       val ext = extern_shortest (Context.proof_of context) space;
-      val names =
-        Change_Table.fold
-          (fn (a, (name :: _, _)) =>
-              if String.isPrefix x a andalso not (is_concealed space name)
-              then
-                let val a' = ext name
-                in if a = a' then cons (a', (kind, name)) else I end
-              else I
-            | _ => I) internals []
-        |> sort_distinct result_ord;
-    in Completion.names pos names end
-  else Completion.none;
+    in
+      Change_Table.fold
+        (fn (a, (name :: _, _)) =>
+            if completed a andalso not (is_concealed space name) then
+              let val a' = ext name
+              in if a = a' then cons (a', (kind, name)) else I end
+            else I
+          | _ => I) internals []
+      |> sort_distinct result_ord
+    end);
 
 
 (* merge *)
diff -r 6b0d9e8ac227 -r 675d0c692c41 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Mar 25 13:45:52 2015 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Mar 25 14:39:40 2015 +0100
@@ -37,8 +37,19 @@
 val _ = Theory.setup
  (ML_Antiquotation.value @{binding system_option}
     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
-      (Context_Position.report ctxt pos (Options.default_markup (name, pos));
-        ML_Syntax.print_string name))) #>
+      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 cat_error msg report end;
+        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)) =>
diff -r 6b0d9e8ac227 -r 675d0c692c41 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Wed Mar 25 13:45:52 2015 +0100
+++ b/src/Pure/System/options.ML	Wed Mar 25 14:39:40 2015 +0100
@@ -13,6 +13,7 @@
   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
@@ -59,6 +60,8 @@
 
 val empty = Options Symtab.empty;
 
+fun names (Options tab) = sort_strings (Symtab.keys tab);
+
 
 (* check *)