# HG changeset patch # User Adam Chlipala # Date 1259160503 18000 # Node ID 38411c2cd363490a81039fc438d5591c5c415484 # Parent 609ab3947a08410ec11b05845fadeee1205540e1 Hint about disallowed attributes diff -r 609ab3947a08 -r 38411c2cd363 src/elaborate.sml --- a/src/elaborate.sml Wed Nov 25 09:30:44 2009 -0500 +++ b/src/elaborate.sml Wed Nov 25 09:48:23 2009 -0500 @@ -4017,11 +4017,33 @@ | (_, 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 diff -r 609ab3947a08 -r 38411c2cd363 tests/vlad2.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/vlad2.ur Wed Nov 25 09:48:23 2009 -0500 @@ -0,0 +1,3 @@ +fun main () = return + +

123

diff -r 609ab3947a08 -r 38411c2cd363 tests/vlad2.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/vlad2.urp Wed Nov 25 09:48:23 2009 -0500 @@ -0,0 +1,2 @@ + +vlad2 diff -r 609ab3947a08 -r 38411c2cd363 tests/vlad2.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/vlad2.urs Wed Nov 25 09:48:23 2009 -0500 @@ -0,0 +1,1 @@ +val main : unit -> transaction page