summaryrefslogtreecommitdiff
path: root/src/getinfo.sig
diff options
context:
space:
mode:
authorGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-11 22:56:29 +0100
committerGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 11:46:57 +0100
commit9b00dc724363ac7b0a31687f14cc3bb2f2460f9b (patch)
tree8a078a63394a2a6067c35324796fe32deb0f5438 /src/getinfo.sig
parent25b0685cefe772c73562665a4cc8d2d40e5ff600 (diff)
Integrated getInfo into LSP
Diffstat (limited to 'src/getinfo.sig')
-rw-r--r--src/getinfo.sig7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/getinfo.sig b/src/getinfo.sig
index 317b7e79..334e19f1 100644
--- a/src/getinfo.sig
+++ b/src/getinfo.sig
@@ -26,6 +26,11 @@
*)
signature GET_INFO = sig
- val getInfo: string (* file:row:col *) -> Print.PD.pp_desc
+ val getInfo:
+ ElabEnv.env ->
+ Elab.str' ->
+ string (* fileName *) ->
+ { line: int , character: int} ->
+ Print.PD.pp_desc
end