equal
deleted
inserted
replaced
404 For convenience we define the function: |
404 For convenience we define the function: |
405 |
405 |
406 *} |
406 *} |
407 |
407 |
408 ML{*fun filtered_input str = |
408 ML{*fun filtered_input str = |
409 filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *} |
409 filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *} |
410 |
410 |
411 text {* |
411 text {* |
412 |
412 |
413 If you now parse |
413 If you now parse |
414 |
414 |
592 |
592 |
593 \begin{readmore} |
593 \begin{readmore} |
594 The functions to do with input and output of XML and YXML are defined |
594 The functions to do with input and output of XML and YXML are defined |
595 in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}. |
595 in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}. |
596 \end{readmore} |
596 \end{readmore} |
597 *} |
597 |
598 |
598 *} |
599 |
599 |
600 section {* Parsing Specifications\label{sec:parsingspecs} *} |
600 section {* Parsing Specifications\label{sec:parsingspecs} *} |
601 |
601 |
602 text {* |
602 text {* |
603 There are a number of special purpose parsers that help with parsing |
603 There are a number of special purpose parsers that help with parsing |