author | wenzelm |
Thu, 22 Nov 2018 17:34:30 +0100 | |
changeset 69327 | 264b44dce6be |
parent 69289 | bf6937af7fe8 |
child 69347 | 54b95d2ec040 |
permissions | -rw-r--r-- |
59720 | 1 |
(* Title: Pure/General/completion.ML |
55672 | 2 |
Author: Makarius |
3 |
||
55674 | 4 |
Semantic completion within the formal context. |
55672 | 5 |
*) |
6 |
||
7 |
signature COMPLETION = |
|
8 |
sig |
|
69289 | 9 |
type name = string * (string * string) |
55687 | 10 |
type T |
69289 | 11 |
val names: Position.T -> name list -> T |
55672 | 12 |
val none: T |
69289 | 13 |
val make: string * Position.T -> ((string -> bool) -> name list) -> T |
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
14 |
val encode: T -> XML.body |
69289 | 15 |
val markup_element: T -> Markup.T * XML.body |
16 |
val markup_report: T list -> string |
|
17 |
val make_report: string * Position.T -> ((string -> bool) -> name list) -> string |
|
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
18 |
val suppress_abbrevs: string -> Markup.T list |
67208 | 19 |
val check_option: Options.T -> Proof.context -> string * Position.T -> string |
20 |
val check_option_value: |
|
21 |
Proof.context -> string * Position.T -> string * Position.T -> Options.T -> string * Options.T |
|
55672 | 22 |
end; |
23 |
||
24 |
structure Completion: COMPLETION = |
|
25 |
struct |
|
26 |
||
59812 | 27 |
(* completion of names *) |
28 |
||
69289 | 29 |
type name = string * (string * string); (*external name, kind, internal name*) |
30 |
||
31 |
abstype T = Completion of {pos: Position.T, total: int, names: name list} |
|
55687 | 32 |
with |
55672 | 33 |
|
55687 | 34 |
fun dest (Completion args) = args; |
55672 | 35 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
36 |
fun names pos names = |
55687 | 37 |
Completion |
38 |
{pos = pos, |
|
39 |
total = length names, |
|
40 |
names = take (Options.default_int "completion_limit") names}; |
|
55672 | 41 |
|
42 |
end; |
|
55687 | 43 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
44 |
val none = names Position.none []; |
55687 | 45 |
|
59812 | 46 |
fun make (name, pos) make_names = |
47 |
if Position.is_reported pos andalso name <> "" andalso name <> "_" |
|
48 |
then names pos (make_names (String.isPrefix (Name.clean name))) |
|
49 |
else none; |
|
50 |
||
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
51 |
fun encode completion = |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
52 |
let |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
53 |
val {total, names, ...} = dest completion; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
54 |
open XML.Encode; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
55 |
in pair int (list (pair string (pair string string))) (total, names) end; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
56 |
|
69289 | 57 |
fun markup_element completion = |
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
58 |
let val {pos, names, ...} = dest completion in |
55687 | 59 |
if Position.is_reported pos andalso not (null names) then |
69289 | 60 |
(Position.markup pos Markup.completion, encode completion) |
61 |
else (Markup.empty, []) |
|
55687 | 62 |
end; |
63 |
||
69289 | 64 |
val markup_report = |
65 |
map (markup_element #> XML.Elem) #> YXML.string_of_body #> Markup.markup_report; |
|
66 |
||
67 |
val make_report = markup_report oo (single oo make); |
|
68 |
||
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
69 |
|
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
70 |
(* suppress short abbreviations *) |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
71 |
|
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
72 |
fun suppress_abbrevs s = |
55917
5438ed05e1c9
special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents:
55915
diff
changeset
|
73 |
if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) <= 1 orelse s = "::") |
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
74 |
then [Markup.no_completion] |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
75 |
else []; |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
76 |
|
67208 | 77 |
|
78 |
(* system options *) |
|
79 |
||
80 |
fun check_option options ctxt (name, pos) = |
|
81 |
let |
|
82 |
val markup = |
|
83 |
Options.markup options (name, pos) handle ERROR msg => |
|
84 |
let |
|
69289 | 85 |
val completion_report = |
86 |
make_report (name, pos) (fn completed => |
|
67208 | 87 |
Options.names options |
88 |
|> filter completed |
|
89 |
|> map (fn a => (a, ("system_option", a)))); |
|
69289 | 90 |
in error (msg ^ completion_report) end; |
67208 | 91 |
val _ = Context_Position.report ctxt pos markup; |
92 |
in name end; |
|
93 |
||
94 |
fun check_option_value ctxt (name, pos) (value, pos') options = |
|
95 |
let |
|
96 |
val _ = check_option options ctxt (name, pos); |
|
97 |
val options' = |
|
98 |
Options.update name value options |
|
99 |
handle ERROR msg => error (msg ^ Position.here pos'); |
|
100 |
in (name, options') end; |
|
101 |
||
55687 | 102 |
end; |