summaryrefslogtreecommitdiff
path: root/src/interactive.mli
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-12-22 00:20:08 +0000
committerAlasdair Armstrong2018-12-22 00:20:08 +0000
commit0a65347ed2868b815dee532acfebb463f8be644b (patch)
tree662b9fb1b240984597b3050fe4c174ccfceecd0f /src/interactive.mli
parentc745a9a8d8d7d2b04e72bbb8bda9d9f0a7aabbfb (diff)
Improve error messages and debugging
Work on improving the formatting and quality of error messages When sail is invoked with sail -i, any type errors now drop the user down to the interactive prompt, with the interactive environment being the environment at the point the type error occurred, this means the typechecker state can be interactively queried in the interpreter to help diagnose type errors.
Diffstat (limited to 'src/interactive.mli')
-rw-r--r--src/interactive.mli9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/interactive.mli b/src/interactive.mli
new file mode 100644
index 00000000..7782f646
--- /dev/null
+++ b/src/interactive.mli
@@ -0,0 +1,9 @@
+open Ast
+open Type_check
+
+val opt_interactive : bool ref
+val opt_suppress_banner : bool ref
+
+val ast : tannot defs ref
+
+val env : Env.t ref