summaryrefslogtreecommitdiff
path: root/src/getinfo.sig
diff options
context:
space:
mode:
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