summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-09-22 09:51:06 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-09-22 09:51:06 -0400
commit8d4e456a56e3cf84589df3f8dd7181550200587f (patch)
treef61d0476f2adf87c506fb62e82154b6e4f4609d2 /src
parent74093a2f38e25a13378ca2a3cc8c2fae4c6f37de (diff)
Resugar tag names before printing parse errors
Diffstat (limited to 'src')
-rw-r--r--src/urweb.grm9
1 files changed, 7 insertions, 2 deletions
diff --git a/src/urweb.grm b/src/urweb.grm
index 7a4d143f..db99d3b5 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -1397,6 +1397,11 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata", Infer)
end)
| tag GT xmlOpt END_TAG (let
+ fun tagOut s =
+ case s of
+ "tabl" => "table"
+ | _ => s
+
val pos = s (tagleft, GTright)
val et = tagIn END_TAG
in
@@ -1423,9 +1428,9 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata", Infer)
()
else
ErrorMsg.errorAt pos ("Begin tag <"
- ^ #1 (#1 tag)
+ ^ tagOut (#1 (#1 tag))
^ "> and end tag </"
- ^ et
+ ^ tagOut et
^ "> don't match.");
(EWild, pos))
end)