update the WhyML section in the manual

doc/expr.bnf

@@ -22,15 +22,15 @@
        | "raise" uqualid                          ; exception raising
        | "raise" "(" uqualid expr ")"             ;
        | "try" expr "with" ("|" handler)+ "end"   ; exception catching
-       | "any" type-c                             ; 
+       | "any" type-c                             ;
        | "let" pattern "=" expr "in" expr         ; local binding
        | "match" expr ("," expr)* "with"          ; pattern matching
          ("|" expr-case)+ "end"                   ;
        | "(" expr ("," expr)+ ")"                 ; tuple
-       | "{|" field-value+ "|}"                   ; record
+       | "{" field-value+ "}"                     ; record
        | expr "." lqualid                         ; field access
        | expr "." lqualid "<-" expr               ; field assignment
-       | "{|" expr "with" field-value+ "|}"       ; field update
+       | "{" expr "with" field-value+ "}"         ; field update
        | expr ":" type 	                          ; cast
        | label expr 	                          ; label
        | "'" uident ":" expr                      ; code mark

doc/macros.tex

@@ -57,7 +57,8 @@
 morekeywords={namespace,predicate,function,inductive,type,use,clone,%
 import,export,theory,module,end,in,with,%
 let,rec,for,to,do,done,match,if,then,else,while,try,invariant,variant,%
-absurd,raise,assert,exception,%
+absurd,raise,assert,exception,private,abstract,mutable,ghost,%
+downto,raises,writes,reads,requires,ensures,returns,val,model,%
 goal,axiom,lemma,forall},%
 string=[b]",%
 sensitive=true,%

doc/module.bnf

@@ -18,8 +18,8 @@
   mtype-defn ::=                                    ; abstract type
     | "=" type                                      ; alias type
     | "=" "|"? type-case ("|" type-case)*           ; algebraic type
-    | "=" "{|" mrecord-field                        ; record type
-          (";" mrecord-field)* "|}"                 ;
+    | "=" "{" mrecord-field                         ; record type
+          (";" mrecord-field)* "}"                  ;
   \
   mrecord-field ::= "mutable"? lident label* ":" type
   \

doc/term.bnf

@@ -10,23 +10,23 @@
        | lqualid term+ 		  ; function application
        | "if" formula "then" term ;
          "else" term              ; conditional
-       | "let" pattern "=" term "in" term 
+       | "let" pattern "=" term "in" term
                                   ; local binding
        | "match" term ("," term)* "with" ;
          ("|" term-case)+ "end"          ; pattern matching
        | "(" term ("," term)+ ")" ; tuple
-       | "{|" field-value+ "|}"   ; record
+       | "{" field-value+ "}"     ; record
        | term "." lqualid         ; field access
-       | "{|" term "with" field-value+ "|}"    ; field update
+       | "{" term "with" field-value+ "}"      ; field update
        | term ":" type 	          ; cast
        | label term 	      	  ; label
        | "'" uident    	      	  ; code mark
        | "(" term ")" 	      	  ; parentheses
   \
-  term-case ::= pattern "->" term ; 
+  term-case ::= pattern "->" term ;
   \
   pattern ::= pattern "|" pattern ; or pattern
-            | pattern "," pattern ; tuple 
+            | pattern "," pattern ; tuple
 	    | "_"                 ; catch-all
 	    | lident              ; variable
 	    | uident pattern*     ; constructor

doc/theory2.bnf

@@ -2,7 +2,7 @@
   type-defn ::=                                      ; abstract type
     | "=" type                                       ; alias type
     | "=" "|"? type-case ("|" type-case)*            ; algebraic type
-    | "=" "{|" record-field (";" record-field)* "|}" ; record type
+    | "=" "{" record-field (";" record-field)* "}"   ; record type
   \
   type-case ::= uident label* type-param*
   \