42 For example: |
42 For example: |
43 |
43 |
44 @{ML_response [display,gray] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"} |
44 @{ML_response [display,gray] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"} |
45 |
45 |
46 @{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"} |
46 @{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"} |
47 |
|
48 The type of a parser is defined as |
|
49 |
|
50 |
|
51 |
|
52 |
47 |
53 This function will either succeed (as in the two examples above) or raise the exception |
48 This function will either succeed (as in the two examples above) or raise the exception |
54 @{text "FAIL"} if no string can be consumed. For example trying to parse |
49 @{text "FAIL"} if no string can be consumed. For example trying to parse |
55 |
50 |
56 @{ML_response_fake [display,gray] "($$ \"x\") (explode \"world\")" |
51 @{ML_response_fake [display,gray] "($$ \"x\") (explode \"world\")" |
579 |
574 |
580 @{ML_response [display,gray] |
575 @{ML_response [display,gray] |
581 "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" |
576 "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" |
582 "XML.Elem (\"token\", [], [XML.Text \"foo\"])"} |
577 "XML.Elem (\"token\", [], [XML.Text \"foo\"])"} |
583 |
578 |
584 You can see better what is going on if you replace |
579 This function returns an XML-tree. You can see better what is going on if |
585 @{ML Position.none} by @{ML "Position.line 42"}, say: |
580 you replace @{ML Position.none} by @{ML "Position.line 42"}, say: |
586 |
581 |
587 @{ML_response [display,gray] |
582 @{ML_response [display,gray] |
588 "let |
583 "let |
589 val input = OuterSyntax.scan (Position.line 42) \"foo\" |
584 val input = OuterSyntax.scan (Position.line 42) \"foo\" |
590 in |
585 in |
661 "((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []), |
656 "((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []), |
662 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
657 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
663 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
658 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
664 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
659 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
665 |
660 |
666 As can be seen, the result is a ``nested'' four-tuple consisting of an |
661 As you see, the result is a ``nested'' four-tuple consisting of an |
667 optional locale (in this case @{ML NONE}); a list of variables with optional |
662 optional locale (in this case @{ML NONE}); a list of variables with optional |
668 type-annotation and syntax-annotation; a list of for-fixes (fixed variables; in this |
663 type-annotation and syntax-annotation; a list of for-fixes (fixed variables; in this |
669 case there are none); and a list of rules where every rule has optionally a name and |
664 case there are none); and a list of rules where every rule has optionally a name and |
670 an attribute. |
665 an attribute. |
671 |
666 |
714 |
709 |
715 @{ML_response [display,gray] |
710 @{ML_response [display,gray] |
716 "parse OuterParse.for_fixes (filtered_input \"for foo and bar and blink\")" |
711 "parse OuterParse.for_fixes (filtered_input \"for foo and bar and blink\")" |
717 "([(foo, NONE, NoSyn), (bar, NONE, NoSyn), (blink, NONE, NoSyn)],[])"} |
712 "([(foo, NONE, NoSyn), (bar, NONE, NoSyn), (blink, NONE, NoSyn)],[])"} |
718 |
713 |
719 Lines 5 to 9 implement the parser for a list of introduction rules, that is propositions |
714 Lines 5 to 9 in the function @{ML spec_parser} implement the parser for a |
720 with theorem annotations. The introduction rules are propositions parsed |
715 list of introduction rules, that is propositions with theorem |
721 by @{ML OuterParse.prop}. However, they can include an optional theorem name plus |
716 annotations. The introduction rules are propositions parsed by @{ML |
|
717 OuterParse.prop}. However, they can include an optional theorem name plus |
722 some attributes. For example |
718 some attributes. For example |
723 |
719 |
724 @{ML_response [display,gray] "let |
720 @{ML_response [display,gray] "let |
725 val input = filtered_input \"foo_lemma[intro,dest!]:\" |
721 val input = filtered_input \"foo_lemma[intro,dest!]:\" |
726 val ((name, attrib), _) = parse (SpecParse.thm_name \":\") input |
722 val ((name, attrib), _) = parse (SpecParse.thm_name \":\") input |
727 in |
723 in |
728 (name, map Args.dest_src attrib) |
724 (name, map Args.dest_src attrib) |
729 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
725 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
730 |
726 |
731 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of |
727 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of |
732 @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some |
728 @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name |
733 attributes. The name has to end with @{text [quotes] ":"}---see argument of |
729 has to end with @{text [quotes] ":"}---see the argument of |
734 @{ML SpecParse.opt_thm_name} in Line 9. |
730 @{ML SpecParse.opt_thm_name} in Line 9. |
735 |
731 |
736 \begin{readmore} |
732 \begin{readmore} |
737 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} |
733 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} |
738 and @{ML_file "Pure/Isar/args.ML"}. |
734 and @{ML_file "Pure/Isar/args.ML"}. |