Mercurial > urweb

comparison src/elaborate.sml @ 1048:38411c2cd363

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hint about disallowed attributes
author Adam Chlipala <adamc@hcoop.net>
date Wed, 25 Nov 2009 09:48:23 -0500
parents 6bcc1020d5cd
children 26197c957ad6
comparison
equal deleted inserted replaced
1047:609ab3947a08 1048:38411c2cd363
4015 case (gs, solved) of 4015 case (gs, solved) of
4016 ([], _) => () 4016 ([], _) => ()
4017 | (_, true) => (oneSummaryRound (); solver gs) 4017 | (_, true) => (oneSummaryRound (); solver gs)
4018 | _ => 4018 | _ =>
4019 app (fn Disjoint (loc, env, denv, c1, c2) => 4019 app (fn Disjoint (loc, env, denv, c1, c2) =>
4020 ((ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; 4020 let
4021 eprefaces' [("Con 1", p_con env c1), 4021 val c1' = ElabOps.hnormCon env c1
4022 ("Con 2", p_con env c2), 4022 val c2' = ElabOps.hnormCon env c2
4023 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), 4023
4024 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) 4024 fun isUnif (c, _) =
4025 case c of
4026 L'.CUnif _ => true
4027 | _ => false
4028
4029 fun maybeAttr (c, _) =
4030 case c of
4031 L'.CRecord ((L'.KType, _), xts) => true
4032 | _ => false
4033 in
4034 ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
4035 eprefaces' [("Con 1", p_con env c1),
4036 ("Con 2", p_con env c2),
4037 ("Hnormed 1", p_con env c1'),
4038 ("Hnormed 2", p_con env c2')];
4039
4040 if (isUnif c1' andalso maybeAttr c2')
4041 orelse (isUnif c2' andalso maybeAttr c1') then
4042 TextIO.output (TextIO.stdErr,
4043 "You may be using a disallowed attribute with an HTML tag.\n")
4044 else
4045 ()
4046 end
4025 | TypeClass (env, c, r, loc) => 4047 | TypeClass (env, c, r, loc) =>
4026 expError env (Unresolvable (loc, c))) 4048 expError env (Unresolvable (loc, c)))
4027 gs 4049 gs
4028 end 4050 end
4029 in 4051 in