equal
deleted
inserted
replaced
1331 \texttt{SpecParse.token} are all the same). |
1331 \texttt{SpecParse.token} are all the same). |
1332 |
1332 |
1333 Input text is split up into tokens, and the input source type for many parsing |
1333 Input text is split up into tokens, and the input source type for many parsing |
1334 functions is \texttt{token list}. |
1334 functions is \texttt{token list}. |
1335 |
1335 |
1336 The data type definition (which is not published in the signature) is |
1336 The datatype definition (which is not published in the signature) is |
1337 \begin{verbatim} |
1337 \begin{verbatim} |
1338 datatype token = Token of Position.T * (token_kind * string); |
1338 datatype token = Token of Position.T * (token_kind * string); |
1339 \end{verbatim} |
1339 \end{verbatim} |
1340 but here are some runnable examples for viewing tokens: |
1340 but here are some runnable examples for viewing tokens: |
1341 |
1341 |
1516 |
1516 |
1517 section{* The \texttt{Args} structure *} |
1517 section{* The \texttt{Args} structure *} |
1518 |
1518 |
1519 text {* |
1519 text {* |
1520 The source file is \texttt{src/Pure/Isar/args.ML}. |
1520 The source file is \texttt{src/Pure/Isar/args.ML}. |
1521 The primary type of this structure is the \texttt{src} data type; |
1521 The primary type of this structure is the \texttt{src} datatype; |
1522 the single constructors not published in the signature, but |
1522 the single constructors not published in the signature, but |
1523 \texttt{Args.src} and \texttt{Args.dest\_src} |
1523 \texttt{Args.src} and \texttt{Args.dest\_src} |
1524 are in fact the constructor and destructor functions. |
1524 are in fact the constructor and destructor functions. |
1525 Note that the types \texttt{Attrib.src} and \texttt{Method.src} |
1525 Note that the types \texttt{Attrib.src} and \texttt{Method.src} |
1526 are in fact \texttt{Args.src}. |
1526 are in fact \texttt{Args.src}. |