summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-09-16 15:34:50 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2010-09-16 15:34:50 -0400
commit10abf930df47a214ef2d66a6727c9e159093bc57 (patch)
tree2bedd5ddfc79ccad67baf651ef94e9c78ccdbc8f
parente0f7a1d2e4ed4d0a264f042de8698fe98bc3b88c (diff)
Fix typing of cut operators; fix lexing of XML comments
-rw-r--r--src/elaborate.sml2
-rw-r--r--src/urweb.lex2
2 files changed, 3 insertions, 1 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index e7848f21..e3f42c19 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1998,6 +1998,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val gs3 = D.prove env denv (first, rest, loc)
in
+ checkKind env c' ck kname;
((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc),
gs1 @ enD gs2 @ enD gs3)
end
@@ -2013,6 +2014,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
val gs3 = D.prove env denv (c', rest, loc)
in
+ checkKind env c' ck (L'.KRecord ktype, loc);
((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc),
gs1 @ enD gs2 @ enD gs3)
end
diff --git a/src/urweb.lex b/src/urweb.lex
index 27af5bdd..0ee09cad 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -172,7 +172,7 @@ cid = [A-Z][A-Za-z0-9_]*;
ws = [\ \t\012];
intconst = [0-9]+;
realconst = [0-9]+\.[0-9]*;
-notags = [^<{\n(]+;
+notags = ([^<{\n(]|(\([^\*]))+;
xcom = ([^\-]|(-[^\-]))+;
oint = [0-9][0-9][0-9];
xint = x[0-9a-fA-F][0-9a-fA-F];