850 this restriction, you can implement your own using the function @{ML_ind |
850 this restriction, you can implement your own using the function @{ML_ind |
851 inline in ML_Antiquote} from the structure @{ML_struct ML_Antiquote}. The code |
851 inline in ML_Antiquote} from the structure @{ML_struct ML_Antiquote}. The code |
852 for the antiquotation @{text "term_pat"} is as follows. |
852 for the antiquotation @{text "term_pat"} is as follows. |
853 *} |
853 *} |
854 |
854 |
855 ML %linenosgray{*let |
855 ML %linenosgray{*val term_pat_setup = |
|
856 let |
856 val parser = Args.context -- Scan.lift Args.name_source |
857 val parser = Args.context -- Scan.lift Args.name_source |
857 |
858 |
858 fun term_pat (ctxt, str) = |
859 fun term_pat (ctxt, str) = |
859 str |> ProofContext.read_term_pattern ctxt |
860 str |> ProofContext.read_term_pattern ctxt |
860 |> ML_Syntax.print_term |
861 |> ML_Syntax.print_term |
861 |> ML_Syntax.atomic |
862 |> ML_Syntax.atomic |
862 in |
863 in |
863 ML_Antiquote.inline "term_pat" (parser >> term_pat) |
864 ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat) |
864 end*} |
865 end*} |
|
866 |
|
867 setup{* term_pat_setup *} |
865 |
868 |
866 text {* |
869 text {* |
867 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 |
868 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 |
869 ProofContext} (Line 5); the next two lines transform the term into a string |
872 ProofContext} (Line 5); the next two lines transform the term into a string |
876 |
879 |
877 which shows the internal representation of the term @{text "Suc ?x"}. Similarly |
880 which shows the internal representation of the term @{text "Suc ?x"}. Similarly |
878 we can write an antiquotation for type patterns. |
881 we can write an antiquotation for type patterns. |
879 *} |
882 *} |
880 |
883 |
881 ML{*let |
884 ML{*val type_pat_setup = |
|
885 let |
882 val parser = Args.context -- Scan.lift Args.name_source |
886 val parser = Args.context -- Scan.lift Args.name_source |
883 |
887 |
884 fun typ_pat (ctxt, str) = |
888 fun typ_pat (ctxt, str) = |
885 str |> Syntax.parse_typ ctxt |
889 str |> Syntax.parse_typ ctxt |
886 |> ML_Syntax.print_typ |
890 |> ML_Syntax.print_typ |
887 |> ML_Syntax.atomic |
891 |> ML_Syntax.atomic |
888 in |
892 in |
889 ML_Antiquote.inline "typ_pat" (parser >> typ_pat) |
893 ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat) |
890 end*} |
894 end*} |
|
895 |
|
896 setup{* type_pat_setup *} |
891 |
897 |
892 text {* |
898 text {* |
893 \begin{readmore} |
899 \begin{readmore} |
894 The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions |
900 The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions |
895 for most antiquotations. Most of the basic operations on ML-syntax are implemented |
901 for most antiquotations. Most of the basic operations on ML-syntax are implemented |