aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-05-05 12:58:13 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-05-05 12:58:13 -0400
commita424e0352aff3490a58d19de5ebf4a164bd03b65 (patch)
tree9cc3661046de89d0263f025bdbf935cce233811d /src/elaborate.sml
parentf2ae62f46ac8b9cefc841bd064c7ea8317cc9752 (diff)
-dumpTypesOnError
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index fe2e2f12..07a1d976 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -39,6 +39,7 @@
open ElabErr
val dumpTypes = ref false
+ val dumpTypesOnError = ref false
val unifyMore = ref false
val incremental = ref false
val verbose = ref false
@@ -4747,7 +4748,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
(*preface ("file", p_file env' file);*)
- if !dumpTypes then
+ if !dumpTypes orelse (!dumpTypesOnError andalso ErrorMsg.anyErrors ()) then
let
open L'
open Print.PD