diff doc/manual.tex @ 1531:7efcf8f4a44a

'-dumpTypes'
author Adam Chlipala <adam@chlipala.net>
date Sun, 07 Aug 2011 16:53:06 -0400
parents 09c56e03beaf
children 7ef09e91198b
line wrap: on
line diff
--- a/doc/manual.tex	Sun Aug 07 13:47:15 2011 -0400
+++ b/doc/manual.tex	Sun Aug 07 16:53:06 2011 -0400
@@ -199,6 +199,8 @@
 \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