summaryrefslogtreecommitdiff
path: root/src/getinfo.sig
diff options
context:
space:
mode:
authorGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-12 22:44:50 +0100
committerGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 11:46:57 +0100
commitfaff2d8ac927fd49f13fbaf9b84ffc99bbb6f9b8 (patch)
tree557c53bb80d4cbf286149504580886cd4259b3f2 /src/getinfo.sig
parent9b00dc724363ac7b0a31687f14cc3bb2f2460f9b (diff)
Added tracking of text of source files and autocomplete
Diffstat (limited to 'src/getinfo.sig')
-rw-r--r--src/getinfo.sig20
1 files changed, 19 insertions, 1 deletions
diff --git a/src/getinfo.sig b/src/getinfo.sig
index 334e19f1..50eee70a 100644
--- a/src/getinfo.sig
+++ b/src/getinfo.sig
@@ -26,11 +26,29 @@
*)
signature GET_INFO = sig
+
+ datatype item =
+ Kind of Elab.kind
+ | Con of Elab.con
+ | Exp of Elab.exp
+ | Sgn_item of Elab.sgn_item
+ | Sgn of Elab.sgn
+ | Str of Elab.str
+ | Decl of Elab.decl
+
val getInfo:
ElabEnv.env ->
Elab.str' ->
string (* fileName *) ->
{ line: int , character: int} ->
- Print.PD.pp_desc
+ { smallest : { span : ErrorMsg.span
+ , item : item
+ , env : ElabEnv.env }
+ , smallestgoodpart : { span : ErrorMsg.span
+ , desc : Print.PD.pp_desc
+ , env : ElabEnv.env
+ , item : item
+ } option
+}
end