--- 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;
--- 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) =
--- 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;
--- 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
--- 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} =
--- 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
--- 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 ()
--- 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;
--- 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]
--- 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>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>.
-}
-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]
\<close>
generate_haskell_file "File.hs" = \<open>