527 |
527 |
528 section {* Parsing Specifications *} |
528 section {* Parsing Specifications *} |
529 |
529 |
530 text {* |
530 text {* |
531 There are a number of special purpose parsers that help with parsing specifications |
531 There are a number of special purpose parsers that help with parsing specifications |
532 of functions, inductive definitions and so on. For example the function |
532 of functions, inductive definitions and so on. For example the |
533 @{ML OuterParse.target} reads a target in order to indicate a locale. |
533 @{ML OuterParse.target} reads a target in order to indicate a locale. |
534 |
534 |
535 @{ML_response [display,gray] |
535 @{ML_response [display,gray] |
536 "let |
536 "let |
537 val input = filtered_input \"(in test)\" |
537 val input = filtered_input \"(in test)\" |
541 |
541 |
542 The function @{ML OuterParse.opt_target} makes this parser ``optional'', that |
542 The function @{ML OuterParse.opt_target} makes this parser ``optional'', that |
543 is wrapping the result into an option type and returning @{ML NONE} if no |
543 is wrapping the result into an option type and returning @{ML NONE} if no |
544 target is present. |
544 target is present. |
545 |
545 |
546 The function @{ML OuterParse.fixes} reads a list of constants |
546 The function @{ML OuterParse.fixes} reads an \isacommand{and}-separated |
547 that can include type annotations and syntax translations. |
547 list of constants that can include type annotations and syntax translations. |
548 The list is separated by \isacommand{and}. For example: |
548 For example:\footnote{Note that in the code we need to write |
|
549 @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes |
|
550 in the compound type.} |
549 *} |
551 *} |
550 |
552 |
551 text {* |
553 text {* |
552 |
554 |
553 @{ML_response [display,gray] |
555 @{ML_response [display,gray] |
559 end" |
561 end" |
560 "([(foo, SOME \<dots>, Mixfix (\"FOO\",[100],100)), |
562 "([(foo, SOME \<dots>, Mixfix (\"FOO\",[100],100)), |
561 (bar, SOME \<dots>, NoSyn), |
563 (bar, SOME \<dots>, NoSyn), |
562 (blonk, NONE, NoSyn)],[])"} |
564 (blonk, NONE, NoSyn)],[])"} |
563 |
565 |
564 Whenever types are given, then they are stored in the @{ML SOME}s. |
566 Whenever types are given, then they are stored in the @{ML SOME}s. |
565 Note that we had to write @{text "\\\"int \<Rightarrow> bool\\\""} to properly escape |
567 If a syntax translation is present for a constant, then it is |
566 the double quotes in the compound type. |
568 stored in the @{ML Mixfix} data structure; no syntax translation is |
|
569 indicated by @{ML NoSyn}. |
|
570 |
|
571 (FIXME: should for-fixes take any syntax annotation?) |
567 |
572 |
568 @{ML OuterParse.for_fixes} is an ``optional'' that prefixes |
573 @{ML OuterParse.for_fixes} is an ``optional'' that prefixes |
569 @{ML OuterParse.fixes} with the comman \isacommand{for}. |
574 @{ML OuterParse.fixes} with the comman \isacommand{for}. |
570 (FIXME give an example and explain more) |
575 (FIXME give an example and explain more) |
571 |
576 |