# HG changeset patch # User wenzelm # Date 1542032052 -3600 # Node ID bf6937af7fe80a3d2b41689ef7620cf17436166c # Parent 4c3704ecb0e62b184fe094b2cf724e42d6b43fd4 clarified signature; diff -r 4c3704ecb0e6 -r bf6937af7fe8 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; diff -r 4c3704ecb0e6 -r bf6937af7fe8 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Mon Nov 12 14:02:33 2018 +0100 +++ b/src/Pure/General/name_space.ML Mon Nov 12 15:14:12 2018 +0100 @@ -564,12 +564,9 @@ |> map (fn pos => (pos, markup space name)); in ((name, reports), x) end | NONE => - let - val completions = map (fn pos => completion context space (K true) (xname, pos)) ps; - in - error (undefined space name ^ Position.here_list ps ^ - Markup.markup_report (implode (map Completion.reported_text completions))) - end) + error (undefined space name ^ Position.here_list ps ^ + Completion.markup_report + (map (fn pos => completion context space (K true) (xname, pos)) ps))) end; fun check context table (xname, pos) = diff -r 4c3704ecb0e6 -r bf6937af7fe8 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Mon Nov 12 14:02:33 2018 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Mon Nov 12 15:14:12 2018 +0100 @@ -293,15 +293,14 @@ in name end else let - val completion = - Completion.make (name, pos) + val completion_report = + Completion.make_report (name, pos) (fn completed => Keyword.dest_commands keywords |> filter completed |> sort_strings |> map (fn a => (a, (Markup.commandN, a)))); - val report = Markup.markup_report (Completion.reported_text completion); - in error ("Bad command " ^ quote name ^ Position.here pos ^ report) end + in error ("Bad command " ^ quote name ^ Position.here pos ^ completion_report) end end; diff -r 4c3704ecb0e6 -r bf6937af7fe8 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Nov 12 14:02:33 2018 +0100 +++ b/src/Pure/Isar/proof_context.ML Mon Nov 12 15:14:12 2018 +0100 @@ -450,8 +450,8 @@ val name = Type.cert_class tsig (Name_Space.intern class_space xname) handle TYPE (msg, _, _) => error (msg ^ Position.here pos ^ - Markup.markup_report (Completion.reported_text - (Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos)))); + Completion.markup_report + [Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos)]); val reports = if Context_Position.is_reported ctxt pos then [(pos, Name_Space.markup class_space name)] else []; @@ -535,10 +535,8 @@ fun consts_completion_message ctxt (c, ps) = ps |> map (fn pos => - Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos) - |> Completion.reported_text) - |> implode - |> Markup.markup_report; + Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos)) + |> Completion.markup_report; fun check_const {proper, strict} ctxt (c, ps) = let diff -r 4c3704ecb0e6 -r bf6937af7fe8 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Mon Nov 12 14:02:33 2018 +0100 +++ b/src/Pure/PIDE/resources.ML Mon Nov 12 15:14:12 2018 +0100 @@ -90,15 +90,15 @@ SOME entry => (Context_Position.report ctxt pos (markup name entry); name) | NONE => let - val completion = - Completion.make (name, pos) (fn completed => + val completion_report = + Completion.make_report (name, pos) + (fn completed => entries |> map #1 |> filter completed |> sort_strings |> map (fn a => (a, (kind, a)))); - val report = Markup.markup_report (Completion.reported_text completion); - in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end) + in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end) end; fun markup_session name {pos, serial} = diff -r 4c3704ecb0e6 -r bf6937af7fe8 src/Pure/Tools/jedit.ML --- a/src/Pure/Tools/jedit.ML Mon Nov 12 14:02:33 2018 +0100 +++ b/src/Pure/Tools/jedit.ML Mon Nov 12 15:14:12 2018 +0100 @@ -63,15 +63,14 @@ in writeln (msg ^ Position.here pos); name end else let - val completion = - Completion.make (name, pos) + val completion_report = + Completion.make_report (name, pos) (fn completed => Lazy.force all_actions |> filter completed |> sort_strings |> map (fn a => (a, ("action", a)))); - val report = Markup.markup_report (Completion.reported_text completion); - in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ report) end + in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ completion_report) end val _ = Theory.setup diff -r 4c3704ecb0e6 -r bf6937af7fe8 src/Pure/Tools/named_theorems.ML --- a/src/Pure/Tools/named_theorems.ML Mon Nov 12 14:02:33 2018 +0100 +++ b/src/Pure/Tools/named_theorems.ML Mon Nov 12 15:14:12 2018 +0100 @@ -77,10 +77,7 @@ let val space = Facts.space_of (Proof_Context.facts_of ctxt); val completion = Name_Space.completion context space (defined_entry context) (xname, pos); - in - error (undeclared xname ^ Position.here pos ^ - Markup.markup_report (Completion.reported_text completion)) - end; + in error (undeclared xname ^ Position.here pos ^ Completion.markup_report [completion]) end; in (case try (Proof_Context.get_fact_generic context) fact_ref of SOME (SOME name, _) => if defined_entry context name then name else err () diff -r 4c3704ecb0e6 -r bf6937af7fe8 src/Pure/theory.ML --- a/src/Pure/theory.ML Mon Nov 12 14:02:33 2018 +0100 +++ b/src/Pure/theory.ML Mon Nov 12 15:14:12 2018 +0100 @@ -139,15 +139,14 @@ Context.get_theory long thy name handle ERROR msg => let - val completion = - Completion.make (name, pos) + val completion_report = + Completion.make_report (name, pos) (fn completed => map (Context.theory_name' long) (ancestors_of thy) |> filter (completed o Long_Name.base_name) |> sort_strings |> map (fn a => (a, (Markup.theoryN, a)))); - val report = Markup.markup_report (Completion.reported_text completion); - in error (msg ^ Position.here pos ^ report) end; + in error (msg ^ Position.here pos ^ completion_report) end; val _ = Context_Position.report ctxt pos (get_markup thy'); in thy' end; diff -r 4c3704ecb0e6 -r bf6937af7fe8 src/Tools/Haskell/Completion.hs --- a/src/Tools/Haskell/Completion.hs Mon Nov 12 14:02:33 2018 +0100 +++ b/src/Tools/Haskell/Completion.hs Mon Nov 12 15:14:12 2018 +0100 @@ -9,8 +9,9 @@ See also "$ISABELLE_HOME/src/Pure/General/completion.ML". -} -module Isabelle.Completion (Name, T, names, none, make, encode, reported_text) -where +module Isabelle.Completion ( + Name, T, names, none, make, markup_element, markup_report, make_report + ) where import qualified Data.List as List @@ -37,15 +38,26 @@ then names limit props (make_names $ List.isPrefixOf $ clean_name name) else none -encode :: T -> XML.Body -encode (Completion _ total names) = - Encode.pair Encode.int - (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string))) - (total, names) +markup_element :: T -> (Markup.T, XML.Body) +markup_element (Completion props total names) = + if not (null names) then + let + markup = Markup.properties props Markup.completion + body = + Encode.pair Encode.int + (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string))) + (total, names) + in (markup, body) + else (Markup.empty, []) -reported_text :: T -> String -reported_text completion@(Completion props total names) = - if not (null names) then - let markup = Markup.properties props Markup.completion - in YXML.string_of $ XML.Elem markup (encode completion) - else "" +markup_report :: [T] -> String +markup_report [] = "" +markup_report elems = + elems + |> map (markup_element #> uncurry XML.Elem) + |> XML.Elem Markup.report + |> YXML.string_of + +make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String +make_report limit name_props make_names = + markup_report [make limit name_props make_names] diff -r 4c3704ecb0e6 -r bf6937af7fe8 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Mon Nov 12 14:02:33 2018 +0100 +++ b/src/Tools/Haskell/Haskell.thy Mon Nov 12 15:14:12 2018 +0100 @@ -550,8 +550,9 @@ See also \<^file>\$ISABELLE_HOME/src/Pure/General/completion.ML\. -} -module Isabelle.Completion (Name, T, names, none, make, encode, reported_text) -where +module Isabelle.Completion ( + Name, T, names, none, make, markup_element, markup_report, make_report + ) where import qualified Data.List as List @@ -578,18 +579,29 @@ then names limit props (make_names $ List.isPrefixOf $ clean_name name) else none -encode :: T -> XML.Body -encode (Completion _ total names) = - Encode.pair Encode.int - (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string))) - (total, names) +markup_element :: T -> (Markup.T, XML.Body) +markup_element (Completion props total names) = + if not (null names) then + let + markup = Markup.properties props Markup.completion + body = + Encode.pair Encode.int + (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string))) + (total, names) + in (markup, body) + else (Markup.empty, []) -reported_text :: T -> String -reported_text completion@(Completion props total names) = - if not (null names) then - let markup = Markup.properties props Markup.completion - in YXML.string_of $ XML.Elem markup (encode completion) - else "" +markup_report :: [T] -> String +markup_report [] = "" +markup_report elems = + elems + |> map (markup_element #> uncurry XML.Elem) + |> XML.Elem Markup.report + |> YXML.string_of + +make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String +make_report limit name_props make_names = + markup_report [make limit name_props make_names] \ generate_haskell_file "File.hs" = \