equal
deleted
inserted
replaced
854 also difficult to read. In the next chapter we describe how to construct |
854 also difficult to read. In the next chapter we describe how to construct |
855 terms with the (build in) antiquotation @{text "@{term \<dots>}"}. A restriction |
855 terms with the (build in) antiquotation @{text "@{term \<dots>}"}. A restriction |
856 of this antiquotation is that it does not allow you to use schematic |
856 of this antiquotation is that it does not allow you to use schematic |
857 variables in terms. If you want to have an antiquotation that does not have |
857 variables in terms. If you want to have an antiquotation that does not have |
858 this restriction, you can implement your own using the function @{ML_ind |
858 this restriction, you can implement your own using the function @{ML_ind |
859 inline in ML_Antiquote} from the structure @{ML_struct ML_Antiquote}. The code |
859 inline in ML_Antiquotation} from the structure @{ML_struct ML_Antiquotation}. The code |
860 for the antiquotation @{text "term_pat"} is as follows. |
860 for the antiquotation @{text "term_pat"} is as follows. |
861 *} |
861 *} |
862 |
862 |
863 ML %linenosgray{*val term_pat_setup = |
863 ML %linenosgray{*val term_pat_setup = |
864 let |
864 let |
867 fun term_pat (ctxt, str) = |
867 fun term_pat (ctxt, str) = |
868 str |> Proof_Context.read_term_pattern ctxt |
868 str |> Proof_Context.read_term_pattern ctxt |
869 |> ML_Syntax.print_term |
869 |> ML_Syntax.print_term |
870 |> ML_Syntax.atomic |
870 |> ML_Syntax.atomic |
871 in |
871 in |
872 ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat) |
872 ML_Antiquotation.inline @{binding "term_pat"} (parser >> term_pat) |
873 end*} |
873 end*} |
874 |
874 |
875 text {* |
875 text {* |
876 To use it you also have to install it using \isacommand{setup} like so |
876 To use it you also have to install it using \isacommand{setup} like so |
877 *} |
877 *} |
904 str |> Syntax.read_typ ctxt' |
904 str |> Syntax.read_typ ctxt' |
905 |> ML_Syntax.print_typ |
905 |> ML_Syntax.print_typ |
906 |> ML_Syntax.atomic |
906 |> ML_Syntax.atomic |
907 end |
907 end |
908 in |
908 in |
909 ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat) |
909 ML_Antiquotation.inline @{binding "typ_pat"} (parser >> typ_pat) |
910 end*} |
910 end*} |
911 |
911 |
912 text {* |
912 text {* |
913 which can be installed with |
913 which can be installed with |
914 *} |
914 *} |
919 However, a word of warning is in order: Introducing new antiquotations |
919 However, a word of warning is in order: Introducing new antiquotations |
920 should be done only after careful deliberations. They can make your |
920 should be done only after careful deliberations. They can make your |
921 code harder to read, than making it easier. |
921 code harder to read, than making it easier. |
922 |
922 |
923 \begin{readmore} |
923 \begin{readmore} |
924 The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions |
924 The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"} |
925 for most antiquotations. Most of the basic operations on ML-syntax are implemented |
925 contain the infrastructure and definitions for most antiquotations. Most of the basic operations |
926 in @{ML_file "Pure/ML/ml_syntax.ML"}. |
926 on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}. |
927 \end{readmore} |
927 \end{readmore} |
928 *} |
928 *} |
929 |
929 |
930 section {* Storing Data in Isabelle\label{sec:storing} *} |
930 section {* Storing Data in Isabelle\label{sec:storing} *} |
931 |
931 |