author | wenzelm |
Sun, 02 Oct 2016 21:05:14 +0200 | |
changeset 63999 | 5649a993666d |
parent 60731 | 4ac4b314d93c |
child 67208 | 16519cd83ed4 |
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 |
|
55687 | 9 |
type T |
55977 | 10 |
val names: Position.T -> (string * (string * string)) list -> T |
55672 | 11 |
val none: T |
59812 | 12 |
val make: string * Position.T -> ((string -> bool) -> (string * (string * string)) list) -> T |
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
13 |
val encode: T -> XML.body |
55840
2982d233d798
consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents:
55694
diff
changeset
|
14 |
val reported_text: T -> string |
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
15 |
val suppress_abbrevs: string -> Markup.T list |
55672 | 16 |
end; |
17 |
||
18 |
structure Completion: COMPLETION = |
|
19 |
struct |
|
20 |
||
59812 | 21 |
(* completion of names *) |
22 |
||
55977 | 23 |
abstype T = |
24 |
Completion of {pos: Position.T, total: int, names: (string * (string * string)) list} |
|
55687 | 25 |
with |
55672 | 26 |
|
55687 | 27 |
fun dest (Completion args) = args; |
55672 | 28 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
29 |
fun names pos names = |
55687 | 30 |
Completion |
31 |
{pos = pos, |
|
32 |
total = length names, |
|
33 |
names = take (Options.default_int "completion_limit") names}; |
|
55672 | 34 |
|
35 |
end; |
|
55687 | 36 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
37 |
val none = names Position.none []; |
55687 | 38 |
|
59812 | 39 |
fun make (name, pos) make_names = |
40 |
if Position.is_reported pos andalso name <> "" andalso name <> "_" |
|
41 |
then names pos (make_names (String.isPrefix (Name.clean name))) |
|
42 |
else none; |
|
43 |
||
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
44 |
fun encode completion = |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
45 |
let |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
46 |
val {total, names, ...} = dest completion; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
47 |
open XML.Encode; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
48 |
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
|
49 |
|
55840
2982d233d798
consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents:
55694
diff
changeset
|
50 |
fun reported_text completion = |
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
51 |
let val {pos, names, ...} = dest completion in |
55687 | 52 |
if Position.is_reported pos andalso not (null names) then |
53 |
let |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
54 |
val markup = Position.markup pos Markup.completion; |
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
59812
diff
changeset
|
55 |
in YXML.string_of (XML.Elem (markup, encode completion)) end |
55840
2982d233d798
consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents:
55694
diff
changeset
|
56 |
else "" |
55687 | 57 |
end; |
58 |
||
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
59 |
|
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
60 |
(* suppress short abbreviations *) |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
61 |
|
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
62 |
fun suppress_abbrevs s = |
55917
5438ed05e1c9
special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents:
55915
diff
changeset
|
63 |
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
|
64 |
then [Markup.no_completion] |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
65 |
else []; |
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents:
55840
diff
changeset
|
66 |
|
55687 | 67 |
end; |