src/Pure/General/completion.ML

--- a/src/Pure/General/completion.ML	Mon Nov 12 14:02:33 2018 +0100
+++ b/src/Pure/General/completion.ML	Mon Nov 12 15:14:12 2018 +0100
@@ -6,12 +6,15 @@
 
 signature COMPLETION =
 sig
+  type name = string * (string * string)
   type T
-  val names: Position.T -> (string * (string * string)) list -> T
+  val names: Position.T -> name list -> T
   val none: T
-  val make: string * Position.T -> ((string -> bool) -> (string * (string * string)) list) -> T
+  val make: string * Position.T -> ((string -> bool) -> name list) -> T
   val encode: T -> XML.body
-  val reported_text: T -> string
+  val markup_element: T -> Markup.T * XML.body
+  val markup_report: T list -> string
+  val make_report: string * Position.T -> ((string -> bool) -> name list) -> string
   val suppress_abbrevs: string -> Markup.T list
   val check_option: Options.T -> Proof.context -> string * Position.T -> string
   val check_option_value:
@@ -23,8 +26,9 @@
 
 (* completion of names *)
 
-abstype T =
-  Completion of {pos: Position.T, total: int, names: (string * (string * string)) list}
+type name = string * (string * string);  (*external name, kind, internal name*)
+
+abstype T = Completion of {pos: Position.T, total: int, names: name list}
 with
 
 fun dest (Completion args) = args;
@@ -50,15 +54,18 @@
     open XML.Encode;
   in pair int (list (pair string (pair string string))) (total, names) end;
 
-fun reported_text completion =
+fun markup_element completion =
   let val {pos, names, ...} = dest completion in
     if Position.is_reported pos andalso not (null names) then
-      let
-        val markup = Position.markup pos Markup.completion;
-      in YXML.string_of (XML.Elem (markup, encode completion)) end
-    else ""
+      (Position.markup pos Markup.completion, encode completion)
+    else (Markup.empty, [])
   end;
 
+val markup_report =
+  map (markup_element #> XML.Elem) #> YXML.string_of_body #> Markup.markup_report;
+
+val make_report = markup_report oo (single oo make);
+
 
 (* suppress short abbreviations *)
 
@@ -75,13 +82,12 @@
     val markup =
       Options.markup options (name, pos) handle ERROR msg =>
         let
-          val completion =
-            make (name, pos) (fn completed =>
+          val completion_report =
+            make_report (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;
+        in error (msg ^ completion_report) end;
     val _ = Context_Position.report ctxt pos markup;
   in name end;