724 @{ML_ind Args.context} |
724 @{ML_ind Args.context} |
725 *} |
725 *} |
726 (* |
726 (* |
727 ML {* |
727 ML {* |
728 let |
728 let |
729 val parser = Args.context -- Scan.lift Args.name_source |
729 val parser = Args.context -- Scan.lift Args.name_inner_syntax |
730 |
730 |
731 fun term_pat (ctxt, str) = |
731 fun term_pat (ctxt, str) = |
732 str |> Syntax.read_prop ctxt |
732 str |> Syntax.read_prop ctxt |
733 in |
733 in |
734 (parser >> term_pat) (Context.Proof @{context}, filtered_input "f (a::nat)") |
734 (parser >> term_pat) (Context.Proof @{context}, filtered_input "f (a::nat)") |
750 text {* |
750 text {* |
751 There is usually no need to write your own parser for parsing inner syntax, that is |
751 There is usually no need to write your own parser for parsing inner syntax, that is |
752 for terms and types: you can just call the predefined parsers. Terms can |
752 for terms and types: you can just call the predefined parsers. Terms can |
753 be parsed using the function @{ML_ind term in Parse}. For example: |
753 be parsed using the function @{ML_ind term in Parse}. For example: |
754 |
754 |
755 @{ML_response [display,gray] |
755 @{ML_response_fake [display,gray] |
756 "let |
756 "let |
757 val input = Outer_Syntax.scan Position.none \"foo\" |
757 val input = Outer_Syntax.scan Position.none \"foo\" |
758 in |
758 in |
759 Parse.term input |
759 Parse.term input |
760 end" |
760 end" |
761 "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"} |
761 "(\"<markup>\", [])"} |
|
762 |
762 |
763 |
763 The function @{ML_ind prop in Parse} is similar, except that it gives a different |
764 The function @{ML_ind prop in Parse} is similar, except that it gives a different |
764 error message, when parsing fails. As you can see, the parser not just returns |
765 error message, when parsing fails. As you can see, the parser not just returns |
765 the parsed string, but also some encoded information. You can decode the |
766 the parsed string, but also some markup information. You can decode the |
766 information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. For example |
767 information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. |
767 |
|
768 @{ML_response_fake [display,gray] |
|
769 "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" |
|
770 "Text \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""} |
|
771 |
|
772 The result of the decoding is an XML-tree. You can see better what is going on if |
768 The result of the decoding is an XML-tree. You can see better what is going on if |
773 you replace @{ML Position.none} by @{ML "Position.line 42"}, say: |
769 you replace @{ML Position.none} by @{ML "Position.line 42"}, say: |
774 |
770 |
775 @{ML_response_fake [display,gray] |
771 @{ML_response_fake [display,gray] |
776 "let |
772 "let |
845 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\") |
841 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\") |
846 in |
842 in |
847 parse spec_parser input |
843 parse spec_parser input |
848 end" |
844 end" |
849 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
845 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
850 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
846 [((even0,\<dots>),\<dots>), |
851 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
847 ((evenS,\<dots>),\<dots>), |
852 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
848 ((oddS,\<dots>),\<dots>)]), [])"} |
853 |
849 |
854 As you see, the result is a pair consisting of a list of |
850 As you see, the result is a pair consisting of a list of |
855 variables with optional type-annotation and syntax-annotation, and a list of |
851 variables with optional type-annotation and syntax-annotation, and a list of |
856 rules where every rule has optionally a name and an attribute. |
852 rules where every rule has optionally a name and an attribute. |
857 |
853 |
867 val input = filtered_input |
863 val input = filtered_input |
868 \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\" |
864 \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\" |
869 in |
865 in |
870 parse Parse.fixes input |
866 parse Parse.fixes input |
871 end" |
867 end" |
872 "([(foo, SOME \"\\^E\\^Ftoken\\^Eint \<Rightarrow> bool\\^E\\^F\\^E\", NoSyn), |
868 "([(foo, SOME \<dots>, NoSyn), |
873 (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)), |
869 (bar, SOME \<dots>, Mixfix (\"BAR\", [], 100)), |
874 (blonk, NONE, NoSyn)],[])"} |
870 (blonk, NONE, NoSyn)],[])"} |
875 *} |
871 *} |
876 |
872 |
877 text {* |
873 text {* |
878 Whenever types are given, they are stored in the @{ML SOME}s. The types are |
874 Whenever types are given, they are stored in the @{ML SOME}s. The types are |
895 |
891 |
896 @{ML_response [display,gray] "let |
892 @{ML_response [display,gray] "let |
897 val input = filtered_input \"foo_lemma[intro,dest!]:\" |
893 val input = filtered_input \"foo_lemma[intro,dest!]:\" |
898 val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input |
894 val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input |
899 in |
895 in |
900 (name, map Args.dest_src attrib) |
896 (name, map Args.name_of_src attrib) |
901 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
897 end" "(foo_lemma, [(\"intro\", \<dots>), (\"dest\", \<dots>)])"} |
902 |
898 |
903 The function @{ML_ind opt_thm_name in Parse_Spec} is the ``optional'' variant of |
899 The function @{ML_ind opt_thm_name in Parse_Spec} is the ``optional'' variant of |
904 @{ML_ind thm_name in Parse_Spec}. Theorem names can contain attributes. The name |
900 @{ML_ind thm_name in Parse_Spec}. Theorem names can contain attributes. The name |
905 has to end with @{text [quotes] ":"}---see the argument of |
901 has to end with @{text [quotes] ":"}---see the argument of |
906 the function @{ML Parse_Spec.opt_thm_name} in Line 7. |
902 the function @{ML Parse_Spec.opt_thm_name} in Line 7. |
1131 |
1127 |
1132 ML %linenosgray{*let |
1128 ML %linenosgray{*let |
1133 fun after_qed thm_name thms lthy = |
1129 fun after_qed thm_name thms lthy = |
1134 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
1130 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
1135 |
1131 |
1136 fun setup_proof (thm_name, (txt, pos)) lthy = |
1132 fun setup_proof (thm_name, {text, ...}) lthy = |
1137 let |
1133 let |
1138 val trm = Code_Runtime.value lthy result_cookie ("", txt) |
1134 val trm = Code_Runtime.value lthy result_cookie ("", text) |
1139 in |
1135 in |
1140 Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy |
1136 Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy |
1141 end |
1137 end |
1142 |
1138 |
1143 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
1139 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |