author | wenzelm |
Sun, 02 Mar 2014 20:34:11 +0100 | |
changeset 55840 | 2982d233d798 |
parent 55694 | a1184dfb8e00 |
child 55915 | 607948c90bf0 |
permissions | -rw-r--r-- |
55672 | 1 |
(* Title: Pure/Isar/completion.ML |
2 |
Author: Makarius |
|
3 |
||
55674 | 4 |
Semantic completion within the formal context. |
55672 | 5 |
*) |
6 |
||
7 |
signature COMPLETION = |
|
8 |
sig |
|
55687 | 9 |
type T |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
10 |
val names: Position.T -> (string * string) list -> T |
55672 | 11 |
val none: T |
55840
2982d233d798
consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents:
55694
diff
changeset
|
12 |
val reported_text: T -> string |
55687 | 13 |
val report: T -> unit |
55672 | 14 |
end; |
15 |
||
16 |
structure Completion: COMPLETION = |
|
17 |
struct |
|
18 |
||
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
19 |
abstype T = Completion of {pos: Position.T, total: int, names: (string * string) list} |
55687 | 20 |
with |
55672 | 21 |
|
55687 | 22 |
fun dest (Completion args) = args; |
55672 | 23 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
24 |
fun names pos names = |
55687 | 25 |
Completion |
26 |
{pos = pos, |
|
27 |
total = length names, |
|
28 |
names = take (Options.default_int "completion_limit") names}; |
|
55672 | 29 |
|
30 |
end; |
|
55687 | 31 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
32 |
val none = names Position.none []; |
55687 | 33 |
|
55840
2982d233d798
consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents:
55694
diff
changeset
|
34 |
fun reported_text completion = |
55687 | 35 |
let val {pos, total, names} = dest completion in |
36 |
if Position.is_reported pos andalso not (null names) then |
|
37 |
let |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
38 |
val markup = Position.markup pos Markup.completion; |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
39 |
val body = (total, names) |> |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
40 |
let open XML.Encode in pair int (list (pair string string)) end; |
55840
2982d233d798
consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents:
55694
diff
changeset
|
41 |
in YXML.string_of (XML.Elem (markup, body)) end |
2982d233d798
consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents:
55694
diff
changeset
|
42 |
else "" |
55687 | 43 |
end; |
44 |
||
55840
2982d233d798
consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents:
55694
diff
changeset
|
45 |
val report = Output.report o reported_text; |
2982d233d798
consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents:
55694
diff
changeset
|
46 |
|
55687 | 47 |
end; |