Mercurial > urweb

comparison src/urweb.grm @ 356:383c72d11db8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Basis and Top syntax-highlight, indent, parse, and type-check
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Oct 2008 12:21:54 -0400
parents 527529a083d9
children c1e96b387115
comparison
equal deleted inserted replaced
355:fa2d25fe75ce 356:383c72d11db8
712 val loc = s (UNDERleft, cexpright) 712 val loc = s (UNDERleft, cexpright)
713 in 713 in
714 ((EAbs ("_", SOME cexp, e), loc), 714 ((EAbs ("_", SOME cexp, e), loc),
715 (TFun (cexp, t), loc)) 715 (TFun (cexp, t), loc))
716 end) 716 end)
717 | cterm TWIDDLE cterm (fn (e, t) =>
718 let
719 val loc = s (cterm1left, cterm2right)
720 in
721 ((EDisjoint (cterm1, cterm2, e), loc),
722 (CDisjoint (cterm1, cterm2, t), loc))
723 end)
724 | eargp (eargp) 717 | eargp (eargp)
725 718
726 eargp : SYMBOL (fn (e, t) => 719 eargp : SYMBOL (fn (e, t) =>
727 let 720 let
728 val loc = s (SYMBOLleft, SYMBOLright) 721 val loc = s (SYMBOLleft, SYMBOLright)
767 (TFun (cexp, t), loc)) 760 (TFun (cexp, t), loc))
768 end) 761 end)
769 | LPAREN cterm TWIDDLE cterm RPAREN(fn (e, t) => 762 | LPAREN cterm TWIDDLE cterm RPAREN(fn (e, t) =>
770 let 763 let
771 val loc = s (LPARENleft, RPARENright) 764 val loc = s (LPARENleft, RPARENright)
765 in
766 ((EDisjoint (cterm1, cterm2, e), loc),
767 (CDisjoint (cterm1, cterm2, t), loc))
768 end)
769 | LBRACK cterm TWIDDLE cterm RBRACK(fn (e, t) =>
770 let
771 val loc = s (LBRACKleft, RBRACKright)
772 in 772 in
773 ((EDisjoint (cterm1, cterm2, e), loc), 773 ((EDisjoint (cterm1, cterm2, e), loc),
774 (CDisjoint (cterm1, cterm2, t), loc)) 774 (CDisjoint (cterm1, cterm2, t), loc))
775 end) 775 end)
776 776