Ur/Web: doc/manual.tex comparison

comparison doc/manual.tex @ 1797:bb942416bf1c

Remove 'class' declaration; now use 'con' instead

author	Adam Chlipala <adam@chlipala.net>
date	Sun, 29 Jul 2012 12:27:13 -0400
parents	69daa6d70299
children	3d922a28370b

comparison

equal deleted inserted replaced

-:0de0daab5fbb
+:bb942416bf1c
 \tableofcontents
 \section{Introduction}
-\emph{Ur} is a programming language designed to introduce richer type system features into functional programming in the tradition of ML and Haskell.  Ur is functional, pure, statically-typed, and strict.  Ur supports a powerful kind of \emph{metaprogramming} based on \emph{type-level computation with type-level records}.
+\emph{Ur} is a programming language designed to introduce richer type system features into functional programming in the tradition of ML and Haskell.  Ur is functional, pure, statically typed, and strict.  Ur supports a powerful kind of \emph{metaprogramming} based on \emph{type-level computation with type-level records}.
 \emph{Ur/Web} is Ur plus a special standard library and associated rules for parsing and optimization.  Ur/Web supports construction of dynamic web applications backed by SQL databases.  The signature of the standard library is such that well-typed Ur/Web programs ``don't go wrong'' in a very broad sense.  Not only do they not crash during particular page generations, but they also may not:
 \begin{itemize}
 \item Suffer from any kinds of code-injection attacks
 \item \texttt{cleanup}: maximum number of cleanup operations (e.g., entries recording the need to deallocate certain temporary objects) that may be active at once per request
 \item \texttt{database}: maximum size of database files (currently only used by SQLite)
 \item \texttt{deltas}: maximum number of messages sendable in a single request handler with \texttt{Basis.send}
 \item \texttt{globals}: maximum number of global variables that FFI libraries may set in a single request context
 \item \texttt{headers}: maximum size (in bytes) of per-request buffer used to hold HTTP headers for generated pages
-\item \texttt{heap}: maximum size (in bytes) of per-request heap for dynamically-allocated data
+\item \texttt{heap}: maximum size (in bytes) of per-request heap for dynamically allocated data
 \item \texttt{inputs}: maximum number of top-level form fields per request
 \item \texttt{messages}: maximum size (in bytes) of per-request buffer used to hold a single outgoing message sent with \texttt{Basis.send}
 \item \texttt{page}: maximum size (in bytes) of per-request buffer used to hold HTML content of generated pages
 \item \texttt{script}: maximum size (in bytes) of per-request buffer used to hold JavaScript content of generated pages
 \item \texttt{subinputs}: maximum number of form fields per request, excluding top-level fields
 \\
 &&& \_ & \textrm{wildcard} \\
 &&& (e) & \textrm{explicit precedence} \\
 \\
 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
-&&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
+&&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually recursive values} \\
 \end{array}$$
 As with constructors, we include both abstraction and application for kind polymorphism, but applications are only inferred internally.
 \emph{Declarations} primarily bring new symbols into context.
 $$\begin{array}{rrcll}
 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
 &&& \mt{val} \; x : \tau = e & \textrm{value} \\
-&&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
+&&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually recursive values} \\
 &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
 &&& \mt{open} \; M & \textrm{module inclusion} \\
 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
 &&& \mt{table} \; x : c & \textrm{SQL table} \\
 &&& \mt{view} \; x = e & \textrm{SQL view} \\
 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
 &&& \mt{style} \; x : \tau & \textrm{CSS class} \\
-&&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
 &&& \mt{task} \; e = e & \textrm{recurring task} \\
 \\
 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
 &&& X & \textrm{variable} \\
 &&& M.X & \textrm{projection} \\
 At the expression level, an analogue is available of the composite $\lambda$ form for constructors.  We define the language of binders as $b ::= p \mid [x] \mid [x \; ? \; \kappa] \mid X \mid [c \sim c]$.  A lone variable $[x]$ stands for an implicit constructor variable of unspecified kind.  The standard value-level function binder is recovered as the type-annotated pattern form $x : \tau$.  It is a compile-time error to include a pattern $p$ that does not match every value of the appropriate type.
 A local $\mt{val}$ declaration may bind a pattern instead of just a plain variable.  As for function arguments, only irrefutable patterns are legal.
-The keyword $\mt{fun}$ is a shorthand for $\mt{val} \; \mt{rec}$ that allows arguments to be specified before the equal sign in the definition of each mutually-recursive function, as in SML.  Each curried argument must follow the grammar of the $b$ non-terminal introduced two paragraphs ago.  A $\mt{fun}$ declaration is elaborated into a version that adds additional $\lambda$s to the fronts of the righthand sides, as appropriate.
+The keyword $\mt{fun}$ is a shorthand for $\mt{val} \; \mt{rec}$ that allows arguments to be specified before the equal sign in the definition of each mutually recursive function, as in SML.  Each curried argument must follow the grammar of the $b$ non-terminal introduced two paragraphs ago.  A $\mt{fun}$ declaration is elaborated into a version that adds additional $\lambda$s to the fronts of the righthand sides, as appropriate.
 A signature item $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2$.  A declaration $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2 = M$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2 = \mt{functor}(X_2 : S_1) : S_2 = M$.
 An $\mt{open} \; \mt{constraints}$ declaration is implicitly inserted for the argument of every functor at the beginning of the functor body.  For every declaration of the form $\mt{structure} \; X : S = \mt{struct} \ldots \mt{end}$, an $\mt{open} \; \mt{constraints} \; X$ declaration is implicitly inserted immediately afterward.
 \subsection{Declaration Typing}
 We use an auxiliary judgment $\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'$, expressing the enrichment of $\Gamma$ with the types of the datatype constructors $\overline{dc}$, when they are known to belong to datatype $x$ with type parameters $\overline{y}$.
-This is the first judgment where we deal with constructor classes, for the $\mt{class}$ declaration form.  We will omit their special handling in this formal specification.  Section \ref{typeclasses} gives an informal description of how constructor classes influence type inference.
 We presuppose the existence of a function $\mathcal O$, where $\mathcal O(M, \overline{s})$ implements the $\mt{open}$ declaration by producing a context with the appropriate entry for each available component of module $M$ with signature items $\overline{s}$.  Where possible, $\mathcal O$ uses ``transparent'' entries (e.g., an abstract type $M.x$ is mapped to $x :: \mt{Type} = M.x$), so that the relationship with $M$ is maintained.  A related function $\mathcal O_c$ builds a context containing the disjointness constraints found in $\overline s$.
 We write $\kappa_1^n \to \kappa$ as a shorthand, where $\kappa_1^0 \to \kappa = \kappa$ and $\kappa_1^{n+1} \to \kappa_2 = \kappa_1 \to (\kappa_1^n \to \kappa_2)$.  We write $\mt{len}(\overline{y})$ for the length of vector $\overline{y}$ of variables.
 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
 \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
 $$\infer{\Gamma \vdash \mt{task} \; e_1 = e_2 \leadsto \Gamma}{
 \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind} \; \tau
 & \Gamma \vdash e_2 :: \tau \to \mt{Basis}.\mt{transaction} \; \{\}
 }$$
-$$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
-\Gamma \vdash c :: \kappa
-}$$
 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
 }
 \quad \infer{\overline{y}; x; \Gamma \vdash X \; \mt{of} \; \tau \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to \tau \to x \; \overline{y}}{
 }$$
 \subsection{Signature Item Typing}
 We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
+This is the first judgment where we deal with constructor classes, for the $\mt{class}$ forms.  We will omit their special handling in this formal specification.  Section \ref{typeclasses} gives an informal description of how constructor classes influence type inference.
 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
 \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
 \Gamma \vdash s \leadsto \Gamma'
 & \Gamma' \vdash \overline{s} \leadsto \Gamma''
 }
 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}$$
 \subsection{Signature Compatibility}
-To simplify the judgments in this section, we assume that all signatures are alpha-varied as necessary to avoid including multiple bindings for the same identifier.  This is in addition to the usual alpha-variation of locally-bound variables.
+To simplify the judgments in this section, we assume that all signatures are alpha-varied as necessary to avoid including multiple bindings for the same identifier.  This is in addition to the usual alpha-variation of locally bound variables.
 We rely on a judgment $\Gamma \vdash \overline{s} \leq s'$, which expresses the occurrence in signature items $\overline{s}$ of an item compatible with $s'$.  We also use a judgment $\Gamma \vdash \overline{dc} \leq \overline{dc}$, which expresses compatibility of datatype definitions.
 $$\infer{\Gamma \vdash S \equiv S}{}
 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
 }$$
 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{class} \; x :: \kappa}{}
 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{class} \; x :: \kappa}{}
 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{class} \; x :: \kappa = c_2}{
+\Gamma \vdash c_1 \equiv c_2
+}$$
+$$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{class} \; x :: \kappa}{}
+\quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{class} \; x :: \kappa}{}
+\quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{class} \; x :: \kappa = c_2}{
 \Gamma \vdash c_1 \equiv c_2
 }$$
 \subsection{Module Typing}
 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
 \mt{sigOf}(\mt{view} \; x = e) &=& \mt{view} \; x : c \textrm{ (where $\Gamma \vdash e : \mt{Basis}.\mt{sql\_query} \; [] \; [] \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; c') \; c$)} \\
 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
-\mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x \\
+\mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x
-\mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
 \end{eqnarray*}
 \begin{eqnarray*}
 \mt{selfify}(M, \cdot) &=& \cdot \\
 \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, s) \; \mt{selfify}(M, \overline{s'}) \\
 \\
 \subsection{\label{typeclasses}Constructor Classes}
 Ur includes a constructor class facility inspired by Haskell's.  The current version is experimental, with very general Prolog-like facilities that can lead to compile-time non-termination.
-Constructor classes are integrated with the module system.  A constructor class of kind $\kappa$ is just a constructor of kind $\kappa$.  By marking such a constructor $c$ as a constructor class, the programmer instructs the type inference engine to, in each scope, record all values of types $c \; c_1 \; \ldots \; c_n$ as \emph{instances}.  Any function argument whose type is of such a form is treated as implicit, to be determined by examining the current instance database.
+Constructor classes are integrated with the module system.  A constructor class of kind $\kappa$ is just a constructor of kind $\kappa$.  By marking such a constructor $c$ as a constructor class, the programmer instructs the type inference engine to, in each scope, record all values of types $c \; c_1 \; \ldots \; c_n$ as \emph{instances}.  Any function argument whose type is of such a form is treated as implicit, to be determined by examining the current instance database.  Any suitably kinded constructor within a module may be exposed as a constructor class from outside the module, simply by using a $\mt{class}$ signature item instead of a $\mt{con}$ signature item in the module's signature.
-The ``dictionary encoding'' often used in Haskell implementations is made explicit in Ur.  Constructor class instances are just properly-typed values, and they can also be considered as ``proofs'' of membership in the class.  In some cases, it is useful to pass these proofs around explicitly.  An underscore written where a proof is expected will also be inferred, if possible, from the current instance database.
+The ``dictionary encoding'' often used in Haskell implementations is made explicit in Ur.  Constructor class instances are just properly typed values, and they can also be considered as ``proofs'' of membership in the class.  In some cases, it is useful to pass these proofs around explicitly.  An underscore written where a proof is expected will also be inferred, if possible, from the current instance database.
-Just as for constructors, constructors classes may be exported from modules, and they may be exported as concrete or abstract.  Concrete constructor classes have their ``real'' definitions exposed, so that client code may add new instances freely.  Abstract constructor classes are useful as ``predicates'' that can be used to enforce invariants, as we will see in some definitions of SQL syntax in the Ur/Web standard library.
+Just as for constructors, constructors classes may be exported from modules, and they may be exported as concrete or abstract.  Concrete constructor classes have their ``real'' definitions exposed, so that client code may add new instances freely.  Automatic inference of concrete class instances will not generally work, so abstract classes are almost always the right choice.  They are useful as ``predicates'' that can be used to enforce invariants, as we will see in some definitions of SQL syntax in the Ur/Web standard library.  Free extension of a concrete class is easily supported by exporting a constructor function from a module, since the class implementation will be concrete within the module.
 \subsection{Reverse-Engineering Record Types}
 It's useful to write Ur functions and functors that take record constructors as inputs, but these constructors can grow quite long, even though their values are often implied by other arguments.  The compiler uses a simple heuristic to infer the values of unification variables that are mapped over, yielding known results.  If the result is empty, we're done; if it's not empty, we replace a single unification variable with a new constructor formed from three new unification variables, as in $[\alpha = \beta] \rc \gamma$.  This process can often be repeated to determine a unification variable fully.
 \mt{val} \; \mt{debug} : \mt{string} \to \mt{transaction} \; \mt{unit}
 \end{array}$$
 \subsection{HTTP}
-There are transactions for reading an HTTP header by name and for getting and setting strongly-typed cookies.  Cookies may only be created by the $\mt{cookie}$ declaration form, ensuring that they be named consistently based on module structure.  For now, cookie operations are server-side only.
+There are transactions for reading an HTTP header by name and for getting and setting strongly typed cookies.  Cookies may only be created by the $\mt{cookie}$ declaration form, ensuring that they be named consistently based on module structure.  For now, cookie operations are server-side only.
 $$\begin{array}{l}
 \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\
 \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\
 \mt{val} \; \mt{setCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \{\mt{Value} : \mt{t}, \mt{Expires} : \mt{option} \; \mt{time}, \mt{Secure} : \mt{bool}\} \to \mt{transaction} \; \mt{unit} \\
 \mt{val} \; \mt{clearCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; \mt{unit}
 \mt{val} \; \mt{sql\_times} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_binary} \; \mt{t} \; \mt{t} \; \mt{t} \\
 \mt{val} \; \mt{sql\_div} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_binary} \; \mt{t} \; \mt{t} \; \mt{t} \\
 \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int}
 \end{array}$$
-Finally, we have aggregate functions.  The $\mt{COUNT(\ast)}$ syntax is handled specially, since it takes no real argument.  The other aggregate functions are placed into a general type family, using constructor classes to restrict usage to properly-typed arguments.  The key aspect of the $\mt{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields.
+Finally, we have aggregate functions.  The $\mt{COUNT(\ast)}$ syntax is handled specially, since it takes no real argument.  The other aggregate functions are placed into a general type family, using constructor classes to restrict usage to properly typed arguments.  The key aspect of the $\mt{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields.
 $$\begin{array}{l}
 \mt{val} \; \mt{sql\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int}
 \end{array}$$
 $$\begin{array}{l}
 $$\begin{array}{l}
 \mt{val} \; \mt{tryDml} : \mt{dml} \to \mt{transaction} \; (\mt{option} \; \mt{string})
 \end{array}$$
-Properly-typed records may be used to form $\mt{INSERT}$ commands.
+Properly typed records may be used to form $\mt{INSERT}$ commands.
 $$\begin{array}{l}
 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml}
 \end{array}$$
 Similar support is provided for \cd{style} attributes.  Normal CSS syntax may be used in string literals that are \cd{style} attribute values, and the desugaring may be accessed elsewhere with the pseudo-function \cd{STYLE}.
 \section{\label{structure}The Structure of Web Applications}
-A web application is built from a series of modules, with one module, the last one appearing in the \texttt{.urp} file, designated as the main module.  The signature of the main module determines the URL entry points to the application.  Such an entry point should have type $\mt{t1} \to \ldots \to \mt{tn} \to \mt{transaction} \; \mt{page}$, for any integer $n \geq 0$, where $\mt{page}$ is a type synonym for top-level HTML pages, defined in $\mt{Basis}$.  If such a function is at the top level of main module $M$, with $n = 0$, it will be accessible at URI \texttt{/M/f}, and so on for more deeply-nested functions, as described in Section \ref{tag} below.  See Section \ref{cl} for information on the \texttt{prefix} and \texttt{rewrite url} directives, which can be used to rewrite the default URIs of different entry point functions.  The final URL of a function is its default module-based URI, with \texttt{rewrite url} rules applied, and with the \texttt{prefix} prepended.  Arguments to an entry-point function are deserialized from the part of the URI following \texttt{f}.
+A web application is built from a series of modules, with one module, the last one appearing in the \texttt{.urp} file, designated as the main module.  The signature of the main module determines the URL entry points to the application.  Such an entry point should have type $\mt{t1} \to \ldots \to \mt{tn} \to \mt{transaction} \; \mt{page}$, for any integer $n \geq 0$, where $\mt{page}$ is a type synonym for top-level HTML pages, defined in $\mt{Basis}$.  If such a function is at the top level of main module $M$, with $n = 0$, it will be accessible at URI \texttt{/M/f}, and so on for more deeply nested functions, as described in Section \ref{tag} below.  See Section \ref{cl} for information on the \texttt{prefix} and \texttt{rewrite url} directives, which can be used to rewrite the default URIs of different entry point functions.  The final URL of a function is its default module-based URI, with \texttt{rewrite url} rules applied, and with the \texttt{prefix} prepended.  Arguments to an entry-point function are deserialized from the part of the URI following \texttt{f}.
 Elements of modules beside the main module, including page handlers, will only be included in the final application if they are transitive dependencies of the handlers in the main module.
 Normal links are accessible via HTTP \texttt{GET}, which the relevant standard says should never cause side effects.  To export a page which may cause side effects, accessible only via HTTP \texttt{POST}, include one argument of the page handler of type $\mt{Basis.postBody}$.  When the handler is called, this argument will receive a value that can be deconstructed into a MIME type (with $\mt{Basis.postType}$) and payload (with $\mt{Basis.postData}$).  This kind of handler should not be used with forms that exist solely within Ur/Web apps; for these, use Ur/Web's built-in support, as described below.  It may still be useful to use $\mt{Basis.postBody}$ with form requests submitted by code outside an Ur/Web app.  For such cases, the function $\mt{Top.postFields} : \mt{postBody} \to \mt{list} \; (\mt{string} \times \mt{string})$ may be useful, breaking a \texttt{POST} body of type \texttt{application/x-www-form-urlencoded} into its name-value pairs.
 Functions are specialized to particular argument patterns.  This is an important trick for avoiding the need to maintain any closures at runtime.  Currently, specialization only happens for prefixes of a function's full list of parameters, so you may need to take care to put arguments of function types before other arguments.  The optimizer will not be effective enough if you use arguments that mix functions and values that must be calculated at run-time.  For instance, a tuple of a function and an integer counter would not lead to successful code generation; these should be split into separate arguments via currying.
 \subsection{Untangle}
-Remove unnecessary mutual recursion, splitting recursive groups into strongly-connected components.
+Remove unnecessary mutual recursion, splitting recursive groups into strongly connected components.
 \subsection{Shake}
 Remove all definitions not needed to run the page handlers that are visible in the signature of the last module listed in the \texttt{.urp} file.

Mercurial > urweb

comparison doc/manual.tex @ 1797:bb942416bf1c