summaryrefslogtreecommitdiff
path: root/doc/manual.tex
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-08-07 16:53:06 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-08-07 16:53:06 -0400
commite75a028e3ced5d05be1baa05c6fb1a83b277a45f (patch)
tree3b71b2a102795dcd3b2bb3e106a0ee2309487376 /doc/manual.tex
parent4e0410306a4d4288dd36450dc8f9ea2e8bd0a154 (diff)
'-dumpTypes'
Diffstat (limited to 'doc/manual.tex')
-rw-r--r--doc/manual.tex2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index a139310c..a39f8ef8 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -199,6 +199,8 @@ urweb -tc P
\end{verbatim}
It is often worthwhile to run \cd{urweb} in this mode, because later phases of compilation can take significantly longer than type-checking alone, and the type checker catches many errors that would traditionally be found through debugging a running application.
+A related option is \cd{-dumpTypes}, which, as long as parsing succeeds, outputs to stdout a summary of the kinds of all identifiers declared with \cd{con} and the types of all identifiers declared with \cd{val} or \cd{val rec}. This information is dumped even if there are errors during type inference. Compiler error messages go to stderr, not stdout, so it is easy to distinguish the two kinds of output programmatically.
+
To output information relevant to CSS stylesheets (and not finish regular compilation), run
\begin{verbatim}
urweb -css P