Commit d7d59227 authored by POTTIER Francois's avatar POTTIER Francois

Eliminated some macros and fixed a spacing problem.

parent 9ed30f63
......@@ -1826,15 +1826,12 @@ channel.
\section{Generated API}
\newcommand{\mystartsymbol}{\texttt{main}\xspace}
\newcommand{\mystartsymboltype}{\texttt{thing}\xspace}
When \menhir processes a grammar specification, say \texttt{parser.mly}, it
produces one \ocaml module, \texttt{Parser}, whose code resides in the file
\texttt{parser.ml} and whose signature resides in the file
\texttt{parser.mli}. We now review this signature. For simplicity,
we assume that the grammar specification has just one start symbol
\mystartsymbol, whose \ocaml type is \mystartsymboltype.
\verb+main+, whose \ocaml type is \verb+thing+.
\subsection{Monolithic API}
\label{sec:monolithic}
......@@ -1919,7 +1916,7 @@ $O(n)$ space in memory.
% error recovery, up to a complete parse... as in Merlin.
In this API, the parser is started by invoking
\texttt{Incremental.\mystartsymbol}. (Recall that we assume \mystartsymbol is
\verb+Incremental.main+. (Recall that we assume \verb+main+ is
the name of the start symbol.) The generated file \texttt{parser.mli} contains
the following declaration:
\begin{verbatim}
......@@ -2015,9 +2012,9 @@ parser has suspended itself with a result of the form
This function expects just the previous result \verb+result+. It produces a new
result. It does not raise any exception.
The incremental API subsumes the monolithic API. Indeed, \mystartsymbol can be
The incremental API subsumes the monolithic API. Indeed, \verb+main+ can be
(and is in fact) implemented by first using
\texttt{Incremental.\mystartsymbol}, then calling \verb+offer+ and
\verb+Incremental.main+, then calling \verb+offer+ and
\verb+resume+ in a loop, until a final result is obtained.
At this time, because the type \verb+env+ is opaque, the state of the parser
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment