1.1 --- a/doc-src/Nitpick/nitpick.tex	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -2742,10 +2742,12 @@
     1.4  
     1.5  \prew
     1.6  $\textbf{val}\,~\textit{pick\_nits\_in\_term} : \\
     1.7 -\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{term~list} \rightarrow \textit{term} \\
     1.8 -\hbox{}\quad{\rightarrow}\; \textit{string} * \textit{Proof.state}$ \\
     1.9 +\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{mode}
    1.10 +\rightarrow \textit{int} \rightarrow \textit{int} \rightarrow \textit{int}$ \\
    1.11 +$\hbox{}\quad{\rightarrow}\; (\textit{term} * \textit{term})~\textit{list}
    1.12 +\rightarrow \textit{term~list} \rightarrow \textit{term} \rightarrow \textit{string} * \textit{Proof.state}$ \\
    1.13  $\textbf{val}\,~\textit{pick\_nits\_in\_subgoal} : \\
    1.14 -\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
    1.15 +\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{mode} \rightarrow \textit{int} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
    1.16  \postw
    1.17  
    1.18  The return value is a new proof state paired with an outcome string
    1.19 @@ -2760,13 +2762,13 @@
    1.20  \postw
    1.21  
    1.22  The second argument lets you override option values before they are parsed and
    1.23 -put into a \textit{params} record. Here is an example:
    1.24 +put into a \textit{params} record. Here is an example where Nitpick is invoked
    1.25 +on subgoal $i$ of $n$ with no time limit:
    1.26  
    1.27  \prew
    1.28  $\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout\/}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
    1.29 -$\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
    1.30 -& \textit{state}~\textit{params}~\textit{false} \\[-2pt]
    1.31 -& \textit{subgoal}\end{aligned}$
    1.32 +$\textbf{val}\,~(\textit{outcome},\, \textit{state}') = {}$ \\
    1.33 +$\hbox{}\quad\textit{Nitpick.pick\_nits\_in\_subgoal}~\textit{state}~\textit{params}~\textit{Nitpick.Normal}~\textit{i}~\textit{n}$
    1.34  \postw
    1.35  
    1.36  \let\antiq=\textrm