merged
authorwenzelm
Mon Jun 27 22:44:44 2011 +0200 (2011-06-27)
changeset 43581c3e4d280bdeb
parent 43580 023a1d1f97bd
parent 43565 486b56f2139c
child 43583 4d375d0fa4b0
merged
NEWS
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
     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 + (inline (Binding.name "assert")
   39.38 +    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
   39.39  
   39.40 -val _ = inline "make_string" (Scan.succeed ml_make_string);
   39.41 +  inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
   39.42  
   39.43 -val _ = value "binding"
   39.44 -  (Scan.lift (Parse.position Args.name)
   39.45 -    >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
   39.46 +  value (Binding.name "binding")
   39.47 +    (Scan.lift (Parse.position Args.name)
   39.48 +      >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))) #>
   39.49  
   39.50 -val _ = value "theory"
   39.51 -  (Scan.lift Args.name >> (fn name =>
   39.52 -    "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
   39.53 -  || Scan.succeed "ML_Context.the_global_context ()");
   39.54 +  value (Binding.name "theory")
   39.55 +    (Scan.lift Args.name >> (fn name =>
   39.56 +      "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
   39.57 +    || Scan.succeed "ML_Context.the_global_context ()") #>
   39.58  
   39.59 -val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
   39.60 +  value (Binding.name "context") (Scan.succeed "ML_Context.the_local_context ()") #>
   39.61  
   39.62 -val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
   39.63 -val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
   39.64 -val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
   39.65 +  inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
   39.66 +  inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
   39.67 +  inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
   39.68  
   39.69 -val _ = macro "let" (Args.context --
   39.70 -  Scan.lift
   39.71 -    (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
   39.72 -    >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt)));
   39.73 +  macro (Binding.name "let")
   39.74 +    (Args.context --
   39.75 +      Scan.lift
   39.76 +        (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
   39.77 +        >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))) #>
   39.78  
   39.79 -val _ = macro "note" (Args.context :|-- (fn ctxt =>
   39.80 -  Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
   39.81 -    ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
   39.82 -  >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt))));
   39.83 +  macro (Binding.name "note")
   39.84 +    (Args.context :|-- (fn ctxt =>
   39.85 +      Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms
   39.86 +        >> (fn ((a, srcs), ths) =>
   39.87 +          ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
   39.88 +      >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #>
   39.89  
   39.90 -val _ = value "ctyp" (Args.typ >> (fn T =>
   39.91 -  "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
   39.92 +  value (Binding.name "ctyp") (Args.typ >> (fn T =>
   39.93 +    "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
   39.94  
   39.95 -val _ = value "cterm" (Args.term >> (fn t =>
   39.96 -  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
   39.97 +  value (Binding.name "cterm") (Args.term >> (fn t =>
   39.98 +  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   39.99  
  39.100 -val _ = value "cprop" (Args.prop >> (fn t =>
  39.101 -  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
  39.102 +  value (Binding.name "cprop") (Args.prop >> (fn t =>
  39.103 +  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
  39.104  
  39.105 -val _ = value "cpat"
  39.106 -  (Args.context -- Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
  39.107 -    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
  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 -
  39.162 +val _ = Context.>> (Context.map_theory
  39.163 + (inline (Binding.name "const_name")
  39.164 +    (const_name (fn (consts, c) => (Consts.the_type consts c; c))) #>
  39.165 +  inline (Binding.name "const_abbrev")
  39.166 +    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
  39.167 +  inline (Binding.name "const_syntax")
  39.168 +    (const_name (fn (_, c) => Lexicon.mark_const c)) #>
  39.169  
  39.170 -val _ = inline "syntax_const"
  39.171 -  (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
  39.172 -    if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
  39.173 -    then ML_Syntax.print_string c
  39.174 -    else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
  39.175 +  inline (Binding.name "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 -
   40.20 -val global_parsers =
   40.21 -  Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
   40.22 +structure Antiq_Parsers = Theory_Data
   40.23 +(
   40.24 +  type T = (Position.T -> antiq context_parser) Name_Space.table;
   40.25 +  val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
   40.26 +  val extend = I;
   40.27 +  fun merge data : T = Name_Space.merge_tables data;
   40.28 +);
   40.29  
   40.30 -in
   40.31 +fun add_antiq name scan thy = thy
   40.32 +  |> Antiq_Parsers.map
   40.33 +    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
   40.34 +      (name, scan) #> snd);
   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 -
   45.33 -val global_commands =
   45.34 -  Unsynchronized.ref
   45.35 -    (Symtab.empty: (Args.src -> Toplevel.state -> Proof.context -> string) Symtab.table);
   45.36 +structure Antiquotations = Theory_Data
   45.37 +(
   45.38 +  type T =
   45.39 +    (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
   45.40 +      (string -> Proof.context -> Proof.context) Name_Space.table;
   45.41 +  val empty : T =
   45.42 +    (Name_Space.empty_table Markup.doc_antiquotationN,
   45.43 +      Name_Space.empty_table Markup.doc_antiquotation_optionN);
   45.44 +  val extend = I;
   45.45 +  fun merge ((commands1, options1), (commands2, options2)) : T =
   45.46 +    (Name_Space.merge_tables (commands1, commands2),
   45.47 +      Name_Space.merge_tables (options1, options2));
   45.48 +);
   45.49  
   45.50 -val global_options =
   45.51 -  Unsynchronized.ref (Symtab.empty: (string -> Proof.context -> Proof.context) Symtab.table);
   45.52 -
   45.53 -fun add_item kind name item tab =
   45.54 - (if not (Symtab.defined tab name) then ()
   45.55 -  else warning ("Redefined document antiquotation " ^ kind ^ ": " ^ quote name);
   45.56 -  Symtab.update (name, item) tab);
   45.57 -
   45.58 -in
   45.59 +fun add_command name cmd thy =
   45.60 +  thy |> Antiquotations.map
   45.61 +    (apfst
   45.62 +      (Name_Space.define
   45.63 +        (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, cmd) #> snd));
   45.64  
   45.65 -fun add_command name cmd =
   45.66 -  CRITICAL (fn () => Unsynchronized.change global_commands (add_item "command" name cmd));
   45.67 -fun add_option name opt =
   45.68 -  CRITICAL (fn () => Unsynchronized.change global_options (add_item "option" name opt));
   45.69 +fun add_option name opt thy =
   45.70 +  thy |> Antiquotations.map
   45.71 +    (apsnd
   45.72 +      (Name_Space.define
   45.73 +        (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, opt) #> snd));
   45.74  
   45.75 -fun defined_command name = Symtab.defined (! global_commands) name;
   45.76 -fun defined_option name = Symtab.defined (! global_options) name;
   45.77 +val intern_command = Name_Space.intern o #1 o #1 o Antiquotations.get;
   45.78 +val defined_command = Symtab.defined o #2 o #1 o Antiquotations.get;
   45.79  
   45.80 -fun command src =
   45.81 -  let val ((name, _), pos) = Args.dest_src src in
   45.82 -    (case Symtab.lookup (! global_commands) name of
   45.83 -      NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
   45.84 -    | SOME f =>
   45.85 -       (Position.report pos (Markup.doc_antiq name);
   45.86 -        (fn state => fn ctxt => f src state ctxt handle ERROR msg =>
   45.87 -          cat_error msg ("The error(s) above occurred in document antiquotation: " ^
   45.88 -            quote name ^ Position.str_of pos))))
   45.89 +val intern_option = Name_Space.intern o #1 o #2 o Antiquotations.get;
   45.90 +val defined_option = Symtab.defined o #2 o #2 o Antiquotations.get;
   45.91 +
   45.92 +fun command src state ctxt =
   45.93 +  let
   45.94 +    val thy = Proof_Context.theory_of ctxt;
   45.95 +    val ((xname, _), pos) = Args.dest_src src;
   45.96 +    val (name, f) = Name_Space.check ctxt (#1 (Antiquotations.get thy)) (xname, pos);
   45.97 +  in
   45.98 +    f src state ctxt handle ERROR msg =>
   45.99 +      cat_error msg ("The error(s) above occurred in document antiquotation: " ^
  45.100 +        quote name ^ Position.str_of pos)
  45.101    end;
  45.102  
  45.103 -fun option (name, s) ctxt =
  45.104 -  (case Symtab.lookup (! global_options) name of
  45.105 -    NONE => error ("Unknown document antiquotation option: " ^ quote name)
  45.106 -  | SOME opt => opt s ctxt);
  45.107 -
  45.108 +fun option ((xname, pos), s) ctxt =
  45.109 +  let
  45.110 +    val thy = Proof_Context.theory_of ctxt;
  45.111 +    val (_, opt) = Name_Space.check ctxt (#2 (Antiquotations.get thy)) (xname, pos);
  45.112 +  in opt s ctxt end;
  45.113  
  45.114 -fun print_antiquotations () =
  45.115 - [Pretty.big_list "document antiquotation commands:"
  45.116 -    (map Pretty.str (sort_strings (Symtab.keys (! global_commands)))),
  45.117 -  Pretty.big_list "document antiquotation options:"
  45.118 -    (map Pretty.str (sort_strings (Symtab.keys (! global_options))))]
  45.119 - |> Pretty.chunks |> Pretty.writeln;
  45.120 -
  45.121 -end;
  45.122 +fun print_antiquotations ctxt =
  45.123 +  let
  45.124 +    val thy = Proof_Context.theory_of ctxt;
  45.125 +    val (commands, options) = Antiquotations.get thy;
  45.126 +    val command_names = map #1 (Name_Space.extern_table ctxt commands);
  45.127 +    val option_names = map #1 (Name_Space.extern_table ctxt options);
  45.128 +  in
  45.129 +    [Pretty.big_list "document antiquotations:" (map Pretty.str command_names),
  45.130 +      Pretty.big_list "document antiquotation options:" (map Pretty.str option_names)]
  45.131 +    |> Pretty.chunks |> Pretty.writeln
  45.132 +  end;
  45.133  
  45.134  fun antiquotation name scan out =
  45.135    add_command name
  45.136 @@ -152,7 +166,7 @@
  45.137  local
  45.138  
  45.139  val property =
  45.140 -  Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
  45.141 +  Parse.position Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
  45.142  
  45.143  val properties =
  45.144    Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
  45.145 @@ -445,23 +459,25 @@
  45.146  
  45.147  (* options *)
  45.148  
  45.149 -val _ = add_option "show_types" (Config.put show_types o boolean);
  45.150 -val _ = add_option "show_sorts" (Config.put show_sorts o boolean);
  45.151 -val _ = add_option "show_structs" (Config.put show_structs o boolean);
  45.152 -val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
  45.153 -val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
  45.154 -val _ = add_option "names_long" (Config.put Name_Space.names_long o boolean);
  45.155 -val _ = add_option "names_short" (Config.put Name_Space.names_short o boolean);
  45.156 -val _ = add_option "names_unique" (Config.put Name_Space.names_unique o boolean);
  45.157 -val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
  45.158 -val _ = add_option "display" (Config.put display o boolean);
  45.159 -val _ = add_option "break" (Config.put break o boolean);
  45.160 -val _ = add_option "quotes" (Config.put quotes o boolean);
  45.161 -val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single);
  45.162 -val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
  45.163 -val _ = add_option "indent" (Config.put indent o integer);
  45.164 -val _ = add_option "source" (Config.put source o boolean);
  45.165 -val _ = add_option "goals_limit" (Config.put Goal_Display.goals_limit o integer);
  45.166 +val _ =
  45.167 +  Context.>> (Context.map_theory
  45.168 +   (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
  45.169 +    add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
  45.170 +    add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
  45.171 +    add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
  45.172 +    add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
  45.173 +    add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
  45.174 +    add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
  45.175 +    add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
  45.176 +    add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
  45.177 +    add_option (Binding.name "display") (Config.put display o boolean) #>
  45.178 +    add_option (Binding.name "break") (Config.put break o boolean) #>
  45.179 +    add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
  45.180 +    add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
  45.181 +    add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
  45.182 +    add_option (Binding.name "indent") (Config.put indent o integer) #>
  45.183 +    add_option (Binding.name "source") (Config.put source o boolean) #>
  45.184 +    add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer)));
  45.185  
  45.186  
  45.187  (* basic pretty printing *)
  45.188 @@ -562,22 +578,26 @@
  45.189  
  45.190  in
  45.191  
  45.192 -val _ = basic_entities_style "thm" (Term_Style.parse -- Attrib.thms) pretty_thm_style;
  45.193 -val _ = basic_entity "prop" (Term_Style.parse -- Args.prop) pretty_term_style;
  45.194 -val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style;
  45.195 -val _ = basic_entity "term_type" (Term_Style.parse -- Args.term) pretty_term_typ;
  45.196 -val _ = basic_entity "typeof" (Term_Style.parse -- Args.term) pretty_term_typeof;
  45.197 -val _ = basic_entity "const" (Args.const_proper false) pretty_const;
  45.198 -val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
  45.199 -val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
  45.200 -val _ = basic_entity "class" (Scan.lift Args.name) pretty_class;
  45.201 -val _ = basic_entity "type" (Scan.lift Args.name) pretty_type;
  45.202 -val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
  45.203 -val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
  45.204 -val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
  45.205 -val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
  45.206 -val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
  45.207 -val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
  45.208 +val _ =
  45.209 +  Context.>> (Context.map_theory
  45.210 +   (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
  45.211 +    basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
  45.212 +    basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
  45.213 +    basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
  45.214 +    basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
  45.215 +    basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
  45.216 +    basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
  45.217 +    basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
  45.218 +    basic_entity (Binding.name "class") (Scan.lift Args.name) pretty_class #>
  45.219 +    basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
  45.220 +    basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
  45.221 +    basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
  45.222 +    basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
  45.223 +    basic_entity (Binding.name "theory") (Scan.lift Args.name) pretty_theory #>
  45.224 +    basic_entities_style (Binding.name "thm_style")
  45.225 +      (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style #>
  45.226 +    basic_entity (Binding.name "term_style")
  45.227 +      (Term_Style.parse_bare -- Args.term) pretty_term_style));
  45.228  
  45.229  end;
  45.230  
  45.231 @@ -598,8 +618,10 @@
  45.232  
  45.233  in
  45.234  
  45.235 -val _ = goal_state "goals" true;
  45.236 -val _ = goal_state "subgoals" false;
  45.237 +val _ =
  45.238 +  Context.>> (Context.map_theory
  45.239 +   (goal_state (Binding.name "goals") true #>
  45.240 +    goal_state (Binding.name "subgoals") false));
  45.241  
  45.242  end;
  45.243  
  45.244 @@ -608,16 +630,19 @@
  45.245  
  45.246  val _ = Keyword.keyword "by";
  45.247  
  45.248 -val _ = antiquotation "lemma"
  45.249 -  (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
  45.250 -  (fn {source, context, ...} => fn (prop, methods) =>
  45.251 -    let
  45.252 -      val prop_src =
  45.253 -        (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
  45.254 -      val _ = context
  45.255 -        |> Proof.theorem NONE (K I) [[(prop, [])]]
  45.256 -        |> Proof.global_terminal_proof methods;
  45.257 -    in output context (maybe_pretty_source pretty_term context prop_src [prop]) end);
  45.258 +val _ =
  45.259 +  Context.>> (Context.map_theory
  45.260 +   (antiquotation (Binding.name "lemma")
  45.261 +    (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
  45.262 +    (fn {source, context, ...} => fn (prop, methods) =>
  45.263 +      let
  45.264 +        val prop_src =
  45.265 +          (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
  45.266 +        (* FIXME check proof!? *)
  45.267 +        val _ = context
  45.268 +          |> Proof.theorem NONE (K I) [[(prop, [])]]
  45.269 +          |> Proof.global_terminal_proof methods;
  45.270 +      in output context (maybe_pretty_source pretty_term context prop_src [prop]) end)));
  45.271  
  45.272  
  45.273  (* ML text *)
  45.274 @@ -642,25 +667,30 @@
  45.275  
  45.276  in
  45.277  
  45.278 -val _ = ml_text "ML" (ml_enclose "fn _ => (" ");");
  45.279 -val _ = ml_text "ML_type" (ml_enclose "val _ = NONE : (" ") option;");
  45.280 -val _ = ml_text "ML_struct" (ml_enclose "functor XXX() = struct structure XX = " " end;");
  45.281 +val _ =
  45.282 +  Context.>> (Context.map_theory
  45.283 +   (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
  45.284 +    ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
  45.285 +    ml_text (Binding.name "ML_struct")
  45.286 +      (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
  45.287  
  45.288 -val _ = ml_text "ML_functor"   (* FIXME formal treatment of functor name (!?) *)
  45.289 -  (fn pos => fn txt =>
  45.290 -    ML_Lex.read Position.none ("ML_Env.check_functor " ^
  45.291 -      ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos)))));
  45.292 +    ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
  45.293 +      (fn pos => fn txt =>
  45.294 +        ML_Lex.read Position.none ("ML_Env.check_functor " ^
  45.295 +          ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
  45.296  
  45.297 -val _ = ml_text "ML_text" (K (K []));
  45.298 +    ml_text (Binding.name "ML_text") (K (K []))));
  45.299  
  45.300  end;
  45.301  
  45.302  
  45.303  (* files *)
  45.304  
  45.305 -val _ = antiquotation "file" (Scan.lift Args.name)
  45.306 -  (fn {context, ...} => fn path =>
  45.307 -    if File.exists (Path.explode path) then verb_text path
  45.308 -    else error ("Bad file: " ^ quote path));
  45.309 +val _ =
  45.310 +  Context.>> (Context.map_theory
  45.311 +   (antiquotation (Binding.name "file") (Scan.lift Args.name)
  45.312 +    (fn _ => fn path =>
  45.313 +      if File.exists (Path.explode path) then verb_text path
  45.314 +      else error ("Bad file: " ^ quote path))));
  45.315  
  45.316  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(