summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-11-25 09:48:23 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-11-25 09:48:23 -0500
commit68e0439b741bf84508f90b42611d681ced933874 (patch)
treeb30db3385f35000cd8cd74718be5c3ce815c0147 /src/elaborate.sml
parent44367f408f2b8dd52f780426920e0d196cc52eb2 (diff)
Hint about disallowed attributes
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml32
1 files changed, 27 insertions, 5 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index ec742ce7..eccc4840 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -4017,11 +4017,33 @@ fun elabFile basis topStr topSgn env file =
| (_, true) => (oneSummaryRound (); solver gs)
| _ =>
app (fn Disjoint (loc, env, denv, c1, c2) =>
- ((ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
- eprefaces' [("Con 1", p_con env c1),
- ("Con 2", p_con env c2),
- ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
- ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
+ let
+ val c1' = ElabOps.hnormCon env c1
+ val c2' = ElabOps.hnormCon env c2
+
+ fun isUnif (c, _) =
+ case c of
+ L'.CUnif _ => true
+ | _ => false
+
+ fun maybeAttr (c, _) =
+ case c of
+ L'.CRecord ((L'.KType, _), xts) => true
+ | _ => false
+ in
+ ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
+ eprefaces' [("Con 1", p_con env c1),
+ ("Con 2", p_con env c2),
+ ("Hnormed 1", p_con env c1'),
+ ("Hnormed 2", p_con env c2')];
+
+ if (isUnif c1' andalso maybeAttr c2')
+ orelse (isUnif c2' andalso maybeAttr c1') then
+ TextIO.output (TextIO.stdErr,
+ "You may be using a disallowed attribute with an HTML tag.\n")
+ else
+ ()
+ end
| TypeClass (env, c, r, loc) =>
expError env (Unresolvable (loc, c)))
gs