clarified signature;

--- a/src/Pure/General/completion.ML	Wed May 27 20:02:02 2020 +0200
+++ b/src/Pure/General/completion.ML	Wed May 27 20:38:59 2020 +0200
@@ -16,6 +16,10 @@
   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_item: string -> (string * 'a -> Markup.T) ->
+    (string * 'a) list -> Proof.context -> string * Position.T -> string
+  val check_entity: string -> (string * Position.T) list ->
+    Proof.context -> string * Position.T -> string
   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
@@ -75,21 +79,22 @@
   else [];
 
 
-(* system options *)
+(* check items *)
 
-fun check_option options ctxt (name, pos) =
-  let
-    val markup =
-      Options.markup options (name, pos) handle ERROR msg =>
-        let
-          val completion_report =
-            make_report (name, pos) (fn completed =>
-                Options.names options
-                |> filter completed
-                |> map (fn a => (a, ("system_option", a))));
-        in error (msg ^ completion_report) end;
-    val _ = Context_Position.report ctxt pos markup;
-  in name end;
+fun check_item kind markup items ctxt (name, pos) =
+  (case AList.lookup (op =) items name of
+    SOME x => (Context_Position.report ctxt pos (markup (name, x)); name)
+  | NONE =>
+      let
+        fun make_names completed =
+          map_filter (fn (a, _) => if completed a then SOME (a, (kind, a)) else NONE) items;
+        val completion_report = make_report (name, pos) make_names;
+      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end);
+
+fun check_entity kind = check_item kind (Position.entity_markup kind);
+
+
+val check_option = check_entity Markup.system_optionN o Options.dest;
 
 fun check_option_value ctxt (name, pos) (value, pos') options =
   let

--- a/src/Pure/PIDE/resources.ML	Wed May 27 20:02:02 2020 +0200
+++ b/src/Pure/PIDE/resources.ML	Wed May 27 20:38:59 2020 +0200
@@ -94,29 +94,17 @@
 fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
 
+
 fun check_name which kind markup ctxt (name, pos) =
-  let val entries = get_session_base which in
-    (case AList.lookup (op =) entries name of
-      SOME entry => (Context_Position.report ctxt pos (markup name entry); name)
-    | NONE =>
-        let
-          val completion_report =
-            Completion.make_report (name, pos)
-              (fn completed =>
-                entries
-                |> map #1
-                |> filter completed
-                |> sort_strings
-                |> map (fn a => (a, (kind, a))));
-        in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end)
-  end;
+  Completion.check_item kind markup (get_session_base which |> sort_by #1) ctxt (name, pos);
 
-fun markup_session name {pos, serial} =
-  Markup.properties
-    (Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name);
+val check_session =
+  check_name #session_positions "session"
+    (fn (name, {pos, serial}) =>
+      Markup.entity Markup.sessionN name
+      |> Markup.properties (Position.entity_properties_of false serial pos));
 
-val check_session = check_name #session_positions "session" markup_session;
-val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name);
+val check_doc = check_name #docs "documentation" (Markup.doc o #1);
 
 
 (* manage source files *)

--- a/src/Pure/System/isabelle_system.ML	Wed May 27 20:02:02 2020 +0200
+++ b/src/Pure/System/isabelle_system.ML	Wed May 27 20:38:59 2020 +0200
@@ -51,23 +51,9 @@
   bash_output_check "declare -Fx"
   |> split_lines |> map_filter (space_explode " " #> try List.last);
 
-fun check_bash_function ctxt (name, pos) =
-  let
-    val kind = Markup.bash_functionN;
-    val funs = bash_functions ();
-  in
-    if member (op =) funs name then
-      (Context_Position.report ctxt pos (Markup.bash_function name); name)
-    else
-      let
-        val completion_report =
-          Completion.make_report (name, pos)
-            (fn completed =>
-              filter completed funs
-              |> sort_strings
-              |> map (fn a => (a, (kind, a))));
-      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end
-  end;
+fun check_bash_function ctxt arg =
+  Completion.check_item Markup.bash_functionN (Markup.bash_function o #1)
+    (bash_functions () |> map (rpair ())) ctxt arg;
 
 
 (* directory operations *)

--- a/src/Pure/System/options.ML	Wed May 27 20:02:02 2020 +0200
+++ b/src/Pure/System/options.ML	Wed May 27 20:38:59 2020 +0200
@@ -13,8 +13,7 @@
   val unknownT: string
   type T
   val empty: T
-  val names: T -> string list
-  val markup: T -> string * Position.T -> Markup.T
+  val dest: T -> (string * Position.T) list
   val typ: T -> string -> string
   val bool: T -> string -> bool
   val int: T -> string -> int
@@ -29,7 +28,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
@@ -62,7 +60,9 @@
 
 val empty = Options Symtab.empty;
 
-fun names (Options tab) = sort_strings (Symtab.keys tab);
+fun dest (Options tab) =
+  Symtab.fold (fn (name, {pos, ...}) => cons (name, pos)) tab []
+  |> sort_by #1;
 
 
 (* check *)
@@ -80,17 +80,6 @@
   end;
 
 
-(* markup *)
-
-fun markup options (name, pos) =
-  let
-    val opt =
-      check_name options name
-        handle ERROR msg => error (msg ^ Position.here pos);
-    val props = Position.def_properties_of (#pos opt);
-  in Markup.properties props (Markup.entity Markup.system_optionN name) end;
-
-
 (* typ *)
 
 fun typ options name = #typ (check_name options name);
@@ -189,7 +178,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;

--- a/src/Pure/System/scala.ML	Wed May 27 20:02:02 2020 +0200
+++ b/src/Pure/System/scala.ML	Wed May 27 20:38:59 2020 +0200
@@ -75,23 +75,9 @@
 
 fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
 
-fun check_function ctxt (name, pos) =
-  let
-    val kind = Markup.scala_functionN;
-    val funs = functions ();
-  in
-    if member (op =) funs name then
-      (Context_Position.report ctxt pos (Markup.scala_function name); name)
-    else
-      let
-        val completion_report =
-          Completion.make_report (name, pos)
-            (fn completed =>
-              filter completed funs
-              |> sort_strings
-              |> map (fn a => (a, (kind, a))));
-      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end
-  end;
+fun check_function ctxt arg =
+  Completion.check_item Markup.scala_functionN (Markup.scala_function o #1)
+    (functions () |> sort_strings |> map (rpair ())) ctxt arg;
 
 val _ = Theory.setup
  (ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>