summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-13 16:36:16 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-13 16:36:16 -0400
commit6698d60845b031a20fa7c91e8b4b8e8e326648ea (patch)
tree96714924f1004212784631e95cb38ee9f07962d8
parent27a53b9cda6c4e3e1732659fe44a7fb6bad03655 (diff)
More descriptive info flow error message
-rw-r--r--src/iflow.sml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/iflow.sml b/src/iflow.sml
index c8a8df89..d0fc0d80 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -1282,7 +1282,8 @@ fun buildable (e, loc) =
val (_, hs) = !hyps
in
ErrorMsg.errorAt loc "The information flow policy may be violated here.";
- Print.preface ("Hypotheses", Print.p_list p_atom hs)
+ Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs),
+ ("User learns", p_exp e)]
end)
end