equal
deleted
inserted
replaced
762 replaced with the value representing the theory. |
762 replaced with the value representing the theory. |
763 |
763 |
764 Another important antiquotation is @{text "@{context}"}. (What the |
764 Another important antiquotation is @{text "@{context}"}. (What the |
765 difference between a theory and a context is will be described in Chapter |
765 difference between a theory and a context is will be described in Chapter |
766 \ref{chp:advanced}.) A context is for example needed in order to use the |
766 \ref{chp:advanced}.) A context is for example needed in order to use the |
767 function @{ML print_abbrevs in ProofContext} that list of all currently |
767 function @{ML print_abbrevs in Proof_Context} that list of all currently |
768 defined abbreviations. |
768 defined abbreviations. |
769 |
769 |
770 @{ML_response_fake [display, gray] |
770 @{ML_response_fake [display, gray] |
771 "ProofContext.print_abbrevs @{context}" |
771 "Proof_Context.print_abbrevs @{context}" |
772 "Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x) |
772 "Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x) |
773 INTER \<equiv> INFI |
773 INTER \<equiv> INFI |
774 Inter \<equiv> Inf |
774 Inter \<equiv> Inf |
775 \<dots>"} |
775 \<dots>"} |
776 |
776 |
855 ML %linenosgray{*val term_pat_setup = |
855 ML %linenosgray{*val term_pat_setup = |
856 let |
856 let |
857 val parser = Args.context -- Scan.lift Args.name_source |
857 val parser = Args.context -- Scan.lift Args.name_source |
858 |
858 |
859 fun term_pat (ctxt, str) = |
859 fun term_pat (ctxt, str) = |
860 str |> ProofContext.read_term_pattern ctxt |
860 str |> Proof_Context.read_term_pattern ctxt |
861 |> ML_Syntax.print_term |
861 |> ML_Syntax.print_term |
862 |> ML_Syntax.atomic |
862 |> ML_Syntax.atomic |
863 in |
863 in |
864 ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat) |
864 ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat) |
865 end*} |
865 end*} |
867 setup{* term_pat_setup *} |
867 setup{* term_pat_setup *} |
868 |
868 |
869 text {* |
869 text {* |
870 The parser in Line 2 provides us with a context and a string; this string is |
870 The parser in Line 2 provides us with a context and a string; this string is |
871 transformed into a term using the function @{ML_ind read_term_pattern in |
871 transformed into a term using the function @{ML_ind read_term_pattern in |
872 ProofContext} (Line 5); the next two lines transform the term into a string |
872 Proof_Context} (Line 5); the next two lines transform the term into a string |
873 so that the ML-system can understand it. (All these functions will be explained |
873 so that the ML-system can understand it. (All these functions will be explained |
874 in more detail in later sections.) An example for this antiquotation is: |
874 in more detail in later sections.) An example for this antiquotation is: |
875 |
875 |
876 @{ML_response_fake [display,gray] |
876 @{ML_response_fake [display,gray] |
877 "@{term_pat \"Suc (?x::nat)\"}" |
877 "@{term_pat \"Suc (?x::nat)\"}" |