*** empty log message ***

1 files changed, 266 insertions, 261 deletions

diff --git a/doc/reference/reference.verb.tex b/doc/reference/reference.verb.tex
index 03471656bf..fbd2cbdd57 100644
--- a/doc/reference/reference.verb.tex
+++ b/doc/reference/reference.verb.tex
@@ -446,7 +446,7 @@ definitions, as well as packages.
 \item
 \verb@C.super.x@ where \verb@C@ references a class and \verb@x@ references a 
 stable member of
-one of the base types of \verb@C@. 
+one of the base classes of \verb@C@. 
 The path \verb@super.x@ is taken as a shorthand for \verb@C.super.x@ where 
 \verb@C@ is the class directly enclosing the reference. 
 \end{itemize}
@@ -566,7 +566,7 @@ the following types are ill-formed:
 A compound type \verb@T$_1$ with ... with T$_n$ {R}@ represents
 objects with members as given in the component types $T_1 \commadots
 T_n$ and the refinement \verb@{R}@. Each component type $T_i$ must be a
-class type and the base type sequence generated by types $T_1
+class type and the base class sequence generated by types $T_1
 \commadots T_n$ must be well-formed (\sref{sec:basetypes-wf}). A
 refinement \verb@{R}@ contains declarations and type
 definitions. Each declaration or definition in a refinement must
@@ -613,7 +613,7 @@ do they appear explicitely in programs. They are introduced in this
 report as the internal types of defined identifiers.
 
 \subsection{Method Types}
-\label{sec:method-types}\todo{Change Syntax}
+\label{sec:method-types}
 
 A method type is denoted internally as $(ps)U$, where $(ps)$ is a
 parameter section $(x_1: T_1 \commadots x_n: T_n)$ for some $n \geq 0$
@@ -708,46 +708,47 @@ val f = 0
 \end{verbatim}
 define a function \verb@f@ which has type \verb@(x: T)T $\overload$ Int@.
 
-\section{Base Types and Member Definitions}
+\section{Base Classes and Member Definitions}
+\label{sec:base-classes}
 
-Types, bounds and base types of class members depend on the way the
+Types, bounds and base classes of class members depend on the way the
 members are referenced.  Central here are three notions, namely:
 \begin{enumerate}
-\item the notion of the base type sequence of a type $T$,
+\item the notion of the base class sequence of a type $T$,
 \item the notion of a type $T$ seen as a member of some class $C$ from some 
       prefix type $S$,
 \item the notion of a member binding of some type $T$.
 \end{enumerate}
 These notions are defined mutually recursively as follows.
 
-1. The {\em base type sequence} of a type is a sequence of class types, 
+1. The {\em base class sequence} of a type is a sequence of class types, 
 given as follows.
 \begin{itemize}
 \item
-The base types of a class type \verb@C@ are the base types of class
+The base classes of a class type \verb@C@ are the base classes of class
 \verb@C@.
 \item
-The base types of an aliased type are the base types of its alias.
+The base classes of an aliased type are the base classes of its alias.
 \item
-The base types of an abstract type are the base types of its upper bound.
+The base classes of an abstract type are the base classes of its upper bound.
 \item
-The base types of a parameterized type \verb@C[T$_1$, ..., T$_n$]@ are the base types
+The base classes of a parameterized type \verb@C[T$_1$, ..., T$_n$]@ are the base classes
 of type \verb@C@, where every occurrence of a type parameter $a_i$ 
 of \verb@C@ has been replaced by the corresponding parameter type $T_i$.
 \item
-The base types of a singleton type \verb@p.type@ are the base types of
+The base classes of a singleton type \verb@p.type@ are the base classes of
 the type of \verb@p@.
 \item
-The base types of a compound type
+The base classes of a compound type
 \verb@T$_1$ with ... with T$_n$ with {R}@ is the concatenation of the
-base types of all \verb@T$_i$@'s, except that later base types replace
-earlier base types which are instances of the same class.
+base classes of all \verb@T$_i$@'s, except that later base classes replace
+earlier base classes which are instances of the same class.
 \end{itemize}
 
 2. The notion of a type \verb@T@
 {\em seen as a member of some class \verb@C@ from some prefix type
 \verb@S@} makes sense only if the prefix type \verb@S@
-has a type instance of class \verb@C@ as a base type, say
+has a type instance of class \verb@C@ as a base class, say
 \verb@S' # C[T$_1$, ..., T$_n$]@. Then we define as follows.
 \begin{itemize}
  \item 
@@ -755,7 +756,7 @@ has a type instance of class \verb@C@ as a base type, say
  \item Otherwise, if \verb@T@ is the $i$'th type parameter of some class \verb@D@, then
    \begin{itemize}
    \item
-   If \verb@S@ has a base type \verb@D[U$_1$, ..., U$_n$]@, for some type parameters
+   If \verb@S@ has a base class \verb@D[U$_1$, ..., U$_n$]@, for some type parameters
    \verb@[U$_1$, ..., U$_n$]@, then \verb@T@ seen as a member of $C$ from $S$ is $U_i$.
    \item
    Otherwise, if $C$ is defined in a class $C'$, then
@@ -772,7 +773,7 @@ has a type instance of class \verb@C@ as a base type, say
    \begin{itemize}
    \item
    If \verb@D@ is a subclass of \verb@C@ and 
-   \verb@S@ has a type instance of class $D$ among its base types.
+   \verb@S@ has a type instance of class $D$ among its base classes.
    then \verb@T@ seen as a member of $C$ from $S$ is $S$.
    \item
    Otherwise, if $C$ is defined in a class $C'$, then
@@ -793,7 +794,7 @@ then we use ``\verb@T@ seen from \verb@S@'' as a shorthand for
 ``\verb@T@ seen as a member of $D$ from $S$.
 
 3. The {\em member bindings} of a type $T$ are all bindings $d$ such that
-there exists a type instance of some class $C$ among the base types of $T$
+there exists a type instance of some class $C$ among the base classes of $T$
 and there exists a definition or declaration $d'$ in $C$
 such that $d$ results from $d'$ by replacing every
 type $T'$ in $d'$ by $T'$ seen as a member of $C$ from $T$.
@@ -1437,7 +1438,7 @@ is equivalent to the block \verb@{ M.add(M.z, M.one) }@.
 \label{sec:globaldefs}
 
 \syntax\begin{verbatim}
-  ClsDef          \>::=\> ([case] class | trait) ClassDef {`,' ClassDef}
+  ClsDef          \=::=\= ([case] class | trait) ClassDef {`,' ClassDef}
                   \>  |\> [case] object ObjectDef {`,' ObjectDef}
 \end{verbatim}
 
@@ -1475,20 +1476,26 @@ members.
 %template must be equivalent to a type which does not refer to any
 %private members of that template.
 
-\paragraph{Connection with Java} 
+\paragraph{Connection with Java} A template may have a Java class as
+its superclass and Java interfaces as its mixin classes. On the other
+hand, it is not permitted to have a Java class as a mixin class, or a
+Java interface as a superclass.
 
 \subsection{Constructor Invocations}
 \label{sec:constr-invoke}
 \syntax\begin{verbatim}
-  Constr \=::= \= StableId [TypeArgs] {ArgumentExpr}
+  Constr \=::= \= StableId [TypeArgs] [`(' [Exprs] `)']  
 \end{verbatim}
 
 Constructor invocations define the type, members, and initial state of
 objects created by an instance creation expression, or of parts of an
 object's definition which are inherited by a class or module
-definition. A constructor invocation is a designator or function
-application whose function part is a stable identifier and whose type
-is a class constructor type \verb@class T@, for some type \verb@T@.
+definition. A constructor invocation is a function application 
+\verb@x.c(args)@, where \verb@x@ is a stable identifier
+\sref{sec:stable-ids}), \verb@c@ is a constructor name, and
+\verb@(args)@ is an argument list. The prefix \verb@x.@ can be
+omitted. The argument list \verb@(args)@ can also be omitted, in which
+case an empty argument list \verb@()@ is implicitly added.
 
 \subsection{Base Classes}
 \label{sec:base-classes}
@@ -1513,10 +1520,16 @@ base classes of the template represented by \verb@C@, followed by \verb@C@
 itself.  The base classes of a constructor invocation of type \verb@class T@
 are the base classes of \verb@T@.
 
-If two classes in the base class sequence of a template refer to the
-same class definition, then that definition must define an interface
-(\sref{sec:interfaces}), and both references must have the same
-qualifiers and parameters (if any).
+The notions of mixin base classes and base classes are extended from
+classes to arbitrary types following the definitions of
+\sref{sec:base-classes}.
+ 
+If two types in the base class sequence of a template refer to the
+same class definition, then that definition must define a trait
+(\sref{sec:traits}), and the type that comes later in the sequence must
+conform to the type that comes first. Furthermore, a base class
+sequence may not contain two different case classes
+\sref{sec:case-classes}.
 
 \subsection{Evaluation}
 
@@ -1583,6 +1596,7 @@ of a base class which succeeds \verb@b@ in the base class sequence of the
 template.
 \end{enumerate}
 
+\comment{
 The type of a member \verb@m@ is determined as follows: If \verb@m@ is defined
 in \verb@stats@, then its type is the type as given in the member's
 declaration or definition. Otherwise, if \verb@m@ is inherited from the
@@ -1619,13 +1633,14 @@ labelled \verb@qualified@, the qualified name is $M\qex x$. If $M$ is
 not labelled \verb@qualified@, the qualified name is $\epsilon\qex x$.
 \end{enumerate}
 }
+}
 
 \example Consider the class definitions
 
 \begin{verbatim}
-class A with { def f: Int = 1 ; def g: Int = 2 ; def h: Int = 3 }
-abstract class B with { def f: Int = 4 ; def g: Int }
-abstract class C extends A with B with { def h: Int }
+class A { def f: Int = 1 ; def g: Int = 2 ; def h: Int = 3 }
+abstract class B { def f: Int = 4 ; def g: Int }
+abstract class C extends A with B { def h: Int }
 \end{verbatim}
 
 Then class \verb@C@ has a directly bound abstract member \verb@h@. It
@@ -1649,282 +1664,157 @@ in addition to the members inherited from class \verb@Any@.
 \subsection{Overriding}
 \label{sec:overriding}
 
-A template member \verb@M$ that has the same \ifqualified{qualified} name as a
-non-private member \verb@M'$ of a base class (and that belongs to the same
-namespace) is said to {\em override} that member.  In this case the
-binding of the overriding member \verb@M$ must be more specific
-(\sref{sec:subtyping}) than the binding of the overridden member \verb@M'$.
-Furthermore, the overridden definition may not be a class or module
-definition or a type alias.  Method definitions may only override
-other method definitions (or the methods implicitly defined by a
-variable definition). They may not override value or let definitions.
-Finally, the following restrictions on modifiers apply to \verb@M$ and
-\verb@M'$:
+A template member
+\verb@M@ that has the same \ifqualified{qualified} 
+name as a non-private member \verb@M'@
+of a base class (and that belongs to the same namespace) is said to
+{\em override} that member.  In this case the binding of the
+overriding member
+\verb@M@ must be more specific (\sref{sec:subtyping}) than the 
+binding of the overridden member \verb@M'@.
+Furthermore, the overridden definition may not be a class or class
+constructor definition.  Method definitions may only override other
+method definitions (or the methods implicitly defined by a variable
+definition). They may not override value let definitions.  Finally,
+the following restrictions on modifiers apply to
+\verb@M@ and \verb@M'@:
 \begin{itemize}
 \item
-\verb@M$ must not be labelled \verb@private@.
+\verb@M'@ must not be labelled \verb@final@.
 \item
-If \verb@M'$ is not abstract, then \verb@M$ must be labelled \verb@override@.
+\verb@M@ must not be labelled \verb@private@.
 \item
-If \verb@M'$ is labelled \verb@protected@, then \verb@M$ must also be
+If \verb@M@ is labelled \verb@protected@, then \verb@M'@ must also be
 labelled \verb@protected@.
-\iffinaltype{
 \item
-\verb@M'$ may be labelled \verb@final@ only if it is an abstract type
-binding.
-}
+If \verb@M'@ is not an abstract member, then
+\verb@M@ must be labelled \verb@override@.
 \end{itemize}
 
 \example\label{ex:compound-a}
 Consider the definitions:
 \begin{verbatim}
-abstract class Root with { type T extends Root }
-abstract class A extends Root with { type T extends A }
-abstract class B extends Root with { type T extends B }
+trait Root with { type T <: Root }
+trait A extends Root with { type T <: A }
+trait B extends Root with { type T <: B }
+trait C extends A with B;
 \end{verbatim}
-Then the compound type \verb@A with B@ is not well-formed because the
-binding of \verb@T@ in \verb@A with B@ is
+Then the trait definition \verb@C@ is not well-formed because the
+binding of \verb@T@ in \verb@C@ is
 \verb@type T extends B@,
 which fails to be more specific than the binding of same name in type
-\verb@A@. The problem can be solved by adding a refinement
-(\sref{sec:refinements}) which further constrains
-\verb@T@. E.g., \verb@A with B with { type T extends A with B }@.
-%\begin{verbatim}
-%A with B with { type T extends A with B }
-%\end{verbatim}
+\verb@A@. The problem can be solved by adding an overriding 
+definition of type \verb@T@ in class \verb@C@:
+\begin{verbatim}
+class C extends A with B { type T <: C }
+\end{verbatim}
 
 \subsection{Modifiers}
 \label{sec:modifiers}
 
 \syntax\begin{verbatim}
-  Modifier       \=::= \= final
-		 \>  | \> private
-		 \>  | \> protected
-		 \>  | \> override [Qualid]
-	         \>  |\> abstract
-\end{verbatim}
-
-Member definitions may be preceded by modifiers which
-affect the \ifqualified{qualified names, }accessibility and usage of the identifiers
-bound by them.  If several modifiers are given, their order does not
-matter, but the same modifier may not occur repeatedly.  Modifiers
-preceding a repeated definition apply to all constituent definitions.
-The rules governing the validity and meaning of a modifier are as
-follows.
-\begin{itemize}
-\item
-The \verb@abstract@ modifier is used in class definitions. It is
-mandatory if the class has abstract members.  Classes with
-\verb@abstract@ members cannot be instantiated
-(\sref{sec:inst-creation}) with a constructor invocation unless
-followed by mixin constructors or statements which override all
-abstract members of the class.
-\item
-The \verb@final@ modifier applies to class member definitions and to
-class definitions. A \verb@final@ function, value, or variable may not
-be overridden in subclasses.  A
-\verb@final@ class may
-not be used as superclass or mixin class in a class definition or
-instance creation expression.
-Excepted from this rule are only
+  Modifier            \=::=\= LocalModifier
+		  \>  |\> private
+                  \>  |\> protected
+                  \>  |\> override 
+  LocalModifier   \>::=\> abstract
+                  \>  |\> final
+		  \>  |\> sealed
+\end{verbatim}
+
+Member definitions may be preceded by modifiers which affect the
+\ifqualified{qualified names, }accessibility and usage of the
+identifiers bound by them.  If several modifiers are given, their
+order does not matter, but the same modifier may not occur repeatedly.
+Modifiers preceding a repeated definition apply to all constituent
+definitions.  The rules governing the validity and meaning of a
+modifier are as follows.
 \begin{itemize}
-\item classes whose definitions are nested within the definition
-of the final class itself, and
-\item classes whose definition occurs within the same statement
-sequence as the definition of the final class.
-\end{itemize}
-\iffinaltype{
-A non-abstract final class is also called a {\em
-leaf class}.  When used in a binding of an abstract type, \verb@final@
-restricts the possible instances of the abstract type to leaf
-classes (see also \sref{sec:typedcl}).
-}
-\verb@final@ is redundant for modules and non-abstract type bindings.
 \item
 The \verb@private@ modifier can be used with any definition in a
 template. Private identifiers can be accessed only from within the template
-that defines them.  Furthermore, accesses are not permitted in
-packagings (\sref{sec:topdefs}) other than the one containing the
-definition. Private members are not inherited by subclasses and they
+that defines them.  
+%Furthermore, accesses are not permitted in
+%packagings (\sref{sec:topdefs}) other than the one containing the
+%definition. 
+Private members are not inherited by subclasses and they
 may not override definitions in superclasses.
-\verb@private@ may not be combined in one modifier list with
-\verb@protected@, \verb@abstract@, \verb@final@ or
-\verb@override@.
+\verb@private@ may not be applied to abstract members, and it
+may not be combined in one modifier list with
+\verb@protected@, \verb@final@ or \verb@override@.
 \item
 The \verb@protected@ modifier applies to class member definitions.
 Protected members can be accessed from within the template of the defining
 class as well as in all templates that have the defining class as a base class.
-Furthermore, accesses from the template of the defining class are not
-permitted in packagings other than the one
-containing the definition.  A protected identifier \verb@x$ may be used as
-a member name in a selection \verb@r.x$ only if \verb@r$ is one of the reserved
+%Furthermore, accesses from the template of the defining class are not
+%permitted in packagings other than the one
+%containing the definition.  
+A protected identifier \verb@x@ may be used as
+a member name in a selection \verb@r.x@ only if \verb@r@ is one of the reserved
 words \verb@this@ and
-\verb@super@, or if \verb@r$'s type conforms to a type-instance of a class
+\verb@super@, or if \verb@r@'s type conforms to a type-instance of the class
 which contains the access.
 \item
-The \verb@override@ modifier applies to member definitions.  If a
-definition of a simple name \verb@x$ is preceded by
-\verb@override@, the definition is taken to override
-(\sref{sec:overriding}) a member in the least proper supertype
-(\sref{sec:templates}) which is identified by the simple name \verb@x$.
-The \verb@override@ modifier may be followed by a qualified name.  If
-a definition of a simple name \verb@x$ is preceded by
-\verb@override \verb@Q$@, the definition is taken to override
-a member in the base class referenced by the qualified name \verb@Q$ which
-is identified by the simple name \verb@x$.  In both cases, there must exist
-such a member according to the rules of (\sref{sec:names}).
-\verb@override@ may not be combined in one modifier list with
-\verb@private@.
-\ifqualified{
+The \verb@override@ modifier applies to class member definitions.  It
+is mandatory for member definitions that override some other
+non-abstract member definition in a super- or mixin-class. If an
+\verb@override@ modifier is given, there must be at least one
+overridden member definition.  Furthermore, the overridden definition
+must be concrete \sref{sec:members}, unless the class containing the
+overriding member is abstract.
 \item
-The \verb@qualified@ modifier applies to class or module
-definitions. When present, all non-overriding member definitions of
-the class or module (named \verb@M$, say) introduce names which are
-qualified by \verb@M$.  When absent, non-overriding member definitions of
-the class or module introduce names which are qualified by the empty
-string $\epsilon$.
-}
+The \verb@abstract@ modifier is used in class definitions. It is
+mandatory if the class has abstract members, or if the class has
+members labelled \verb@override@ which override only abstract members
+in a superclass or mixin class.  Classes with \verb@abstract@ members
+cannot be instantiated (\sref{sec:inst-creation}) with a constructor
+invocation unless followed by mixin constructors or statements which
+override all abstract members of the class.
+\item
+The \verb@final@ modifier applies to class member definitions and to
+class definitions. A \verb@final@ class member definition may not be
+overridden in subclasses. A \verb@final@ class may not be inherited by
+a template. \verb@final@ is redundant for modules.  Members of final
+classes or modules are implicitly also final, so the \verb@final@
+modifier is redundant for them, too.  \verb@final@ may not be applied
+to abstract members, and it may not be combined in one modifier list with
+\verb@private@ or \verb@sealed@.
+\item
+The \verb@sealed@ modifier applies to class definitions. A
+\verb@sealed@ class may not be inherited, except if either
+\begin{itemize}
+\item
+the inheriting template is nested within the definition of the sealed
+class itself, or
+\item
+the inheriting template belongs to a class or object definition which
+forms part of the same statement sequence as the definition of the
+sealed class.
+\end{itemize}
 \end{itemize}
 
-\comment{
 \example A useful idiom to prevent clients of a class from
 constructing new instances of that class is to declare the class
 \verb@final@ and \verb@abstract@:
 
 \begin{verbatim}
-abstract final class C (x: Int) with {
-  def nextC = C(x + 1) with {}
+object m {
+  abstract final class C (x: Int) {
+    def nextC = C(x + 1) with {}
+  }
+  val empty = new C(0) {}
 }
-val empty = new C(0) with {}
 \end{verbatim}
 For instance, in the code above clients can create instances of class
-\verb@C$ only by calling the \verb@nextC@ method of an existing \verb@C@
+\verb@m.C@ only by calling the \verb@nextC@ method of an existing \verb@m.C@
 object; it is not possible for clients to create objects of class
-\verb@C@ directly. Indeed the following two lines are both in error:
+\verb@m.C@ directly. Indeed the following two lines are both in error:
 
 \begin{verbatim}
-  C(0)                \=// ERROR: C is an interface, may not be instantiated.
-  C(0) with {}        \>// ERROR: C is final, may not be subclassed.
+  m.C(0)           \=// ERROR: C is abstract, so it cannot be instantiated.
+  m.C(0) {}        \>// ERROR: illegal inheritance from final class.
 \end{verbatim}
 
-
-}
-
-\comment{
-\example The following example illustrates the difference between
-virtual and non-virtual members with respect to overriding.
-
-\begin{verbatim}
-class C with {
-  virtual def f = "f in C"
-  def g = "g in C"
-  def both1 = this.f ++ ", " ++ this.g
-  def both2 = f ++ ", " ++ g
-}
-
-class D extends C with {
-  override def f = "f in D"
-  override def g = "redefined g in D"
-  new def g = "new g in D"
-}
-
-val d = D
-println(d.f)                \=// prints ``f in D''
-println(d.g)		    \>// prints ``new g in D''
-println(d.both1)	    \>// prints ``f in D, redefined g in D''
-println(d.both2)	    \>// prints ``f in D, g in C''
-
-val c: C = d
-println(c.f)                \=// prints ``f in D''
-println(c.g)		    \>// prints ``redefined g in D''
-println(c.both1)	    \>// prints ``f in D, redefined g in D''
-println(c.both2)	    \>// prints ``f in D, g in C''
-\end{verbatim}
-}
-
-\comment{
-\section{The Self Type}
-\label{sec:self-type}
-
-\syntax\begin{verbatim}
-SimpleType     \=::= \= $\This$
-\end{verbatim}
-
-The self type \verb@this@ may be used in the statement part of a
-template, where it refers to the type of the object being defined by
-the template.  It is the type of the self reference \verb@this@.
-
-For every leaf class (\sref{sec:modifiers}) $C$, \verb@this@ is
-treated as an alias for the class itself, as if it was declared such:
-\begin{verbatim}
-final class C ... with {
-  type this = C
-  ...
-}
-\end{verbatim}
-For non-leaf classes $C$, \verb@this@ is treated as an abstract type
-bounded by the class itself, as if it was declared such:
-\begin{verbatim}
-abstract class C ... with {
-  type this extends C
-  ...
-}
-\end{verbatim}
-
-Analogously, for every compound type \verb@$T_1$ with ... with $T_n$@,
-\verb@this@ is treated as an abstract type conforming to the whole compound
-type, as if it was bound in the refinement
-\begin{verbatim}
-type this extends $T_1$ with ... with $T_n$ .
-\end{verbatim}
-Finally, for every declaration of a parameter or abstract type
-\mbox{$a \extends T$}, \verb@this@ is treated as an an abstract type
-conforming to $a$, as if the bound type $T$ was augmented to
-\verb@$T$ with { abstract type this extends $a$ }@.
-On the other hand, if the parameter or abstract type is declared
-\verb@final@, as in $\FINAL;a \extends T$, then \verb@this@ is treated as an alias
-for $a$, as if the bound type $T$ was augmented to
-\verb@$T$ with { type this = $a$ }@.
-
-\example
-Consider the following classes for one- and two-dimensional
-points with a \verb@distance@ method that computes the distance
-between two points of the same type.
-\begin{verbatim}
-class Point1D(x: Float) with {
-  def xCoord = x
-  def distance (that: this)  =  abs(this.xCoord - that.xCoord)
-  def self: this = this
-}
-final class FinalPoint1D(x: Float) extends Point1D(x)
-
-class Point2D(x: Float, y: Float) extends Point1D(x) with {
-  def yCoord = y
-  override def distance(that: this) =
-    sqrt (square(this.xCoord - that.xCoord) + square(this.yCoord - that.yCoord))
-}
-\end{verbatim}
-Assume the following definitions:
-\begin{verbatim}
-val p1f: FinalPoint1D = FinalPoint1D(0.0)
-val p1a: Point1D = p1f
-val p1b: Point1D = Point2D(3.0, 4.0)
-\end{verbatim}
-Of the following expressions, three are well-formed, the other three
-are ill-formed.
-\begin{verbatim}
-p1f distance p1f            \=// OK, yields 0,0
-p1f distance p1b	    \>// OK, yields 3.0
-p1a distance p1a 	    \>// OK, yields 0.0
-p1a distance p1f		\>// ERROR, required: p1a.this, found: FinalPoint1D
-p1a distance p1b		\>// ERROR, required: p1a.this, found: p1b.this
-p1b distance p1a		\>// ERROR, required: p1b.this, found: p1a.this
-\end{verbatim}
-The last of these expressions would cause an illegal access to a
-non-existing class \verb@yCoord@ of an object of type \verb@Point1D@,
-if it were permitted to execute in spite of being not well-typed.
-}
-
 \section{Class Definitions}
 \label{sec:classes}
 
@@ -4543,3 +4433,118 @@ not exist.  To reference one of the two functions with simple name
 \verb@M@.
 }
 
+\comment{
+\example The following example illustrates the difference between
+virtual and non-virtual members with respect to overriding.
+
+\begin{verbatim}
+class C with {
+  virtual def f = "f in C"
+  def g = "g in C"
+  def both1 = this.f ++ ", " ++ this.g
+  def both2 = f ++ ", " ++ g
+}
+
+class D extends C with {
+  override def f = "f in D"
+  override def g = "redefined g in D"
+  new def g = "new g in D"
+}
+
+val d = D
+println(d.f)                \=// prints ``f in D''
+println(d.g)		    \>// prints ``new g in D''
+println(d.both1)	    \>// prints ``f in D, redefined g in D''
+println(d.both2)	    \>// prints ``f in D, g in C''
+
+val c: C = d
+println(c.f)                \=// prints ``f in D''
+println(c.g)		    \>// prints ``redefined g in D''
+println(c.both1)	    \>// prints ``f in D, redefined g in D''
+println(c.both2)	    \>// prints ``f in D, g in C''
+\end{verbatim}
+}
+
+\comment{
+\section{The Self Type}
+\label{sec:self-type}
+
+\syntax\begin{verbatim}
+SimpleType     \=::= \= $\This$
+\end{verbatim}
+
+The self type \verb@this@ may be used in the statement part of a
+template, where it refers to the type of the object being defined by
+the template.  It is the type of the self reference \verb@this@.
+
+For every leaf class (\sref{sec:modifiers}) $C$, \verb@this@ is
+treated as an alias for the class itself, as if it was declared such:
+\begin{verbatim}
+final class C ... with {
+  type this = C
+  ...
+}
+\end{verbatim}
+For non-leaf classes $C$, \verb@this@ is treated as an abstract type
+bounded by the class itself, as if it was declared such:
+\begin{verbatim}
+abstract class C ... with {
+  type this extends C
+  ...
+}
+\end{verbatim}
+
+Analogously, for every compound type \verb@$T_1$ with ... with $T_n$@,
+\verb@this@ is treated as an abstract type conforming to the whole compound
+type, as if it was bound in the refinement
+\begin{verbatim}
+type this extends $T_1$ with ... with $T_n$ .
+\end{verbatim}
+Finally, for every declaration of a parameter or abstract type
+\mbox{$a \extends T$}, \verb@this@ is treated as an an abstract type
+conforming to $a$, as if the bound type $T$ was augmented to
+\verb@$T$ with { abstract type this extends $a$ }@.
+On the other hand, if the parameter or abstract type is declared
+\verb@final@, as in $\FINAL;a \extends T$, then \verb@this@ is treated as an alias
+for $a$, as if the bound type $T$ was augmented to
+\verb@$T$ with { type this = $a$ }@.
+
+\example
+Consider the following classes for one- and two-dimensional
+points with a \verb@distance@ method that computes the distance
+between two points of the same type.
+\begin{verbatim}
+class Point1D(x: Float) with {
+  def xCoord = x
+  def distance (that: this)  =  abs(this.xCoord - that.xCoord)
+  def self: this = this
+}
+final class FinalPoint1D(x: Float) extends Point1D(x)
+
+class Point2D(x: Float, y: Float) extends Point1D(x) with {
+  def yCoord = y
+  override def distance(that: this) =
+    sqrt (square(this.xCoord - that.xCoord) + square(this.yCoord - that.yCoord))
+}
+\end{verbatim}
+Assume the following definitions:
+\begin{verbatim}
+val p1f: FinalPoint1D = FinalPoint1D(0.0)
+val p1a: Point1D = p1f
+val p1b: Point1D = Point2D(3.0, 4.0)
+\end{verbatim}
+Of the following expressions, three are well-formed, the other three
+are ill-formed.
+\begin{verbatim}
+p1f distance p1f            \=// OK, yields 0,0
+p1f distance p1b	    \>// OK, yields 3.0
+p1a distance p1a 	    \>// OK, yields 0.0
+p1a distance p1f		\>// ERROR, required: p1a.this, found: FinalPoint1D
+p1a distance p1b		\>// ERROR, required: p1a.this, found: p1b.this
+p1b distance p1a		\>// ERROR, required: p1b.this, found: p1a.this
+\end{verbatim}
+The last of these expressions would cause an illegal access to a
+non-existing class \verb@yCoord@ of an object of type \verb@Point1D@,
+if it were permitted to execute in spite of being not well-typed.
+}
+