diff --git a/doc/gf-modules.html b/doc/gf-modules.html
index ce6a5b41f..51aff0685 100644
--- a/doc/gf-modules.html
+++ b/doc/gf-modules.html
@@ -12,7 +12,7 @@
-8/4/2005
+8/4/2005 - 10/4
@@ -42,7 +42,7 @@ This document is meant as an appendix to the GF tutorial, and
presupposes knowledge of GF judgements and expressions. It aims
just to tell what module system adds to the old functionality;
some information is repeated to give understanding on how the
-module system related to the already familiar uses of GF grammars.
+module system relates to the already familiar uses of GF grammars.
@@ -758,7 +758,7 @@ the instances.
by non-compositional functions (transfer rules) between the
source and target languages. They are being introduce to GF as a module
type of its own, but their development is still in progress. What
-will be available are at least fun and def
+will be available are at least fun and def
judgements, but more is needed. It has not yet been defined how
transfer modules are integrated in multilingual grammars, i.e.\
where in the grammar it is specified what transfer to use.
@@ -771,7 +771,198 @@ has not been implemented.)
Summary of module syntax and semantics
+Abstract syntax modules
+Syntax:
+
+abstract A = (A_1,...,A_n **)?
+{J_1 ; ... ; J_m ; }
+
+
+
+where
+
+- i >= 0
+
- each A_i is itself an abstract module
+
- each J_i is a judgement of one of the forms
+ cat, fun, def, data
+
+Semantic conditions:
+
+- all names declared in each A_i and A must be distinct
+
+
+Concrete syntax modules
+
+Syntax:
+
+incomplete? concrete C of A =
+(C_1,...,C_n **)?
+(open O_1,...,O_k in)?
+{J_1 ; ... ; J_m ; }
+
+
+
+where
+
+- i >= 0
+
- A is an abstract module
+
- each C_i is a concrete module
+
- each O_i is an open specification, of one of the forms
+
+where R is a resource, instance, or concrete, and
+Q is any identifier
+
- each J_i is a judgement of one of the forms
+ lincat, lin, lindef, printname
+
+
+
+
+If the modifier incomplete appears, then any R in
+an open specification may also be an interface.
+
+
+
+Semantic conditions:
+
+- each cat judgement in A
+ must have a corresponding, unique
+ lincat judgement in C
+
- each fun judgement in A
+ must have a corresponding, unique
+ lin judgement in C
+
+
+
+Resource modules
+
+Syntax:
+
+resource R =
+(R_1,...,R_n **)?
+(open O_1,...,O_k in)?
+{J_1 ; ... ; J_m ; }
+
+
+where
+
+- i >= 0
+
- each R_i is a resource module
+
- each O_i is an open specification, of one of the forms
+
+where P is a resource, instance, or concrete, and
+Q is any identifier
+
- each J_i is a judgement of one of the forms
+ oper, param
+
+
+
+
+Semantic conditions:
+
+- all names declared in each R_i and R must be distinct
+
- all constants declared must have a definition
+
+
+
+Interface modules
+
+Syntax:
+
+interface R =
+(R_1,...,R_n **)?
+(open O_1,...,O_k in)?
+{J_1 ; ... ; J_m ; }
+
+
+where
+
+- i >= 0
+
- each R_i is an interface module
+
- each O_i is an open specification, of one of the forms
+
+where P is a resource, instance, or concrete, and
+Q is any identifier
+
- each J_i is a judgement of one of the forms
+ oper, param
+
+
+
+
+Semantic conditions:
+
+- all names declared in each R_i and R must be distinct
+
+
+
+
+Instance modules
+
+Syntax:
+
+instance R of I =
+(R_1,...,R_n **)?
+(open O_1,...,O_k in)?
+{J_1 ; ... ; J_m ; }
+
+
+where
+
+- i >= 0
+
- I is an interface module
+
- each R_i is an instance module
+
- each O_i is an open specification, of one of the forms
+
+where P is a resource, instance, or concrete, and
+Q is any identifier
+
- each J_i is a judgement of one of the forms
+ oper, param
+
+
+
+
+Semantic conditions:
+
+- all names declared in each R_i, I, and R must be distinct
+
- all constants declared in I must have a definition either in
+ I or R
+
+
+
+Instantiated concrete syntax modules
+
+Syntax:
+
+concrete C of A =
+(C_1,...,C_n **)?
+B
+with
+(I_1 =J_1), ...
+, (I_m =J_m) ;
+
+
+
+where
+
+- i >= 0
+
- A is an abstract module
+
- each C_i is a concrete module
+
- B is an incomplete concrete syntax of A
+
- each I_i is an interface
+
- each J_i is an instance of I_i
+