1.1 --- a/NEWS Mon Jun 27 17:04:04 2011 +0200
1.2 +++ b/NEWS Mon Jun 27 22:44:44 2011 +0200
1.3 @@ -141,6 +141,9 @@
1.4
1.5 *** ML ***
1.6
1.7 +* Antiquotations for ML and document preparation are managed as theory
1.8 +data, which requires explicit setup.
1.9 +
1.10 * Isabelle_Process.is_active allows tools to check if the official
1.11 process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop
1.12 (better known as Proof General).
2.1 --- a/doc-src/Classes/Thy/Setup.thy Mon Jun 27 17:04:04 2011 +0200
2.2 +++ b/doc-src/Classes/Thy/Setup.thy Mon Jun 27 22:44:44 2011 +0200
2.3 @@ -5,7 +5,11 @@
2.4 "../../more_antiquote.ML"
2.5 begin
2.6
2.7 -setup {* Code_Target.set_default_code_width 74 *}
2.8 +setup {*
2.9 + Antiquote_Setup.setup #>
2.10 + More_Antiquote.setup #>
2.11 + Code_Target.set_default_code_width 74
2.12 +*}
2.13
2.14 syntax
2.15 "_alpha" :: "type" ("\<alpha>")
3.1 --- a/doc-src/Codegen/Thy/Setup.thy Mon Jun 27 17:04:04 2011 +0200
3.2 +++ b/doc-src/Codegen/Thy/Setup.thy Mon Jun 27 22:44:44 2011 +0200
3.3 @@ -8,6 +8,8 @@
3.4 begin
3.5
3.6 setup {*
3.7 + Antiquote_Setup.setup #>
3.8 + More_Antiquote.setup #>
3.9 let
3.10 val typ = Simple_Syntax.read_typ;
3.11 in
4.1 --- a/doc-src/Codegen/Thy/document/Foundations.tex Mon Jun 27 17:04:04 2011 +0200
4.2 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Mon Jun 27 22:44:44 2011 +0200
4.3 @@ -571,7 +571,7 @@
4.4 language.
4.5
4.6 \ditem{\emph{Inspect code equations}.} Code equations are the central
4.7 - carrier of code generation. Most problems occuring while generating
4.8 + carrier of code generation. Most problems occurring while generating
4.9 code can be traced to single equations which are printed as part of
4.10 the error message. A closer inspection of those may offer the key
4.11 for solving issues (cf.~\secref{sec:equations}).
5.1 --- a/doc-src/IsarImplementation/Thy/Base.thy Mon Jun 27 17:04:04 2011 +0200
5.2 +++ b/doc-src/IsarImplementation/Thy/Base.thy Mon Jun 27 22:44:44 2011 +0200
5.3 @@ -3,4 +3,6 @@
5.4 uses "../../antiquote_setup.ML"
5.5 begin
5.6
5.7 +setup {* Antiquote_Setup.setup *}
5.8 +
5.9 end
6.1 --- a/doc-src/IsarImplementation/Thy/document/Base.tex Mon Jun 27 17:04:04 2011 +0200
6.2 +++ b/doc-src/IsarImplementation/Thy/document/Base.tex Mon Jun 27 22:44:44 2011 +0200
6.3 @@ -11,8 +11,37 @@
6.4 \ Base\isanewline
6.5 \isakeyword{imports}\ Main\isanewline
6.6 \isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
6.7 -\isakeyword{begin}\isanewline
6.8 +\isakeyword{begin}%
6.9 +\endisatagtheory
6.10 +{\isafoldtheory}%
6.11 +%
6.12 +\isadelimtheory
6.13 \isanewline
6.14 +%
6.15 +\endisadelimtheory
6.16 +%
6.17 +\isadelimML
6.18 +\isanewline
6.19 +%
6.20 +\endisadelimML
6.21 +%
6.22 +\isatagML
6.23 +\isacommand{setup}\isamarkupfalse%
6.24 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
6.25 +\endisatagML
6.26 +{\isafoldML}%
6.27 +%
6.28 +\isadelimML
6.29 +\isanewline
6.30 +%
6.31 +\endisadelimML
6.32 +%
6.33 +\isadelimtheory
6.34 +\isanewline
6.35 +%
6.36 +\endisadelimtheory
6.37 +%
6.38 +\isatagtheory
6.39 \isacommand{end}\isamarkupfalse%
6.40 %
6.41 \endisatagtheory
7.1 --- a/doc-src/IsarRef/Thy/Base.thy Mon Jun 27 17:04:04 2011 +0200
7.2 +++ b/doc-src/IsarRef/Thy/Base.thy Mon Jun 27 22:44:44 2011 +0200
7.3 @@ -4,6 +4,7 @@
7.4 begin
7.5
7.6 setup {*
7.7 + Antiquote_Setup.setup #>
7.8 member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup
7.9 *}
7.10
8.1 --- a/doc-src/Main/Docs/Main_Doc.thy Mon Jun 27 17:04:04 2011 +0200
8.2 +++ b/doc-src/Main/Docs/Main_Doc.thy Mon Jun 27 22:44:44 2011 +0200
8.3 @@ -3,16 +3,19 @@
8.4 imports Main
8.5 begin
8.6
8.7 -ML {*
8.8 -fun pretty_term_type_only ctxt (t, T) =
8.9 - (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
8.10 - else error "term_type_only: type mismatch";
8.11 - Syntax.pretty_typ ctxt T)
8.12 -
8.13 -val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
8.14 - (fn {source, context = ctxt, ...} => fn arg =>
8.15 - Thy_Output.output ctxt
8.16 - (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]));
8.17 +setup {*
8.18 + let
8.19 + fun pretty_term_type_only ctxt (t, T) =
8.20 + (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
8.21 + else error "term_type_only: type mismatch";
8.22 + Syntax.pretty_typ ctxt T)
8.23 + in
8.24 + Thy_Output.antiquotation @{binding term_type_only}
8.25 + (Args.term -- Args.typ_abbrev)
8.26 + (fn {source, context = ctxt, ...} => fn arg =>
8.27 + Thy_Output.output ctxt
8.28 + (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]))
8.29 + end
8.30 *}
8.31 (*>*)
8.32 text{*
9.1 --- a/doc-src/System/IsaMakefile Mon Jun 27 17:04:04 2011 +0200
9.2 +++ b/doc-src/System/IsaMakefile Mon Jun 27 22:44:44 2011 +0200
9.3 @@ -22,7 +22,7 @@
9.4 Pure-System: $(LOG)/Pure-System.gz
9.5
9.6 $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \
9.7 - Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy
9.8 + Thy/Base.thy Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy
9.9 @$(USEDIR) -s System Pure Thy
9.10 @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
9.11 Thy/document/pdfsetup.sty Thy/document/session.tex
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/doc-src/System/Thy/Base.thy Mon Jun 27 22:44:44 2011 +0200
10.3 @@ -0,0 +1,10 @@
10.4 +theory Base
10.5 +imports Pure
10.6 +uses "../../antiquote_setup.ML"
10.7 +begin
10.8 +
10.9 +setup {* Antiquote_Setup.setup *}
10.10 +
10.11 +declare [[thy_output_source]]
10.12 +
10.13 +end
11.1 --- a/doc-src/System/Thy/Basics.thy Mon Jun 27 17:04:04 2011 +0200
11.2 +++ b/doc-src/System/Thy/Basics.thy Mon Jun 27 22:44:44 2011 +0200
11.3 @@ -1,5 +1,5 @@
11.4 theory Basics
11.5 -imports Pure
11.6 +imports Base
11.7 begin
11.8
11.9 chapter {* The Isabelle system environment *}
12.1 --- a/doc-src/System/Thy/Interfaces.thy Mon Jun 27 17:04:04 2011 +0200
12.2 +++ b/doc-src/System/Thy/Interfaces.thy Mon Jun 27 22:44:44 2011 +0200
12.3 @@ -1,5 +1,5 @@
12.4 theory Interfaces
12.5 -imports Pure
12.6 +imports Base
12.7 begin
12.8
12.9 chapter {* User interfaces *}
13.1 --- a/doc-src/System/Thy/Misc.thy Mon Jun 27 17:04:04 2011 +0200
13.2 +++ b/doc-src/System/Thy/Misc.thy Mon Jun 27 22:44:44 2011 +0200
13.3 @@ -1,5 +1,5 @@
13.4 theory Misc
13.5 -imports Pure
13.6 +imports Base
13.7 begin
13.8
13.9 chapter {* Miscellaneous tools \label{ch:tools} *}
14.1 --- a/doc-src/System/Thy/Presentation.thy Mon Jun 27 17:04:04 2011 +0200
14.2 +++ b/doc-src/System/Thy/Presentation.thy Mon Jun 27 22:44:44 2011 +0200
14.3 @@ -1,5 +1,5 @@
14.4 theory Presentation
14.5 -imports Pure
14.6 +imports Base
14.7 begin
14.8
14.9 chapter {* Presenting theories \label{ch:present} *}
15.1 --- a/doc-src/System/Thy/ROOT.ML Mon Jun 27 17:04:04 2011 +0200
15.2 +++ b/doc-src/System/Thy/ROOT.ML Mon Jun 27 22:44:44 2011 +0200
15.3 @@ -1,4 +1,1 @@
15.4 -Thy_Output.source_default := true;
15.5 -use "../../antiquote_setup.ML";
15.6 -
15.7 use_thys ["Basics", "Interfaces", "Presentation", "Misc"];
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/doc-src/System/Thy/document/Base.tex Mon Jun 27 22:44:44 2011 +0200
16.3 @@ -0,0 +1,61 @@
16.4 +%
16.5 +\begin{isabellebody}%
16.6 +\def\isabellecontext{Base}%
16.7 +%
16.8 +\isadelimtheory
16.9 +%
16.10 +\endisadelimtheory
16.11 +%
16.12 +\isatagtheory
16.13 +\isacommand{theory}\isamarkupfalse%
16.14 +\ Base\isanewline
16.15 +\isakeyword{imports}\ Pure\isanewline
16.16 +\isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
16.17 +\isakeyword{begin}%
16.18 +\endisatagtheory
16.19 +{\isafoldtheory}%
16.20 +%
16.21 +\isadelimtheory
16.22 +\isanewline
16.23 +%
16.24 +\endisadelimtheory
16.25 +%
16.26 +\isadelimML
16.27 +\isanewline
16.28 +%
16.29 +\endisadelimML
16.30 +%
16.31 +\isatagML
16.32 +\isacommand{setup}\isamarkupfalse%
16.33 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
16.34 +\endisatagML
16.35 +{\isafoldML}%
16.36 +%
16.37 +\isadelimML
16.38 +\isanewline
16.39 +%
16.40 +\endisadelimML
16.41 +\isanewline
16.42 +\isacommand{declare}\isamarkupfalse%
16.43 +\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}thy{\isaliteral{5F}{\isacharunderscore}}output{\isaliteral{5F}{\isacharunderscore}}source{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
16.44 +%
16.45 +\isadelimtheory
16.46 +\isanewline
16.47 +%
16.48 +\endisadelimtheory
16.49 +%
16.50 +\isatagtheory
16.51 +\isacommand{end}\isamarkupfalse%
16.52 +%
16.53 +\endisatagtheory
16.54 +{\isafoldtheory}%
16.55 +%
16.56 +\isadelimtheory
16.57 +\isanewline
16.58 +%
16.59 +\endisadelimtheory
16.60 +\end{isabellebody}%
16.61 +%%% Local Variables:
16.62 +%%% mode: latex
16.63 +%%% TeX-master: "root"
16.64 +%%% End:
17.1 --- a/doc-src/System/Thy/document/Basics.tex Mon Jun 27 17:04:04 2011 +0200
17.2 +++ b/doc-src/System/Thy/document/Basics.tex Mon Jun 27 22:44:44 2011 +0200
17.3 @@ -9,7 +9,7 @@
17.4 \isatagtheory
17.5 \isacommand{theory}\isamarkupfalse%
17.6 \ Basics\isanewline
17.7 -\isakeyword{imports}\ Pure\isanewline
17.8 +\isakeyword{imports}\ Base\isanewline
17.9 \isakeyword{begin}%
17.10 \endisatagtheory
17.11 {\isafoldtheory}%
18.1 --- a/doc-src/System/Thy/document/Interfaces.tex Mon Jun 27 17:04:04 2011 +0200
18.2 +++ b/doc-src/System/Thy/document/Interfaces.tex Mon Jun 27 22:44:44 2011 +0200
18.3 @@ -9,7 +9,7 @@
18.4 \isatagtheory
18.5 \isacommand{theory}\isamarkupfalse%
18.6 \ Interfaces\isanewline
18.7 -\isakeyword{imports}\ Pure\isanewline
18.8 +\isakeyword{imports}\ Base\isanewline
18.9 \isakeyword{begin}%
18.10 \endisatagtheory
18.11 {\isafoldtheory}%
19.1 --- a/doc-src/System/Thy/document/Misc.tex Mon Jun 27 17:04:04 2011 +0200
19.2 +++ b/doc-src/System/Thy/document/Misc.tex Mon Jun 27 22:44:44 2011 +0200
19.3 @@ -9,7 +9,7 @@
19.4 \isatagtheory
19.5 \isacommand{theory}\isamarkupfalse%
19.6 \ Misc\isanewline
19.7 -\isakeyword{imports}\ Pure\isanewline
19.8 +\isakeyword{imports}\ Base\isanewline
19.9 \isakeyword{begin}%
19.10 \endisatagtheory
19.11 {\isafoldtheory}%
20.1 --- a/doc-src/System/Thy/document/Presentation.tex Mon Jun 27 17:04:04 2011 +0200
20.2 +++ b/doc-src/System/Thy/document/Presentation.tex Mon Jun 27 22:44:44 2011 +0200
20.3 @@ -9,7 +9,7 @@
20.4 \isatagtheory
20.5 \isacommand{theory}\isamarkupfalse%
20.6 \ Presentation\isanewline
20.7 -\isakeyword{imports}\ Pure\isanewline
20.8 +\isakeyword{imports}\ Base\isanewline
20.9 \isakeyword{begin}%
20.10 \endisatagtheory
20.11 {\isafoldtheory}%
21.1 --- a/doc-src/TutorialI/Inductive/Advanced.thy Mon Jun 27 17:04:04 2011 +0200
21.2 +++ b/doc-src/TutorialI/Inductive/Advanced.thy Mon Jun 27 22:44:44 2011 +0200
21.3 @@ -1,4 +1,6 @@
21.4 -(*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*)
21.5 +(*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin
21.6 +setup {* Antiquote_Setup.setup *}
21.7 +(*>*)
21.8
21.9 text {*
21.10 The premises of introduction rules may contain universal quantifiers and
22.1 --- a/doc-src/TutorialI/Inductive/Even.thy Mon Jun 27 17:04:04 2011 +0200
22.2 +++ b/doc-src/TutorialI/Inductive/Even.thy Mon Jun 27 22:44:44 2011 +0200
22.3 @@ -1,4 +1,6 @@
22.4 -(*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin(*>*)
22.5 +(*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin
22.6 +setup {* Antiquote_Setup.setup *}
22.7 +(*>*)
22.8
22.9 section{* The Set of Even Numbers *}
22.10
23.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Jun 27 17:04:04 2011 +0200
23.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Jun 27 22:44:44 2011 +0200
23.3 @@ -15,6 +15,19 @@
23.4 %
23.5 \endisadelimtheory
23.6 %
23.7 +\isadelimML
23.8 +%
23.9 +\endisadelimML
23.10 +%
23.11 +\isatagML
23.12 +%
23.13 +\endisatagML
23.14 +{\isafoldML}%
23.15 +%
23.16 +\isadelimML
23.17 +%
23.18 +\endisadelimML
23.19 +%
23.20 \begin{isamarkuptext}%
23.21 The premises of introduction rules may contain universal quantifiers and
23.22 monotone functions. A universal quantifier lets the rule
24.1 --- a/doc-src/TutorialI/Inductive/document/Even.tex Mon Jun 27 17:04:04 2011 +0200
24.2 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Mon Jun 27 22:44:44 2011 +0200
24.3 @@ -15,6 +15,19 @@
24.4 %
24.5 \endisadelimtheory
24.6 %
24.7 +\isadelimML
24.8 +%
24.9 +\endisadelimML
24.10 +%
24.11 +\isatagML
24.12 +%
24.13 +\endisatagML
24.14 +{\isafoldML}%
24.15 +%
24.16 +\isadelimML
24.17 +%
24.18 +\endisadelimML
24.19 +%
24.20 \isamarkupsection{The Set of Even Numbers%
24.21 }
24.22 \isamarkuptrue%
25.1 --- a/doc-src/TutorialI/Protocol/Message.thy Mon Jun 27 17:04:04 2011 +0200
25.2 +++ b/doc-src/TutorialI/Protocol/Message.thy Mon Jun 27 22:44:44 2011 +0200
25.3 @@ -9,6 +9,7 @@
25.4 header{*Theory of Agents and Messages for Security Protocols*}
25.5
25.6 theory Message imports Main uses "../../antiquote_setup.ML" begin
25.7 +setup {* Antiquote_Setup.setup *}
25.8
25.9 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
25.10 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
26.1 --- a/doc-src/TutorialI/Protocol/document/Message.tex Mon Jun 27 17:04:04 2011 +0200
26.2 +++ b/doc-src/TutorialI/Protocol/document/Message.tex Mon Jun 27 22:44:44 2011 +0200
26.3 @@ -15,6 +15,19 @@
26.4 %
26.5 \endisadelimtheory
26.6 %
26.7 +\isadelimML
26.8 +%
26.9 +\endisadelimML
26.10 +%
26.11 +\isatagML
26.12 +%
26.13 +\endisatagML
26.14 +{\isafoldML}%
26.15 +%
26.16 +\isadelimML
26.17 +%
26.18 +\endisadelimML
26.19 +%
26.20 \isadelimproof
26.21 %
26.22 \endisadelimproof
27.1 --- a/doc-src/TutorialI/Types/Setup.thy Mon Jun 27 17:04:04 2011 +0200
27.2 +++ b/doc-src/TutorialI/Types/Setup.thy Mon Jun 27 22:44:44 2011 +0200
27.3 @@ -5,4 +5,7 @@
27.4 "../../more_antiquote.ML"
27.5 begin
27.6
27.7 +setup {* Antiquote_Setup.setup #> More_Antiquote.setup *}
27.8 +
27.9 +
27.10 end
27.11 \ No newline at end of file
28.1 --- a/doc-src/antiquote_setup.ML Mon Jun 27 17:04:04 2011 +0200
28.2 +++ b/doc-src/antiquote_setup.ML Mon Jun 27 22:44:44 2011 +0200
28.3 @@ -4,7 +4,12 @@
28.4 Auxiliary antiquotations for the Isabelle manuals.
28.5 *)
28.6
28.7 -structure Antiquote_Setup: sig end =
28.8 +signature ANTIQUOTE_SETUP =
28.9 +sig
28.10 + val setup: theory -> theory
28.11 +end;
28.12 +
28.13 +structure Antiquote_Setup: ANTIQUOTE_SETUP =
28.14 struct
28.15
28.16 (* misc utils *)
28.17 @@ -35,8 +40,9 @@
28.18
28.19 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
28.20
28.21 -val _ = Thy_Output.antiquotation "verbatim" (Scan.lift Args.name)
28.22 - (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
28.23 +val verbatim_setup =
28.24 + Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
28.25 + (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
28.26
28.27
28.28 (* ML text *)
28.29 @@ -87,42 +93,45 @@
28.30
28.31 in
28.32
28.33 -val _ = index_ml "index_ML" "" ml_val;
28.34 -val _ = index_ml "index_ML_type" "type" ml_type;
28.35 -val _ = index_ml "index_ML_exn" "exception" ml_exn;
28.36 -val _ = index_ml "index_ML_structure" "structure" ml_structure;
28.37 -val _ = index_ml "index_ML_functor" "functor" ml_functor;
28.38 +val index_ml_setup =
28.39 + index_ml @{binding index_ML} "" ml_val #>
28.40 + index_ml @{binding index_ML_type} "type" ml_type #>
28.41 + index_ml @{binding index_ML_exn} "exception" ml_exn #>
28.42 + index_ml @{binding index_ML_structure} "structure" ml_structure #>
28.43 + index_ml @{binding index_ML_functor} "functor" ml_functor;
28.44
28.45 end;
28.46
28.47
28.48 (* named theorems *)
28.49
28.50 -val _ = Thy_Output.antiquotation "named_thms"
28.51 - (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
28.52 - (fn {context = ctxt, ...} =>
28.53 - map (apfst (Thy_Output.pretty_thm ctxt))
28.54 - #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
28.55 - #> (if Config.get ctxt Thy_Output.display
28.56 - then
28.57 - map (fn (p, name) =>
28.58 - Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
28.59 - "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
28.60 - #> space_implode "\\par\\smallskip%\n"
28.61 - #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
28.62 - else
28.63 - map (fn (p, name) =>
28.64 - Output.output (Pretty.str_of p) ^
28.65 - "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
28.66 - #> space_implode "\\par\\smallskip%\n"
28.67 - #> enclose "\\isa{" "}"));
28.68 +val named_thms_setup =
28.69 + Thy_Output.antiquotation @{binding named_thms}
28.70 + (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
28.71 + (fn {context = ctxt, ...} =>
28.72 + map (apfst (Thy_Output.pretty_thm ctxt))
28.73 + #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
28.74 + #> (if Config.get ctxt Thy_Output.display
28.75 + then
28.76 + map (fn (p, name) =>
28.77 + Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
28.78 + "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
28.79 + #> space_implode "\\par\\smallskip%\n"
28.80 + #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
28.81 + else
28.82 + map (fn (p, name) =>
28.83 + Output.output (Pretty.str_of p) ^
28.84 + "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
28.85 + #> space_implode "\\par\\smallskip%\n"
28.86 + #> enclose "\\isa{" "}"));
28.87
28.88
28.89 (* theory file *)
28.90
28.91 -val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
28.92 - (fn {context = ctxt, ...} =>
28.93 - fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
28.94 +val thy_file_setup =
28.95 + Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
28.96 + (fn {context = ctxt, ...} =>
28.97 + fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
28.98
28.99
28.100 (* Isabelle/Isar entities (with index) *)
28.101 @@ -142,8 +151,8 @@
28.102
28.103 fun entity check markup kind index =
28.104 Thy_Output.antiquotation
28.105 - (translate (fn " " => "_" | c => c) kind ^
28.106 - (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))
28.107 + (Binding.name (translate (fn " " => "_" | c => c) kind ^
28.108 + (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
28.109 (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
28.110 (fn {context = ctxt, ...} => fn (logic, name) =>
28.111 let
28.112 @@ -170,30 +179,44 @@
28.113 end);
28.114
28.115 fun entity_antiqs check markup kind =
28.116 - ((entity check markup kind NONE);
28.117 - (entity check markup kind (SOME true));
28.118 - (entity check markup kind (SOME false)));
28.119 + entity check markup kind NONE #>
28.120 + entity check markup kind (SOME true) #>
28.121 + entity check markup kind (SOME false);
28.122
28.123 in
28.124
28.125 -val _ = entity_antiqs no_check "" "syntax";
28.126 -val _ = entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command";
28.127 -val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword";
28.128 -val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "element";
28.129 -val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method";
28.130 -val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute";
28.131 -val _ = entity_antiqs no_check "" "fact";
28.132 -val _ = entity_antiqs no_check "" "variable";
28.133 -val _ = entity_antiqs no_check "" "case";
28.134 -val _ = entity_antiqs (K Thy_Output.defined_command) "" "antiquotation";
28.135 -val _ = entity_antiqs (K Thy_Output.defined_option) "" "antiquotation option";
28.136 -val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
28.137 -val _ = entity_antiqs no_check "" "inference";
28.138 -val _ = entity_antiqs no_check "isatt" "executable";
28.139 -val _ = entity_antiqs (K check_tool) "isatt" "tool";
28.140 -val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
28.141 -val _ = entity_antiqs no_check "" "ML antiquotation"; (* FIXME proper check *)
28.142 +val entity_setup =
28.143 + entity_antiqs no_check "" "syntax" #>
28.144 + entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command" #>
28.145 + entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword" #>
28.146 + entity_antiqs (K Keyword.is_keyword) "isakeyword" "element" #>
28.147 + entity_antiqs (thy_check Method.intern Method.defined) "" "method" #>
28.148 + entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" #>
28.149 + entity_antiqs no_check "" "fact" #>
28.150 + entity_antiqs no_check "" "variable" #>
28.151 + entity_antiqs no_check "" "case" #>
28.152 + entity_antiqs (thy_check Thy_Output.intern_command Thy_Output.defined_command)
28.153 + "" "antiquotation" #>
28.154 + entity_antiqs (thy_check Thy_Output.intern_option Thy_Output.defined_option)
28.155 + "" "antiquotation option" #>
28.156 + entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" #>
28.157 + entity_antiqs no_check "" "inference" #>
28.158 + entity_antiqs no_check "isatt" "executable" #>
28.159 + entity_antiqs (K check_tool) "isatt" "tool" #>
28.160 + entity_antiqs (K (can Thy_Info.get_theory)) "" "theory" #>
28.161 + entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
28.162 + "" Markup.ML_antiquotationN;
28.163
28.164 end;
28.165
28.166 +
28.167 +(* theory setup *)
28.168 +
28.169 +val setup =
28.170 + verbatim_setup #>
28.171 + index_ml_setup #>
28.172 + named_thms_setup #>
28.173 + thy_file_setup #>
28.174 + entity_setup;
28.175 +
28.176 end;
29.1 --- a/doc-src/more_antiquote.ML Mon Jun 27 17:04:04 2011 +0200
29.2 +++ b/doc-src/more_antiquote.ML Mon Jun 27 22:44:44 2011 +0200
29.3 @@ -6,6 +6,7 @@
29.4
29.5 signature MORE_ANTIQUOTE =
29.6 sig
29.7 + val setup: theory -> theory
29.8 end;
29.9
29.10 structure More_Antiquote : MORE_ANTIQUOTE =
29.11 @@ -40,8 +41,9 @@
29.12
29.13 in
29.14
29.15 -val _ = Thy_Output.antiquotation "code_thms" Args.term
29.16 - (fn {source, context, ...} => pretty_code_thm source context);
29.17 +val setup =
29.18 + Thy_Output.antiquotation @{binding code_thms} Args.term
29.19 + (fn {source, context, ...} => pretty_code_thm source context);
29.20
29.21 end;
29.22
30.1 --- a/src/FOL/FOL.thy Mon Jun 27 17:04:04 2011 +0200
30.2 +++ b/src/FOL/FOL.thy Mon Jun 27 22:44:44 2011 +0200
30.3 @@ -177,12 +177,15 @@
30.4 val hyp_subst_tacs = [hyp_subst_tac]
30.5 );
30.6
30.7 -ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
30.8 -
30.9 structure Basic_Classical: BASIC_CLASSICAL = Cla;
30.10 open Basic_Classical;
30.11 *}
30.12
30.13 +setup {*
30.14 + ML_Antiquote.value @{binding claset}
30.15 + (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())")
30.16 +*}
30.17 +
30.18 setup Cla.setup
30.19
30.20 (*Propositional rules*)
31.1 --- a/src/HOL/HOL.thy Mon Jun 27 17:04:04 2011 +0200
31.2 +++ b/src/HOL/HOL.thy Mon Jun 27 22:44:44 2011 +0200
31.3 @@ -853,9 +853,11 @@
31.4
31.5 structure Basic_Classical: BASIC_CLASSICAL = Classical;
31.6 open Basic_Classical;
31.7 +*}
31.8
31.9 -ML_Antiquote.value "claset"
31.10 - (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
31.11 +setup {*
31.12 + ML_Antiquote.value @{binding claset}
31.13 + (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())")
31.14 *}
31.15
31.16 setup Classical.setup
32.1 --- a/src/HOL/Quickcheck_Narrowing.thy Mon Jun 27 17:04:04 2011 +0200
32.2 +++ b/src/HOL/Quickcheck_Narrowing.thy Mon Jun 27 22:44:44 2011 +0200
32.3 @@ -435,6 +435,7 @@
32.4 hide_type code_int narrowing_type narrowing_term cons property
32.5 hide_const int_of of_int nth error toEnum marker empty
32.6 C cons conv nonEmpty "apply" sum ensure_testable all exists
32.7 +hide_const (open) Var Ctr
32.8 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
32.9
32.10
33.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Jun 27 17:04:04 2011 +0200
33.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Jun 27 22:44:44 2011 +0200
33.3 @@ -247,27 +247,28 @@
33.4
33.5 (** document antiquotation **)
33.6
33.7 -val _ = Thy_Output.antiquotation "datatype" (Args.type_name true)
33.8 - (fn {source = src, context = ctxt, ...} => fn dtco =>
33.9 - let
33.10 - val thy = Proof_Context.theory_of ctxt;
33.11 - val (vs, cos) = the_spec thy dtco;
33.12 - val ty = Type (dtco, map TFree vs);
33.13 - val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
33.14 - fun pretty_constr (co, tys) =
33.15 - Pretty.block (Pretty.breaks
33.16 - (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
33.17 - map pretty_typ_bracket tys));
33.18 - val pretty_datatype =
33.19 - Pretty.block
33.20 - (Pretty.command "datatype" :: Pretty.brk 1 ::
33.21 - Syntax.pretty_typ ctxt ty ::
33.22 - Pretty.str " =" :: Pretty.brk 1 ::
33.23 - flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos)));
33.24 - in
33.25 - Thy_Output.output ctxt
33.26 - (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
33.27 - end);
33.28 +val antiq_setup =
33.29 + Thy_Output.antiquotation @{binding datatype} (Args.type_name true)
33.30 + (fn {source = src, context = ctxt, ...} => fn dtco =>
33.31 + let
33.32 + val thy = Proof_Context.theory_of ctxt;
33.33 + val (vs, cos) = the_spec thy dtco;
33.34 + val ty = Type (dtco, map TFree vs);
33.35 + val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
33.36 + fun pretty_constr (co, tys) =
33.37 + Pretty.block (Pretty.breaks
33.38 + (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
33.39 + map pretty_typ_bracket tys));
33.40 + val pretty_datatype =
33.41 + Pretty.block
33.42 + (Pretty.command "datatype" :: Pretty.brk 1 ::
33.43 + Syntax.pretty_typ ctxt ty ::
33.44 + Pretty.str " =" :: Pretty.brk 1 ::
33.45 + flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos)));
33.46 + in
33.47 + Thy_Output.output ctxt
33.48 + (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
33.49 + end);
33.50
33.51
33.52
33.53 @@ -463,6 +464,7 @@
33.54
33.55 val setup =
33.56 trfun_setup #>
33.57 + antiq_setup #>
33.58 Datatype_Interpretation.init;
33.59
33.60
34.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jun 27 17:04:04 2011 +0200
34.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jun 27 22:44:44 2011 +0200
34.3 @@ -320,7 +320,7 @@
34.4 do_formula pos body_t
34.5 #> (if also_skolems andalso will_surely_be_skolemized then
34.6 add_pconst_to_table true
34.7 - (gensym skolem_prefix, PType (order_of_type abs_T, []))
34.8 + (legacy_gensym skolem_prefix, PType (order_of_type abs_T, []))
34.9 else
34.10 I)
34.11 and do_term_or_formula ext_arg T =
35.1 --- a/src/Pure/General/markup.ML Mon Jun 27 17:04:04 2011 +0200
35.2 +++ b/src/Pure/General/markup.ML Mon Jun 27 22:44:44 2011 +0200
35.3 @@ -72,8 +72,9 @@
35.4 val ML_sourceN: string val ML_source: T
35.5 val doc_sourceN: string val doc_source: T
35.6 val antiqN: string val antiq: T
35.7 - val ML_antiqN: string val ML_antiq: string -> T
35.8 - val doc_antiqN: string val doc_antiq: string -> T
35.9 + val ML_antiquotationN: string
35.10 + val doc_antiquotationN: string
35.11 + val doc_antiquotation_optionN: string
35.12 val keyword_declN: string val keyword_decl: string -> T
35.13 val command_declN: string val command_decl: string -> string -> T
35.14 val keywordN: string val keyword: T
35.15 @@ -266,8 +267,9 @@
35.16 val (doc_sourceN, doc_source) = markup_elem "doc_source";
35.17
35.18 val (antiqN, antiq) = markup_elem "antiq";
35.19 -val (ML_antiqN, ML_antiq) = markup_string "ML_antiq" nameN;
35.20 -val (doc_antiqN, doc_antiq) = markup_string "doc_antiq" nameN;
35.21 +val ML_antiquotationN = "ML antiquotation";
35.22 +val doc_antiquotationN = "document antiquotation";
35.23 +val doc_antiquotation_optionN = "document antiquotation option";
35.24
35.25
35.26 (* outer syntax *)
36.1 --- a/src/Pure/General/markup.scala Mon Jun 27 17:04:04 2011 +0200
36.2 +++ b/src/Pure/General/markup.scala Mon Jun 27 22:44:44 2011 +0200
36.3 @@ -189,8 +189,9 @@
36.4 val DOC_SOURCE = "doc_source"
36.5
36.6 val ANTIQ = "antiq"
36.7 - val ML_ANTIQ = "ML_antiq"
36.8 - val DOC_ANTIQ = "doc_antiq"
36.9 + val ML_ANTIQUOTATION = "ML antiquotation"
36.10 + val DOCUMENT_ANTIQUOTATION = "document antiquotation"
36.11 + val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
36.12
36.13
36.14 /* ML syntax */
37.1 --- a/src/Pure/General/name_space.ML Mon Jun 27 17:04:04 2011 +0200
37.2 +++ b/src/Pure/General/name_space.ML Mon Jun 27 22:44:44 2011 +0200
37.3 @@ -50,7 +50,7 @@
37.4 val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
37.5 val alias: naming -> binding -> string -> T -> T
37.6 type 'a table = T * 'a Symtab.table
37.7 - val check: Proof.context -> 'a table -> xstring * Position.T -> string
37.8 + val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
37.9 val get: 'a table -> string -> 'a
37.10 val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
37.11 val empty_table: string -> 'a table
37.12 @@ -383,15 +383,15 @@
37.13
37.14
37.15
37.16 -(** name spaces coupled with symbol tables **)
37.17 +(** name space coupled with symbol table **)
37.18
37.19 type 'a table = T * 'a Symtab.table;
37.20
37.21 fun check ctxt (space, tab) (xname, pos) =
37.22 let val name = intern space xname in
37.23 - if Symtab.defined tab name
37.24 - then (Context_Position.report ctxt pos (markup space name); name)
37.25 - else error (undefined (kind_of space) name ^ Position.str_of pos)
37.26 + (case Symtab.lookup tab name of
37.27 + SOME x => (Context_Position.report ctxt pos (markup space name); (name, x))
37.28 + | NONE => error (undefined (kind_of space) name ^ Position.str_of pos))
37.29 end;
37.30
37.31 fun get (space, tab) name =
38.1 --- a/src/Pure/Isar/isar_cmd.ML Mon Jun 27 17:04:04 2011 +0200
38.2 +++ b/src/Pure/Isar/isar_cmd.ML Mon Jun 27 22:44:44 2011 +0200
38.3 @@ -303,8 +303,12 @@
38.4 Proof.goal (Toplevel.proof_of (diag_state ()))
38.5 handle Toplevel.UNDEF => error "No goal present";
38.6
38.7 -val _ = ML_Antiquote.value "Isar.state" (Scan.succeed "Isar_Cmd.diag_state ()");
38.8 -val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()");
38.9 +val _ =
38.10 + Context.>> (Context.map_theory
38.11 + (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
38.12 + (Scan.succeed "Isar_Cmd.diag_state ()") #>
38.13 + ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
38.14 + (Scan.succeed "Isar_Cmd.diag_goal ()")));
38.15
38.16
38.17 (* present draft files *)
38.18 @@ -380,7 +384,8 @@
38.19 val print_methods = Toplevel.unknown_theory o
38.20 Toplevel.keep (Method.print_methods o Toplevel.theory_of);
38.21
38.22 -val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations;
38.23 +val print_antiquotations =
38.24 + Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of);
38.25
38.26 val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
38.27 let
39.1 --- a/src/Pure/ML/ml_antiquote.ML Mon Jun 27 17:04:04 2011 +0200
39.2 +++ b/src/Pure/ML/ml_antiquote.ML Mon Jun 27 22:44:44 2011 +0200
39.3 @@ -6,11 +6,11 @@
39.4
39.5 signature ML_ANTIQUOTE =
39.6 sig
39.7 - val macro: string -> Proof.context context_parser -> unit
39.8 val variant: string -> Proof.context -> string * Proof.context
39.9 - val inline: string -> string context_parser -> unit
39.10 - val declaration: string -> string -> string context_parser -> unit
39.11 - val value: string -> string context_parser -> unit
39.12 + val macro: binding -> Proof.context context_parser -> theory -> theory
39.13 + val inline: binding -> string context_parser -> theory -> theory
39.14 + val declaration: string -> binding -> string context_parser -> theory -> theory
39.15 + val value: binding -> string context_parser -> theory -> theory
39.16 end;
39.17
39.18 structure ML_Antiquote: ML_ANTIQUOTE =
39.19 @@ -46,7 +46,8 @@
39.20 fun declaration kind name scan = ML_Context.add_antiq name
39.21 (fn _ => scan >> (fn s => fn background =>
39.22 let
39.23 - val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
39.24 + val (a, background') =
39.25 + variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) background;
39.26 val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
39.27 val body = "Isabelle." ^ a;
39.28 in (K (env, body), background') end));
39.29 @@ -57,48 +58,55 @@
39.30
39.31 (** misc antiquotations **)
39.32
39.33 -val _ = inline "assert"
39.34 - (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")");
39.35 +val _ = Context.>> (Context.map_theory
39.36
39.37 -val _ = inline "make_string" (Scan.succeed ml_make_string);
39.38 + (inline (Binding.name "assert")
39.39 + (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
39.40
39.41 -val _ = value "binding"
39.42 - (Scan.lift (Parse.position Args.name)
39.43 - >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
39.44 + inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
39.45
39.46 -val _ = value "theory"
39.47 - (Scan.lift Args.name >> (fn name =>
39.48 - "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
39.49 - || Scan.succeed "ML_Context.the_global_context ()");
39.50 + value (Binding.name "binding")
39.51 + (Scan.lift (Parse.position Args.name)
39.52 + >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))) #>
39.53
39.54 -val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
39.55 + value (Binding.name "theory")
39.56 + (Scan.lift Args.name >> (fn name =>
39.57 + "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
39.58 + || Scan.succeed "ML_Context.the_global_context ()") #>
39.59
39.60 -val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
39.61 -val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
39.62 -val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
39.63 + value (Binding.name "context") (Scan.succeed "ML_Context.the_local_context ()") #>
39.64
39.65 -val _ = macro "let" (Args.context --
39.66 - Scan.lift
39.67 - (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
39.68 - >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt)));
39.69 + inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
39.70 + inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
39.71 + inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
39.72
39.73 -val _ = macro "note" (Args.context :|-- (fn ctxt =>
39.74 - Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
39.75 - ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
39.76 - >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt))));
39.77 + macro (Binding.name "let")
39.78 + (Args.context --
39.79 + Scan.lift
39.80 + (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
39.81 + >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))) #>
39.82
39.83 -val _ = value "ctyp" (Args.typ >> (fn T =>
39.84 - "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
39.85 + macro (Binding.name "note")
39.86 + (Args.context :|-- (fn ctxt =>
39.87 + Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms
39.88 + >> (fn ((a, srcs), ths) =>
39.89 + ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
39.90 + >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #>
39.91
39.92 -val _ = value "cterm" (Args.term >> (fn t =>
39.93 - "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
39.94 + value (Binding.name "ctyp") (Args.typ >> (fn T =>
39.95 + "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
39.96
39.97 -val _ = value "cprop" (Args.prop >> (fn t =>
39.98 - "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
39.99 + value (Binding.name "cterm") (Args.term >> (fn t =>
39.100 + "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
39.101
39.102 -val _ = value "cpat"
39.103 - (Args.context -- Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
39.104 - "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
39.105 + value (Binding.name "cprop") (Args.prop >> (fn t =>
39.106 + "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
39.107 +
39.108 + value (Binding.name "cpat")
39.109 + (Args.context --
39.110 + Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
39.111 + "Thm.cterm_of (ML_Context.the_global_context ()) " ^
39.112 + ML_Syntax.atomic (ML_Syntax.print_term t)))));
39.113
39.114
39.115 (* type classes *)
39.116 @@ -108,11 +116,13 @@
39.117 |> syn ? Lexicon.mark_class
39.118 |> ML_Syntax.print_string);
39.119
39.120 -val _ = inline "class" (class false);
39.121 -val _ = inline "class_syntax" (class true);
39.122 +val _ = Context.>> (Context.map_theory
39.123 + (inline (Binding.name "class") (class false) #>
39.124 + inline (Binding.name "class_syntax") (class true) #>
39.125
39.126 -val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
39.127 - ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
39.128 + inline (Binding.name "sort")
39.129 + (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
39.130 + ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))));
39.131
39.132
39.133 (* type constructors *)
39.134 @@ -128,10 +138,15 @@
39.135 | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos));
39.136 in ML_Syntax.print_string res end);
39.137
39.138 -val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
39.139 -val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
39.140 -val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
39.141 -val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Lexicon.mark_type c));
39.142 +val _ = Context.>> (Context.map_theory
39.143 + (inline (Binding.name "type_name")
39.144 + (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
39.145 + inline (Binding.name "type_abbrev")
39.146 + (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
39.147 + inline (Binding.name "nonterminal")
39.148 + (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
39.149 + inline (Binding.name "type_syntax")
39.150 + (type_name "type" (fn (c, _) => Lexicon.mark_type c))));
39.151
39.152
39.153 (* constants *)
39.154 @@ -144,25 +159,28 @@
39.155 handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
39.156 in ML_Syntax.print_string res end);
39.157
39.158 -val _ = inline "const_name" (const_name (fn (consts, c) => (Consts.the_type consts c; c)));
39.159 -val _ = inline "const_abbrev" (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c)));
39.160 -val _ = inline "const_syntax" (const_name (fn (_, c) => Lexicon.mark_const c));
39.161 +val _ = Context.>> (Context.map_theory
39.162 + (inline (Binding.name "const_name")
39.163 + (const_name (fn (consts, c) => (Consts.the_type consts c; c))) #>
39.164 + inline (Binding.name "const_abbrev")
39.165 + (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
39.166 + inline (Binding.name "const_syntax")
39.167 + (const_name (fn (_, c) => Lexicon.mark_const c)) #>
39.168
39.169 + inline (Binding.name "syntax_const")
39.170 + (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
39.171 + if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
39.172 + then ML_Syntax.print_string c
39.173 + else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))) #>
39.174
39.175 -val _ = inline "syntax_const"
39.176 - (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
39.177 - if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
39.178 - then ML_Syntax.print_string c
39.179 - else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
39.180 -
39.181 -val _ = inline "const"
39.182 - (Args.context -- Scan.lift Args.name_source -- Scan.optional
39.183 - (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
39.184 - >> (fn ((ctxt, raw_c), Ts) =>
39.185 - let
39.186 - val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
39.187 - val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
39.188 - in ML_Syntax.atomic (ML_Syntax.print_term const) end));
39.189 + inline (Binding.name "const")
39.190 + (Args.context -- Scan.lift Args.name_source -- Scan.optional
39.191 + (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
39.192 + >> (fn ((ctxt, raw_c), Ts) =>
39.193 + let
39.194 + val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
39.195 + val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
39.196 + in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
39.197
39.198 end;
39.199
40.1 --- a/src/Pure/ML/ml_context.ML Mon Jun 27 17:04:04 2011 +0200
40.2 +++ b/src/Pure/ML/ml_context.ML Mon Jun 27 22:44:44 2011 +0200
40.3 @@ -24,7 +24,9 @@
40.4 val ml_store_thms: string * thm list -> unit
40.5 val ml_store_thm: string * thm -> unit
40.6 type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
40.7 - val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
40.8 + val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory
40.9 + val intern_antiq: theory -> xstring -> string
40.10 + val defined_antiq: theory -> string -> bool
40.11 val trace_raw: Config.raw
40.12 val trace: bool Config.T
40.13 val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
40.14 @@ -99,29 +101,28 @@
40.15
40.16 type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context;
40.17
40.18 -local
40.19 +structure Antiq_Parsers = Theory_Data
40.20 +(
40.21 + type T = (Position.T -> antiq context_parser) Name_Space.table;
40.22 + val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
40.23 + val extend = I;
40.24 + fun merge data : T = Name_Space.merge_tables data;
40.25 +);
40.26
40.27 -val global_parsers =
40.28 - Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
40.29 +fun add_antiq name scan thy = thy
40.30 + |> Antiq_Parsers.map
40.31 + (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
40.32 + (name, scan) #> snd);
40.33
40.34 -in
40.35 -
40.36 -fun add_antiq name scan = CRITICAL (fn () =>
40.37 - Unsynchronized.change global_parsers (fn tab =>
40.38 - (if not (Symtab.defined tab name) then ()
40.39 - else warning ("Redefined ML antiquotation: " ^ quote name);
40.40 - Symtab.update (name, scan) tab)));
40.41 +val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get;
40.42 +val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get;
40.43
40.44 fun antiquotation src ctxt =
40.45 - let val ((name, _), pos) = Args.dest_src src in
40.46 - (case Symtab.lookup (! global_parsers) name of
40.47 - NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
40.48 - | SOME scan =>
40.49 - (Context_Position.report ctxt pos (Markup.ML_antiq name);
40.50 - Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
40.51 - end;
40.52 -
40.53 -end;
40.54 + let
40.55 + val thy = Proof_Context.theory_of ctxt;
40.56 + val ((xname, _), pos) = Args.dest_src src;
40.57 + val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos);
40.58 + in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end;
40.59
40.60
40.61 (* parsing and evaluation *)
41.1 --- a/src/Pure/ML/ml_thms.ML Mon Jun 27 17:04:04 2011 +0200
41.2 +++ b/src/Pure/ML/ml_thms.ML Mon Jun 27 22:44:44 2011 +0200
41.3 @@ -33,7 +33,7 @@
41.4
41.5 (* fact references *)
41.6
41.7 -fun thm_antiq kind scan = ML_Context.add_antiq kind
41.8 +fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind)
41.9 (fn _ => scan >> (fn ths => fn background =>
41.10 let
41.11 val i = serial ();
41.12 @@ -42,8 +42,10 @@
41.13 val ml = (thm_bind kind a i, "Isabelle." ^ a);
41.14 in (K ml, background') end));
41.15
41.16 -val _ = thm_antiq "thm" (Attrib.thm >> single);
41.17 -val _ = thm_antiq "thms" Attrib.thms;
41.18 +val _ =
41.19 + Context.>> (Context.map_theory
41.20 + (thm_antiq "thm" (Attrib.thm >> single) #>
41.21 + thm_antiq "thms" Attrib.thms));
41.22
41.23
41.24 (* ad-hoc goals *)
41.25 @@ -52,25 +54,27 @@
41.26 val by = Args.$$$ "by";
41.27 val goal = Scan.unless (by || and_) Args.name;
41.28
41.29 -val _ = ML_Context.add_antiq "lemma"
41.30 - (fn _ => Args.context -- Args.mode "open" --
41.31 - Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
41.32 - (by |-- Method.parse -- Scan.option Method.parse)) >>
41.33 - (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
41.34 - let
41.35 - val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
41.36 - val i = serial ();
41.37 - val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
41.38 - fun after_qed res goal_ctxt =
41.39 - put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
41.40 - val ctxt' = ctxt
41.41 - |> Proof.theorem NONE after_qed propss
41.42 - |> Proof.global_terminal_proof methods;
41.43 - val (a, background') = background
41.44 - |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
41.45 - val ml =
41.46 - (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
41.47 - in (K ml, background') end));
41.48 +val _ =
41.49 + Context.>> (Context.map_theory
41.50 + (ML_Context.add_antiq (Binding.name "lemma")
41.51 + (fn _ => Args.context -- Args.mode "open" --
41.52 + Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
41.53 + (by |-- Method.parse -- Scan.option Method.parse)) >>
41.54 + (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
41.55 + let
41.56 + val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
41.57 + val i = serial ();
41.58 + val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
41.59 + fun after_qed res goal_ctxt =
41.60 + put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
41.61 + val ctxt' = ctxt
41.62 + |> Proof.theorem NONE after_qed propss
41.63 + |> Proof.global_terminal_proof methods;
41.64 + val (a, background') = background
41.65 + |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
41.66 + val ml =
41.67 + (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
41.68 + in (K ml, background') end))));
41.69
41.70 end;
41.71
42.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jun 27 17:04:04 2011 +0200
42.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jun 27 22:44:44 2011 +0200
42.3 @@ -41,7 +41,7 @@
42.4 if null ts then Markup.no_output
42.5 else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
42.6 else if name = Markup.sendbackN then (special "W", special "X")
42.7 - else if name = Markup.bindingN then (special "F", special "A")
42.8 + else if name = Markup.bindingN then (special "B", special "A")
42.9 else if name = Markup.hiliteN then (special "0", special "1")
42.10 else if name = Markup.tfreeN then (special "C", special "A")
42.11 else if name = Markup.tvarN then (special "D", special "A")
43.1 --- a/src/Pure/Syntax/syntax.ML Mon Jun 27 17:04:04 2011 +0200
43.2 +++ b/src/Pure/Syntax/syntax.ML Mon Jun 27 22:44:44 2011 +0200
43.3 @@ -369,8 +369,8 @@
43.4 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
43.5 fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
43.6
43.7 -fun read_terms ctxt = map (parse_term ctxt) #> check_terms ctxt;
43.8 -fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt;
43.9 +fun read_terms ctxt = Par_List.map_name "Syntax.read_terms" (parse_term ctxt) #> check_terms ctxt;
43.10 +fun read_props ctxt = Par_List.map_name "Syntax.read_props" (parse_prop ctxt) #> check_props ctxt;
43.11
43.12 val read_term = singleton o read_terms;
43.13 val read_prop = singleton o read_props;
44.1 --- a/src/Pure/Thy/rail.ML Mon Jun 27 17:04:04 2011 +0200
44.2 +++ b/src/Pure/Thy/rail.ML Mon Jun 27 22:44:44 2011 +0200
44.3 @@ -259,8 +259,10 @@
44.4 in
44.5
44.6 val _ =
44.7 - Thy_Output.antiquotation "rail" (Scan.lift (Parse.source_position Parse.string))
44.8 - (fn {state, ...} => output_rules state o read);
44.9 + Context.>> (Context.map_theory
44.10 + (Thy_Output.antiquotation (Binding.name "rail")
44.11 + (Scan.lift (Parse.source_position Parse.string))
44.12 + (fn {state, ...} => output_rules state o read)));
44.13
44.14 end;
44.15
45.1 --- a/src/Pure/Thy/thy_output.ML Mon Jun 27 17:04:04 2011 +0200
45.2 +++ b/src/Pure/Thy/thy_output.ML Mon Jun 27 22:44:44 2011 +0200
45.3 @@ -17,14 +17,17 @@
45.4 val source: bool Config.T
45.5 val break: bool Config.T
45.6 val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
45.7 - val add_option: string -> (string -> Proof.context -> Proof.context) -> unit
45.8 - val defined_command: string -> bool
45.9 - val defined_option: string -> bool
45.10 - val print_antiquotations: unit -> unit
45.11 + val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
45.12 + val intern_command: theory -> xstring -> string
45.13 + val defined_command: theory -> string -> bool
45.14 + val intern_option: theory -> xstring -> string
45.15 + val defined_option: theory -> string -> bool
45.16 + val print_antiquotations: Proof.context -> unit
45.17 + val antiquotation: binding -> 'a context_parser ->
45.18 + ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
45.19 + theory -> theory
45.20 val boolean: string -> bool
45.21 val integer: string -> int
45.22 - val antiquotation: string -> 'a context_parser ->
45.23 - ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> unit
45.24 datatype markup = Markup | MarkupEnv | Verbatim
45.25 val modes: string list Unsynchronized.ref
45.26 val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
45.27 @@ -72,55 +75,66 @@
45.28
45.29 (** maintain global antiquotations **)
45.30
45.31 -local
45.32 +structure Antiquotations = Theory_Data
45.33 +(
45.34 + type T =
45.35 + (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
45.36 + (string -> Proof.context -> Proof.context) Name_Space.table;
45.37 + val empty : T =
45.38 + (Name_Space.empty_table Markup.doc_antiquotationN,
45.39 + Name_Space.empty_table Markup.doc_antiquotation_optionN);
45.40 + val extend = I;
45.41 + fun merge ((commands1, options1), (commands2, options2)) : T =
45.42 + (Name_Space.merge_tables (commands1, commands2),
45.43 + Name_Space.merge_tables (options1, options2));
45.44 +);
45.45
45.46 -val global_commands =
45.47 - Unsynchronized.ref
45.48 - (Symtab.empty: (Args.src -> Toplevel.state -> Proof.context -> string) Symtab.table);
45.49 +fun add_command name cmd thy =
45.50 + thy |> Antiquotations.map
45.51 + (apfst
45.52 + (Name_Space.define
45.53 + (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, cmd) #> snd));
45.54
45.55 -val global_options =
45.56 - Unsynchronized.ref (Symtab.empty: (string -> Proof.context -> Proof.context) Symtab.table);
45.57 +fun add_option name opt thy =
45.58 + thy |> Antiquotations.map
45.59 + (apsnd
45.60 + (Name_Space.define
45.61 + (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, opt) #> snd));
45.62
45.63 -fun add_item kind name item tab =
45.64 - (if not (Symtab.defined tab name) then ()
45.65 - else warning ("Redefined document antiquotation " ^ kind ^ ": " ^ quote name);
45.66 - Symtab.update (name, item) tab);
45.67 +val intern_command = Name_Space.intern o #1 o #1 o Antiquotations.get;
45.68 +val defined_command = Symtab.defined o #2 o #1 o Antiquotations.get;
45.69
45.70 -in
45.71 +val intern_option = Name_Space.intern o #1 o #2 o Antiquotations.get;
45.72 +val defined_option = Symtab.defined o #2 o #2 o Antiquotations.get;
45.73
45.74 -fun add_command name cmd =
45.75 - CRITICAL (fn () => Unsynchronized.change global_commands (add_item "command" name cmd));
45.76 -fun add_option name opt =
45.77 - CRITICAL (fn () => Unsynchronized.change global_options (add_item "option" name opt));
45.78 -
45.79 -fun defined_command name = Symtab.defined (! global_commands) name;
45.80 -fun defined_option name = Symtab.defined (! global_options) name;
45.81 -
45.82 -fun command src =
45.83 - let val ((name, _), pos) = Args.dest_src src in
45.84 - (case Symtab.lookup (! global_commands) name of
45.85 - NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
45.86 - | SOME f =>
45.87 - (Position.report pos (Markup.doc_antiq name);
45.88 - (fn state => fn ctxt => f src state ctxt handle ERROR msg =>
45.89 - cat_error msg ("The error(s) above occurred in document antiquotation: " ^
45.90 - quote name ^ Position.str_of pos))))
45.91 +fun command src state ctxt =
45.92 + let
45.93 + val thy = Proof_Context.theory_of ctxt;
45.94 + val ((xname, _), pos) = Args.dest_src src;
45.95 + val (name, f) = Name_Space.check ctxt (#1 (Antiquotations.get thy)) (xname, pos);
45.96 + in
45.97 + f src state ctxt handle ERROR msg =>
45.98 + cat_error msg ("The error(s) above occurred in document antiquotation: " ^
45.99 + quote name ^ Position.str_of pos)
45.100 end;
45.101
45.102 -fun option (name, s) ctxt =
45.103 - (case Symtab.lookup (! global_options) name of
45.104 - NONE => error ("Unknown document antiquotation option: " ^ quote name)
45.105 - | SOME opt => opt s ctxt);
45.106 +fun option ((xname, pos), s) ctxt =
45.107 + let
45.108 + val thy = Proof_Context.theory_of ctxt;
45.109 + val (_, opt) = Name_Space.check ctxt (#2 (Antiquotations.get thy)) (xname, pos);
45.110 + in opt s ctxt end;
45.111
45.112 -
45.113 -fun print_antiquotations () =
45.114 - [Pretty.big_list "document antiquotation commands:"
45.115 - (map Pretty.str (sort_strings (Symtab.keys (! global_commands)))),
45.116 - Pretty.big_list "document antiquotation options:"
45.117 - (map Pretty.str (sort_strings (Symtab.keys (! global_options))))]
45.118 - |> Pretty.chunks |> Pretty.writeln;
45.119 -
45.120 -end;
45.121 +fun print_antiquotations ctxt =
45.122 + let
45.123 + val thy = Proof_Context.theory_of ctxt;
45.124 + val (commands, options) = Antiquotations.get thy;
45.125 + val command_names = map #1 (Name_Space.extern_table ctxt commands);
45.126 + val option_names = map #1 (Name_Space.extern_table ctxt options);
45.127 + in
45.128 + [Pretty.big_list "document antiquotations:" (map Pretty.str command_names),
45.129 + Pretty.big_list "document antiquotation options:" (map Pretty.str option_names)]
45.130 + |> Pretty.chunks |> Pretty.writeln
45.131 + end;
45.132
45.133 fun antiquotation name scan out =
45.134 add_command name
45.135 @@ -152,7 +166,7 @@
45.136 local
45.137
45.138 val property =
45.139 - Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
45.140 + Parse.position Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
45.141
45.142 val properties =
45.143 Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
45.144 @@ -445,23 +459,25 @@
45.145
45.146 (* options *)
45.147
45.148 -val _ = add_option "show_types" (Config.put show_types o boolean);
45.149 -val _ = add_option "show_sorts" (Config.put show_sorts o boolean);
45.150 -val _ = add_option "show_structs" (Config.put show_structs o boolean);
45.151 -val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
45.152 -val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
45.153 -val _ = add_option "names_long" (Config.put Name_Space.names_long o boolean);
45.154 -val _ = add_option "names_short" (Config.put Name_Space.names_short o boolean);
45.155 -val _ = add_option "names_unique" (Config.put Name_Space.names_unique o boolean);
45.156 -val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
45.157 -val _ = add_option "display" (Config.put display o boolean);
45.158 -val _ = add_option "break" (Config.put break o boolean);
45.159 -val _ = add_option "quotes" (Config.put quotes o boolean);
45.160 -val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single);
45.161 -val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
45.162 -val _ = add_option "indent" (Config.put indent o integer);
45.163 -val _ = add_option "source" (Config.put source o boolean);
45.164 -val _ = add_option "goals_limit" (Config.put Goal_Display.goals_limit o integer);
45.165 +val _ =
45.166 + Context.>> (Context.map_theory
45.167 + (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
45.168 + add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
45.169 + add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
45.170 + add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
45.171 + add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
45.172 + add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
45.173 + add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
45.174 + add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
45.175 + add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
45.176 + add_option (Binding.name "display") (Config.put display o boolean) #>
45.177 + add_option (Binding.name "break") (Config.put break o boolean) #>
45.178 + add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
45.179 + add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
45.180 + add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
45.181 + add_option (Binding.name "indent") (Config.put indent o integer) #>
45.182 + add_option (Binding.name "source") (Config.put source o boolean) #>
45.183 + add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer)));
45.184
45.185
45.186 (* basic pretty printing *)
45.187 @@ -562,22 +578,26 @@
45.188
45.189 in
45.190
45.191 -val _ = basic_entities_style "thm" (Term_Style.parse -- Attrib.thms) pretty_thm_style;
45.192 -val _ = basic_entity "prop" (Term_Style.parse -- Args.prop) pretty_term_style;
45.193 -val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style;
45.194 -val _ = basic_entity "term_type" (Term_Style.parse -- Args.term) pretty_term_typ;
45.195 -val _ = basic_entity "typeof" (Term_Style.parse -- Args.term) pretty_term_typeof;
45.196 -val _ = basic_entity "const" (Args.const_proper false) pretty_const;
45.197 -val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
45.198 -val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
45.199 -val _ = basic_entity "class" (Scan.lift Args.name) pretty_class;
45.200 -val _ = basic_entity "type" (Scan.lift Args.name) pretty_type;
45.201 -val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
45.202 -val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
45.203 -val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
45.204 -val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
45.205 -val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
45.206 -val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
45.207 +val _ =
45.208 + Context.>> (Context.map_theory
45.209 + (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
45.210 + basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
45.211 + basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
45.212 + basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
45.213 + basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
45.214 + basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
45.215 + basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
45.216 + basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
45.217 + basic_entity (Binding.name "class") (Scan.lift Args.name) pretty_class #>
45.218 + basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
45.219 + basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
45.220 + basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
45.221 + basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
45.222 + basic_entity (Binding.name "theory") (Scan.lift Args.name) pretty_theory #>
45.223 + basic_entities_style (Binding.name "thm_style")
45.224 + (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style #>
45.225 + basic_entity (Binding.name "term_style")
45.226 + (Term_Style.parse_bare -- Args.term) pretty_term_style));
45.227
45.228 end;
45.229
45.230 @@ -598,8 +618,10 @@
45.231
45.232 in
45.233
45.234 -val _ = goal_state "goals" true;
45.235 -val _ = goal_state "subgoals" false;
45.236 +val _ =
45.237 + Context.>> (Context.map_theory
45.238 + (goal_state (Binding.name "goals") true #>
45.239 + goal_state (Binding.name "subgoals") false));
45.240
45.241 end;
45.242
45.243 @@ -608,16 +630,19 @@
45.244
45.245 val _ = Keyword.keyword "by";
45.246
45.247 -val _ = antiquotation "lemma"
45.248 - (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
45.249 - (fn {source, context, ...} => fn (prop, methods) =>
45.250 - let
45.251 - val prop_src =
45.252 - (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
45.253 - val _ = context
45.254 - |> Proof.theorem NONE (K I) [[(prop, [])]]
45.255 - |> Proof.global_terminal_proof methods;
45.256 - in output context (maybe_pretty_source pretty_term context prop_src [prop]) end);
45.257 +val _ =
45.258 + Context.>> (Context.map_theory
45.259 + (antiquotation (Binding.name "lemma")
45.260 + (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
45.261 + (fn {source, context, ...} => fn (prop, methods) =>
45.262 + let
45.263 + val prop_src =
45.264 + (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
45.265 + (* FIXME check proof!? *)
45.266 + val _ = context
45.267 + |> Proof.theorem NONE (K I) [[(prop, [])]]
45.268 + |> Proof.global_terminal_proof methods;
45.269 + in output context (maybe_pretty_source pretty_term context prop_src [prop]) end)));
45.270
45.271
45.272 (* ML text *)
45.273 @@ -642,25 +667,30 @@
45.274
45.275 in
45.276
45.277 -val _ = ml_text "ML" (ml_enclose "fn _ => (" ");");
45.278 -val _ = ml_text "ML_type" (ml_enclose "val _ = NONE : (" ") option;");
45.279 -val _ = ml_text "ML_struct" (ml_enclose "functor XXX() = struct structure XX = " " end;");
45.280 +val _ =
45.281 + Context.>> (Context.map_theory
45.282 + (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
45.283 + ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
45.284 + ml_text (Binding.name "ML_struct")
45.285 + (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
45.286
45.287 -val _ = ml_text "ML_functor" (* FIXME formal treatment of functor name (!?) *)
45.288 - (fn pos => fn txt =>
45.289 - ML_Lex.read Position.none ("ML_Env.check_functor " ^
45.290 - ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos)))));
45.291 + ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
45.292 + (fn pos => fn txt =>
45.293 + ML_Lex.read Position.none ("ML_Env.check_functor " ^
45.294 + ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
45.295
45.296 -val _ = ml_text "ML_text" (K (K []));
45.297 + ml_text (Binding.name "ML_text") (K (K []))));
45.298
45.299 end;
45.300
45.301
45.302 (* files *)
45.303
45.304 -val _ = antiquotation "file" (Scan.lift Args.name)
45.305 - (fn {context, ...} => fn path =>
45.306 - if File.exists (Path.explode path) then verb_text path
45.307 - else error ("Bad file: " ^ quote path));
45.308 +val _ =
45.309 + Context.>> (Context.map_theory
45.310 + (antiquotation (Binding.name "file") (Scan.lift Args.name)
45.311 + (fn _ => fn path =>
45.312 + if File.exists (Path.explode path) then verb_text path
45.313 + else error ("Bad file: " ^ quote path))));
45.314
45.315 end;
46.1 --- a/src/Pure/drule.ML Mon Jun 27 17:04:04 2011 +0200
46.2 +++ b/src/Pure/drule.ML Mon Jun 27 22:44:44 2011 +0200
46.3 @@ -313,7 +313,7 @@
46.4 case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
46.5 [] => (fth, fn i => fn x => x) (*No vars: nothing to do!*)
46.6 | vars =>
46.7 - let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix))
46.8 + let fun newName (Var(ix,_)) = (ix, legacy_gensym (string_of_indexname ix))
46.9 val alist = map newName vars
46.10 fun mk_inst (Var(v,T)) =
46.11 (cterm_of thy (Var(v,T)),
47.1 --- a/src/Pure/library.ML Mon Jun 27 17:04:04 2011 +0200
47.2 +++ b/src/Pure/library.ML Mon Jun 27 22:44:44 2011 +0200
47.3 @@ -211,7 +211,7 @@
47.4 'a -> 'b -> 'c * 'b
47.5 val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
47.6 val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
47.7 - val gensym: string -> string
47.8 + val legacy_gensym: string -> string
47.9 type stamp = unit Unsynchronized.ref
47.10 val stamp: unit -> stamp
47.11 type serial = int
47.12 @@ -1043,9 +1043,8 @@
47.13
47.14
47.15
47.16 -(* generating identifiers *)
47.17 +(* generating identifiers -- often fresh *)
47.18
47.19 -(** Freshly generated identifiers; supplied prefix MUST start with a letter **)
47.20 local
47.21 (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
47.22 fun gensym_char i =
47.23 @@ -1059,8 +1058,8 @@
47.24 val gensym_seed = Unsynchronized.ref (0: int);
47.25
47.26 in
47.27 - fun gensym pre =
47.28 - pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed));
47.29 + fun legacy_gensym pre =
47.30 + pre ^ newid (NAMED_CRITICAL "legacy_gensym" (fn () => Unsynchronized.inc gensym_seed));
47.31 end;
47.32
47.33
48.1 --- a/src/Pure/simplifier.ML Mon Jun 27 17:04:04 2011 +0200
48.2 +++ b/src/Pure/simplifier.ML Mon Jun 27 22:44:44 2011 +0200
48.3 @@ -139,8 +139,9 @@
48.4 fun map_simpset f = Context.proof_map (map_ss f);
48.5 fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
48.6
48.7 -val _ = ML_Antiquote.value "simpset"
48.8 - (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
48.9 +val _ = Context.>> (Context.map_theory
48.10 + (ML_Antiquote.value (Binding.name "simpset")
48.11 + (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())")));
48.12
48.13
48.14 (* global simpset *)
48.15 @@ -158,15 +159,16 @@
48.16
48.17 (* get simprocs *)
48.18
48.19 -fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt);
48.20 +fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt) #> #1;
48.21 val the_simproc = Name_Space.get o get_simprocs;
48.22
48.23 val _ =
48.24 - ML_Antiquote.value "simproc"
48.25 - (Args.context -- Scan.lift (Parse.position Args.name)
48.26 - >> (fn (ctxt, name) =>
48.27 - "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^
48.28 - ML_Syntax.print_string (check_simproc ctxt name)));
48.29 + Context.>> (Context.map_theory
48.30 + (ML_Antiquote.value (Binding.name "simproc")
48.31 + (Args.context -- Scan.lift (Parse.position Args.name)
48.32 + >> (fn (ctxt, name) =>
48.33 + "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^
48.34 + ML_Syntax.print_string (check_simproc ctxt name)))));
48.35
48.36
48.37 (* define simprocs *)
49.1 --- a/src/Tools/Code/code_runtime.ML Mon Jun 27 17:04:04 2011 +0200
49.2 +++ b/src/Tools/Code/code_runtime.ML Mon Jun 27 22:44:44 2011 +0200
49.3 @@ -336,7 +336,9 @@
49.4
49.5 (** Isar setup **)
49.6
49.7 -val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
49.8 +val _ =
49.9 + Context.>> (Context.map_theory
49.10 + (ML_Context.add_antiq (Binding.name "code") (fn _ => Args.term >> ml_code_antiq)));
49.11
49.12 local
49.13
50.1 --- a/src/Tools/Code/code_target.ML Mon Jun 27 17:04:04 2011 +0200
50.2 +++ b/src/Tools/Code/code_target.ML Mon Jun 27 22:44:44 2011 +0200
50.3 @@ -60,6 +60,8 @@
50.4 val add_include: string -> string * (string * string list) option -> theory -> theory
50.5
50.6 val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
50.7 +
50.8 + val setup: theory -> theory
50.9 end;
50.10
50.11 structure Code_Target : CODE_TARGET =
50.12 @@ -143,7 +145,7 @@
50.13 };
50.14
50.15 fun make_target ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))) =
50.16 - Target { serial = serial, description = description, reserved = reserved,
50.17 + Target { serial = serial, description = description, reserved = reserved,
50.18 includes = includes, module_alias = module_alias, symbol_syntax = symbol_syntax };
50.19 fun map_target f ( Target { serial, description, reserved, includes, module_alias, symbol_syntax } ) =
50.20 make_target (f ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))));
50.21 @@ -199,7 +201,7 @@
50.22 | _ => true);
50.23 val _ = if overwriting
50.24 then warning ("Overwriting existing target " ^ quote target)
50.25 - else ();
50.26 + else ();
50.27 in
50.28 thy
50.29 |> (Targets.map o apfst o apfst o Symtab.update)
50.30 @@ -251,7 +253,7 @@
50.31 fun collapse_hierarchy thy =
50.32 let
50.33 val ((targets, _), _) = Targets.get thy;
50.34 - fun collapse target =
50.35 + fun collapse target =
50.36 let
50.37 val data = case Symtab.lookup targets target
50.38 of SOME data => data
50.39 @@ -352,7 +354,7 @@
50.40 val serializer = case the_description data
50.41 of Fundamental seri => #serializer seri;
50.42 val reserved = the_reserved data;
50.43 - val module_alias = the_module_alias data
50.44 + val module_alias = the_module_alias data
50.45 val { class, instance, tyco, const } = the_symbol_syntax data;
50.46 val literals = the_literals thy target;
50.47 val (prepared_serializer, prepared_program) = prepare_serializer thy
50.48 @@ -396,7 +398,7 @@
50.49 val { env_var, make_destination, make_command } =
50.50 (#check o the_fundamental thy) target;
50.51 fun ext_check p =
50.52 - let
50.53 + let
50.54 val destination = make_destination p;
50.55 val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
50.56 module_name args naming program names_cs);
50.57 @@ -495,7 +497,7 @@
50.58 fun parse_names category parse internalize lookup =
50.59 Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
50.60 >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs);
50.61 -
50.62 +
50.63 val parse_consts = parse_names "consts" Args.term
50.64 Code.check_const Code_Thingol.lookup_const ;
50.65
50.66 @@ -511,15 +513,17 @@
50.67
50.68 in
50.69
50.70 -val _ = Thy_Output.antiquotation "code_stmts"
50.71 - (parse_const_terms -- Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
50.72 - -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
50.73 - (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
50.74 - let val thy = Proof_Context.theory_of ctxt in
50.75 - present_code thy (mk_cs thy)
50.76 - (fn naming => maps (fn f => f thy naming) mk_stmtss)
50.77 - target some_width "Example" []
50.78 - end);
50.79 +val antiq_setup =
50.80 + Thy_Output.antiquotation @{binding code_stmts}
50.81 + (parse_const_terms --
50.82 + Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
50.83 + -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
50.84 + (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
50.85 + let val thy = Proof_Context.theory_of ctxt in
50.86 + present_code thy (mk_cs thy)
50.87 + (fn naming => maps (fn f => f thy naming) mk_stmtss)
50.88 + target some_width "Example" []
50.89 + end);
50.90
50.91 end;
50.92
50.93 @@ -745,4 +749,9 @@
50.94 | NONE => error ("Bad directive " ^ quote cmd_expr)
50.95 end;
50.96
50.97 +
50.98 +(** theory setup **)
50.99 +
50.100 +val setup = antiq_setup;
50.101 +
50.102 end; (*struct*)
51.1 --- a/src/Tools/Code_Generator.thy Mon Jun 27 17:04:04 2011 +0200
51.2 +++ b/src/Tools/Code_Generator.thy Mon Jun 27 22:44:44 2011 +0200
51.3 @@ -29,6 +29,7 @@
51.4 Solve_Direct.setup
51.5 #> Code_Preproc.setup
51.6 #> Code_Simp.setup
51.7 + #> Code_Target.setup
51.8 #> Code_ML.setup
51.9 #> Code_Haskell.setup
51.10 #> Code_Scala.setup
52.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala Mon Jun 27 17:04:04 2011 +0200
52.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Mon Jun 27 22:44:44 2011 +0200
52.3 @@ -114,7 +114,10 @@
52.4 Map(
52.5 Markup.CLASS -> get_color("red"),
52.6 Markup.TYPE -> get_color("black"),
52.7 - Markup.CONSTANT -> get_color("black"))
52.8 + Markup.CONSTANT -> get_color("black"),
52.9 + Markup.ML_ANTIQUOTATION -> get_color("black"),
52.10 + Markup.DOCUMENT_ANTIQUOTATION -> get_color("black"),
52.11 + Markup.DOCUMENT_ANTIQUOTATION_OPTION -> get_color("black"))
52.12
52.13 private val text_colors: Map[String, Color] =
52.14 Map(