equal
deleted
inserted
replaced
661 and then thread this information up the ``processing chain''. To see this, |
661 and then thread this information up the ``processing chain''. To see this, |
662 modify the function @{ML filtered_input}, described earlier, as follows |
662 modify the function @{ML filtered_input}, described earlier, as follows |
663 \<close> |
663 \<close> |
664 |
664 |
665 ML %grayML\<open>fun filtered_input' str = |
665 ML %grayML\<open>fun filtered_input' str = |
666 filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 7) str)\<close> |
666 filter Token.is_proper |
|
667 (Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 7) str)\<close> |
667 |
668 |
668 text \<open> |
669 text \<open> |
669 where we pretend the parsed string starts on line 7. An example is |
670 where we pretend the parsed string starts on line 7. An example is |
670 |
671 |
671 @{ML_response [display,gray] |
672 @{ML_response [display,gray] |
768 The result of the decoding is an XML-tree. You can see better what is going on if |
769 The result of the decoding is an XML-tree. You can see better what is going on if |
769 you replace @{ML Position.none} by @{ML \<open>Position.line 42\<close>}, say: |
770 you replace @{ML Position.none} by @{ML \<open>Position.line 42\<close>}, say: |
770 |
771 |
771 @{ML_response [display,gray] |
772 @{ML_response [display,gray] |
772 \<open>let |
773 \<open>let |
773 val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) "foo" |
774 val input = Token.explode (Thy_Header.get_keywords' @{context}) |
|
775 (Position.line 42) "foo" |
774 in |
776 in |
775 YXML.parse (fst (Parse.term input)) |
777 YXML.parse (fst (Parse.term input)) |
776 end\<close> |
778 end\<close> |
777 \<open><input delimited="false" line="42" offset="1" end_offset="4">foo</input>\<close>} |
779 \<open><input delimited="false" line="42" offset="1" end_offset="4">foo</input>\<close>} |
778 |
780 |
1138 "proving a proposition" |
1140 "proving a proposition" |
1139 (parser >> setup_proof) |
1141 (parser >> setup_proof) |
1140 end\<close> |
1142 end\<close> |
1141 |
1143 |
1142 text \<open> |
1144 text \<open> |
1143 In Line 12, we implement a parser that first reads in an optional lemma name (terminated |
1145 In Line 13, we implement a parser that first reads in an optional lemma name (terminated |
1144 by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML-text |
1146 by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML-text |
1145 and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime} |
1147 and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime} |
1146 in the structure @{ML_structure Code_Runtime}. Once the ML-text has been turned into a term, |
1148 in the structure @{ML_structure Code_Runtime}. Once the ML-text has been turned into a term, |
1147 the function @{ML theorem in Proof} opens a corresponding proof-state. This function takes the |
1149 the function @{ML theorem in Proof} opens a corresponding proof-state. This function takes the |
1148 function \<open>after_qed\<close> as argument, whose purpose is to store the theorem |
1150 function \<open>after_qed\<close> as argument, whose purpose is to store the theorem |