equal
deleted
inserted
replaced
55 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
55 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
56 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
56 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
57 code, rather they indicate what the response is when the code is evaluated. |
57 code, rather they indicate what the response is when the code is evaluated. |
58 There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for |
58 There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for |
59 including ML-code. The first evaluates the given code, but any effect on the |
59 including ML-code. The first evaluates the given code, but any effect on the |
60 `ambient' theory is suppressed. The second needs to be used if ML-code is defined |
60 theory, in which the code is embedded, is suppressed. The second needs to |
|
61 be used if ML-code is defined |
61 inside a proof. For example |
62 inside a proof. For example |
62 |
63 |
63 \begin{quote} |
64 \begin{quote} |
64 \begin{isabelle} |
65 \begin{isabelle} |
65 \isacommand{lemma}~@{text "test:"}\isanewline |
66 \isacommand{lemma}~@{text "test:"}\isanewline |
68 \isacommand{oops} |
69 \isacommand{oops} |
69 \end{isabelle} |
70 \end{isabelle} |
70 \end{quote} |
71 \end{quote} |
71 |
72 |
72 However, both commands will only play minor roles in this tutorial (we will always |
73 However, both commands will only play minor roles in this tutorial (we will always |
73 arrange that the ML-code is defined outside of proofs). |
74 arrange that the ML-code is defined outside of proofs, for example). |
74 |
75 |
75 Once a portion of code is relatively stable, you usually want to export it |
76 Once a portion of code is relatively stable, you usually want to export it |
76 to a separate ML-file. Such files can then be included somewhere inside a |
77 to a separate ML-file. Such files can then be included somewhere inside a |
77 theory by using the command \isacommand{use}. For example |
78 theory by using the command \isacommand{use}. For example |
78 |
79 |
101 \ldots |
102 \ldots |
102 \end{tabular} |
103 \end{tabular} |
103 \end{quote} |
104 \end{quote} |
104 |
105 |
105 Note that no parentheses are given this time. Note also that the |
106 Note that no parentheses are given this time. Note also that the |
106 `used' file should not contain any |
107 included ML-file should not contain any |
107 \isacommand{use} itself. Otherwise Isabelle is unable to record all |
108 \isacommand{use} itself. Otherwise Isabelle is unable to record all |
108 file dependencies, which is a nuisance if you have to track down |
109 file dependencies, which is a nuisance if you have to track down |
109 errors. |
110 errors. |
110 *} |
111 *} |
111 |
112 |
632 course of this chapter you will learn more about antiquotations: |
633 course of this chapter you will learn more about antiquotations: |
633 they can simplify Isabelle programming since one can directly access all |
634 they can simplify Isabelle programming since one can directly access all |
634 kinds of logical elements from the ML-level. |
635 kinds of logical elements from the ML-level. |
635 *} |
636 *} |
636 |
637 |
637 text {* FIXME: an example of a user defined antiquotation *} |
638 text {* FIXME: give an example of a user defined antiquotation *} |
638 |
639 |
639 ML{*ML_Antiquote.inline "term_pat" |
640 ML{*ML_Antiquote.inline "term_pat" |
640 (Args.context -- Scan.lift Args.name_source >> |
641 (Args.context -- Scan.lift Args.name_source >> |
641 (fn (ctxt, s) => |
642 (fn (ctxt, s) => |
642 let |
643 s |> ProofContext.read_term_pattern ctxt |
643 val t = ProofContext.read_term_pattern ctxt s |
644 |> ML_Syntax.print_term |
644 in |
645 |> ML_Syntax.atomic))*} |
645 ML_Syntax.atomic (ML_Syntax.print_term t) |
|
646 end))*} |
|
647 |
646 |
648 ML{*@{term_pat "?x + ?y"}*} |
647 ML{*@{term_pat "?x + ?y"}*} |
649 |
648 |
650 text {* |
649 text {* |
651 |
|
652 \begin{readmore} |
650 \begin{readmore} |
653 @{ML_file "Pure/ML/ml_antiquote.ML"} |
651 @{ML_file "Pure/ML/ml_antiquote.ML"} |
654 \end{readmore} |
652 \end{readmore} |
655 *} |
653 *} |
656 |
654 |