diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-10-12 12:21:54 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-10-12 12:21:54 -0400 |
| commit | 19b9eee2a968e9fe577792a48d0b4cf931165874 (patch) | |
| tree | 62139cb8c7c3aa9f402a76b19a206cef58cad0d1 /src | |
| parent | eb45f499c2e18f154ad59d75cf29c3903af5c725 (diff) | |
Basis and Top syntax-highlight, indent, parse, and type-check
Diffstat (limited to 'src')
| -rw-r--r-- | src/urweb.grm | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/urweb.grm b/src/urweb.grm index 3c270100..1879b241 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -714,13 +714,6 @@ earg : SYMBOL kcolon kind (fn (e, t) => ((EAbs ("_", SOME cexp, e), loc), (TFun (cexp, t), loc)) end) - | cterm TWIDDLE cterm (fn (e, t) => - let - val loc = s (cterm1left, cterm2right) - in - ((EDisjoint (cterm1, cterm2, e), loc), - (CDisjoint (cterm1, cterm2, t), loc)) - end) | eargp (eargp) eargp : SYMBOL (fn (e, t) => @@ -773,6 +766,13 @@ eargp : SYMBOL (fn (e, t) => ((EDisjoint (cterm1, cterm2, e), loc), (CDisjoint (cterm1, cterm2, t), loc)) end) + | LBRACK cterm TWIDDLE cterm RBRACK(fn (e, t) => + let + val loc = s (LBRACKleft, RBRACKright) + in + ((EDisjoint (cterm1, cterm2, e), loc), + (CDisjoint (cterm1, cterm2, t), loc)) + end) eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) | LPAREN etuple RPAREN (let |