# HG changeset patch # User wenzelm # Date 1590604739 -7200 # Node ID d2509353648265a2698e253495ecca40578c4b87 # Parent f8b0271cc744efa7fbca17c19d9b3e02ea94df38 clarified signature; diff -r f8b0271cc744 -r d25093536482 src/Pure/General/completion.ML --- 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 diff -r f8b0271cc744 -r d25093536482 src/Pure/PIDE/resources.ML --- 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 *) diff -r f8b0271cc744 -r d25093536482 src/Pure/System/isabelle_system.ML --- 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 *) diff -r f8b0271cc744 -r d25093536482 src/Pure/System/options.ML --- 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; diff -r f8b0271cc744 -r d25093536482 src/Pure/System/scala.ML --- 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>\scala_function\