author | wenzelm |
Sun, 23 Feb 2014 21:11:59 +0100 | |
changeset 55694 | a1184dfb8e00 |
parent 55687 | 78c83cd477c1 |
child 55840 | 2982d233d798 |
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 |
55687 | 12 |
val report: T -> unit |
55672 | 13 |
end; |
14 |
||
15 |
structure Completion: COMPLETION = |
|
16 |
struct |
|
17 |
||
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
18 |
abstype T = Completion of {pos: Position.T, total: int, names: (string * string) list} |
55687 | 19 |
with |
55672 | 20 |
|
55687 | 21 |
fun dest (Completion args) = args; |
55672 | 22 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
23 |
fun names pos names = |
55687 | 24 |
Completion |
25 |
{pos = pos, |
|
26 |
total = length names, |
|
27 |
names = take (Options.default_int "completion_limit") names}; |
|
55672 | 28 |
|
29 |
end; |
|
55687 | 30 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
31 |
val none = names Position.none []; |
55687 | 32 |
|
33 |
fun report completion = |
|
34 |
let val {pos, total, names} = dest completion in |
|
35 |
if Position.is_reported pos andalso not (null names) then |
|
36 |
let |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
37 |
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
|
38 |
val body = (total, names) |> |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
39 |
let open XML.Encode in pair int (list (pair string string)) end; |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
40 |
in Output.report (YXML.string_of (XML.Elem (markup, body))) end |
55687 | 41 |
else () |
42 |
end; |
|
43 |
||
44 |
end; |