document antiquotations are managed as theory data, with proper name space and entity markup;
authorwenzelm
Mon Jun 27 22:20:49 2011 +0200 (2011-06-27)
changeset 435649864182c6bad
parent 43563 aeabb735883a
child 43565 486b56f2139c
document antiquotations are managed as theory data, with proper name space and entity markup;
doc-src/Classes/Thy/Setup.thy
doc-src/Codegen/Thy/Setup.thy
doc-src/IsarImplementation/Thy/Base.thy
doc-src/IsarImplementation/Thy/document/Base.tex
doc-src/IsarRef/Thy/Base.thy
doc-src/Main/Docs/Main_Doc.thy
doc-src/System/IsaMakefile
doc-src/System/Thy/Base.thy
doc-src/System/Thy/Basics.thy
doc-src/System/Thy/Interfaces.thy
doc-src/System/Thy/Misc.thy
doc-src/System/Thy/Presentation.thy
doc-src/System/Thy/ROOT.ML
doc-src/System/Thy/document/Base.tex
doc-src/System/Thy/document/Basics.tex
doc-src/System/Thy/document/Interfaces.tex
doc-src/System/Thy/document/Misc.tex
doc-src/System/Thy/document/Presentation.tex
doc-src/TutorialI/Inductive/Advanced.thy
doc-src/TutorialI/Inductive/Even.thy
doc-src/TutorialI/Inductive/document/Advanced.tex
doc-src/TutorialI/Inductive/document/Even.tex
doc-src/TutorialI/Protocol/Message.thy
doc-src/TutorialI/Protocol/document/Message.tex
doc-src/TutorialI/Types/Setup.thy
doc-src/antiquote_setup.ML
doc-src/more_antiquote.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/Isar/isar_cmd.ML
src/Pure/Thy/rail.ML
src/Pure/Thy/thy_output.ML
src/Tools/Code/code_target.ML
src/Tools/Code_Generator.thy
src/Tools/jEdit/src/isabelle_markup.scala
     1.1 --- a/doc-src/Classes/Thy/Setup.thy	Mon Jun 27 17:51:28 2011 +0200
     1.2 +++ b/doc-src/Classes/Thy/Setup.thy	Mon Jun 27 22:20:49 2011 +0200
     1.3 @@ -5,7 +5,11 @@
     1.4    "../../more_antiquote.ML"
     1.5  begin
     1.6  
     1.7 -setup {* Code_Target.set_default_code_width 74 *}
     1.8 +setup {*
     1.9 +  Antiquote_Setup.setup #>
    1.10 +  More_Antiquote.setup #>
    1.11 +  Code_Target.set_default_code_width 74
    1.12 +*}
    1.13  
    1.14  syntax
    1.15    "_alpha" :: "type"  ("\<alpha>")
     2.1 --- a/doc-src/Codegen/Thy/Setup.thy	Mon Jun 27 17:51:28 2011 +0200
     2.2 +++ b/doc-src/Codegen/Thy/Setup.thy	Mon Jun 27 22:20:49 2011 +0200
     2.3 @@ -8,6 +8,8 @@
     2.4  begin
     2.5  
     2.6  setup {*
     2.7 +  Antiquote_Setup.setup #>
     2.8 +  More_Antiquote.setup #>
     2.9  let
    2.10    val typ = Simple_Syntax.read_typ;
    2.11  in
     3.1 --- a/doc-src/IsarImplementation/Thy/Base.thy	Mon Jun 27 17:51:28 2011 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/Base.thy	Mon Jun 27 22:20:49 2011 +0200
     3.3 @@ -3,4 +3,6 @@
     3.4  uses "../../antiquote_setup.ML"
     3.5  begin
     3.6  
     3.7 +setup {* Antiquote_Setup.setup *}
     3.8 +
     3.9  end
     4.1 --- a/doc-src/IsarImplementation/Thy/document/Base.tex	Mon Jun 27 17:51:28 2011 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/Base.tex	Mon Jun 27 22:20:49 2011 +0200
     4.3 @@ -11,8 +11,37 @@
     4.4  \ Base\isanewline
     4.5  \isakeyword{imports}\ Main\isanewline
     4.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
     4.7 -\isakeyword{begin}\isanewline
     4.8 +\isakeyword{begin}%
     4.9 +\endisatagtheory
    4.10 +{\isafoldtheory}%
    4.11 +%
    4.12 +\isadelimtheory
    4.13 +\isanewline
    4.14 +%
    4.15 +\endisadelimtheory
    4.16 +%
    4.17 +\isadelimML
    4.18  \isanewline
    4.19 +%
    4.20 +\endisadelimML
    4.21 +%
    4.22 +\isatagML
    4.23 +\isacommand{setup}\isamarkupfalse%
    4.24 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
    4.25 +\endisatagML
    4.26 +{\isafoldML}%
    4.27 +%
    4.28 +\isadelimML
    4.29 +\isanewline
    4.30 +%
    4.31 +\endisadelimML
    4.32 +%
    4.33 +\isadelimtheory
    4.34 +\isanewline
    4.35 +%
    4.36 +\endisadelimtheory
    4.37 +%
    4.38 +\isatagtheory
    4.39  \isacommand{end}\isamarkupfalse%
    4.40  %
    4.41  \endisatagtheory
     5.1 --- a/doc-src/IsarRef/Thy/Base.thy	Mon Jun 27 17:51:28 2011 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/Base.thy	Mon Jun 27 22:20:49 2011 +0200
     5.3 @@ -4,6 +4,7 @@
     5.4  begin
     5.5  
     5.6  setup {*
     5.7 +  Antiquote_Setup.setup #>
     5.8    member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup
     5.9  *}
    5.10  
     6.1 --- a/doc-src/Main/Docs/Main_Doc.thy	Mon Jun 27 17:51:28 2011 +0200
     6.2 +++ b/doc-src/Main/Docs/Main_Doc.thy	Mon Jun 27 22:20:49 2011 +0200
     6.3 @@ -3,16 +3,19 @@
     6.4  imports Main
     6.5  begin
     6.6  
     6.7 -ML {*
     6.8 -fun pretty_term_type_only ctxt (t, T) =
     6.9 -  (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
    6.10 -   else error "term_type_only: type mismatch";
    6.11 -   Syntax.pretty_typ ctxt T)
    6.12 -
    6.13 -val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
    6.14 -  (fn {source, context = ctxt, ...} => fn arg =>
    6.15 -    Thy_Output.output ctxt
    6.16 -      (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]));
    6.17 +setup {*
    6.18 +  let
    6.19 +    fun pretty_term_type_only ctxt (t, T) =
    6.20 +      (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
    6.21 +       else error "term_type_only: type mismatch";
    6.22 +       Syntax.pretty_typ ctxt T)
    6.23 +  in
    6.24 +    Thy_Output.antiquotation @{binding term_type_only}
    6.25 +      (Args.term -- Args.typ_abbrev)
    6.26 +      (fn {source, context = ctxt, ...} => fn arg =>
    6.27 +        Thy_Output.output ctxt
    6.28 +          (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]))
    6.29 +  end
    6.30  *}
    6.31  (*>*)
    6.32  text{*
     7.1 --- a/doc-src/System/IsaMakefile	Mon Jun 27 17:51:28 2011 +0200
     7.2 +++ b/doc-src/System/IsaMakefile	Mon Jun 27 22:20:49 2011 +0200
     7.3 @@ -22,7 +22,7 @@
     7.4  Pure-System: $(LOG)/Pure-System.gz
     7.5  
     7.6  $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML		\
     7.7 -  Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy
     7.8 +  Thy/Base.thy Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy
     7.9  	@$(USEDIR) -s System Pure Thy
    7.10  	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
    7.11  	 Thy/document/pdfsetup.sty Thy/document/session.tex
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-src/System/Thy/Base.thy	Mon Jun 27 22:20:49 2011 +0200
     8.3 @@ -0,0 +1,10 @@
     8.4 +theory Base
     8.5 +imports Pure
     8.6 +uses "../../antiquote_setup.ML"
     8.7 +begin
     8.8 +
     8.9 +setup {* Antiquote_Setup.setup *}
    8.10 +
    8.11 +declare [[thy_output_source]]
    8.12 +
    8.13 +end
     9.1 --- a/doc-src/System/Thy/Basics.thy	Mon Jun 27 17:51:28 2011 +0200
     9.2 +++ b/doc-src/System/Thy/Basics.thy	Mon Jun 27 22:20:49 2011 +0200
     9.3 @@ -1,5 +1,5 @@
     9.4  theory Basics
     9.5 -imports Pure
     9.6 +imports Base
     9.7  begin
     9.8  
     9.9  chapter {* The Isabelle system environment *}
    10.1 --- a/doc-src/System/Thy/Interfaces.thy	Mon Jun 27 17:51:28 2011 +0200
    10.2 +++ b/doc-src/System/Thy/Interfaces.thy	Mon Jun 27 22:20:49 2011 +0200
    10.3 @@ -1,5 +1,5 @@
    10.4  theory Interfaces
    10.5 -imports Pure
    10.6 +imports Base
    10.7  begin
    10.8  
    10.9  chapter {* User interfaces *}
    11.1 --- a/doc-src/System/Thy/Misc.thy	Mon Jun 27 17:51:28 2011 +0200
    11.2 +++ b/doc-src/System/Thy/Misc.thy	Mon Jun 27 22:20:49 2011 +0200
    11.3 @@ -1,5 +1,5 @@
    11.4  theory Misc
    11.5 -imports Pure
    11.6 +imports Base
    11.7  begin
    11.8  
    11.9  chapter {* Miscellaneous tools \label{ch:tools} *}
    12.1 --- a/doc-src/System/Thy/Presentation.thy	Mon Jun 27 17:51:28 2011 +0200
    12.2 +++ b/doc-src/System/Thy/Presentation.thy	Mon Jun 27 22:20:49 2011 +0200
    12.3 @@ -1,5 +1,5 @@
    12.4  theory Presentation
    12.5 -imports Pure
    12.6 +imports Base
    12.7  begin
    12.8  
    12.9  chapter {* Presenting theories \label{ch:present} *}
    13.1 --- a/doc-src/System/Thy/ROOT.ML	Mon Jun 27 17:51:28 2011 +0200
    13.2 +++ b/doc-src/System/Thy/ROOT.ML	Mon Jun 27 22:20:49 2011 +0200
    13.3 @@ -1,4 +1,1 @@
    13.4 -Thy_Output.source_default := true;
    13.5 -use "../../antiquote_setup.ML";
    13.6 -
    13.7  use_thys ["Basics", "Interfaces", "Presentation", "Misc"];
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/doc-src/System/Thy/document/Base.tex	Mon Jun 27 22:20:49 2011 +0200
    14.3 @@ -0,0 +1,61 @@
    14.4 +%
    14.5 +\begin{isabellebody}%
    14.6 +\def\isabellecontext{Base}%
    14.7 +%
    14.8 +\isadelimtheory
    14.9 +%
   14.10 +\endisadelimtheory
   14.11 +%
   14.12 +\isatagtheory
   14.13 +\isacommand{theory}\isamarkupfalse%
   14.14 +\ Base\isanewline
   14.15 +\isakeyword{imports}\ Pure\isanewline
   14.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
   14.17 +\isakeyword{begin}%
   14.18 +\endisatagtheory
   14.19 +{\isafoldtheory}%
   14.20 +%
   14.21 +\isadelimtheory
   14.22 +\isanewline
   14.23 +%
   14.24 +\endisadelimtheory
   14.25 +%
   14.26 +\isadelimML
   14.27 +\isanewline
   14.28 +%
   14.29 +\endisadelimML
   14.30 +%
   14.31 +\isatagML
   14.32 +\isacommand{setup}\isamarkupfalse%
   14.33 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
   14.34 +\endisatagML
   14.35 +{\isafoldML}%
   14.36 +%
   14.37 +\isadelimML
   14.38 +\isanewline
   14.39 +%
   14.40 +\endisadelimML
   14.41 +\isanewline
   14.42 +\isacommand{declare}\isamarkupfalse%
   14.43 +\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}thy{\isaliteral{5F}{\isacharunderscore}}output{\isaliteral{5F}{\isacharunderscore}}source{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
   14.44 +%
   14.45 +\isadelimtheory
   14.46 +\isanewline
   14.47 +%
   14.48 +\endisadelimtheory
   14.49 +%
   14.50 +\isatagtheory
   14.51 +\isacommand{end}\isamarkupfalse%
   14.52 +%
   14.53 +\endisatagtheory
   14.54 +{\isafoldtheory}%
   14.55 +%
   14.56 +\isadelimtheory
   14.57 +\isanewline
   14.58 +%
   14.59 +\endisadelimtheory
   14.60 +\end{isabellebody}%
   14.61 +%%% Local Variables:
   14.62 +%%% mode: latex
   14.63 +%%% TeX-master: "root"
   14.64 +%%% End:
    15.1 --- a/doc-src/System/Thy/document/Basics.tex	Mon Jun 27 17:51:28 2011 +0200
    15.2 +++ b/doc-src/System/Thy/document/Basics.tex	Mon Jun 27 22:20:49 2011 +0200
    15.3 @@ -9,7 +9,7 @@
    15.4  \isatagtheory
    15.5  \isacommand{theory}\isamarkupfalse%
    15.6  \ Basics\isanewline
    15.7 -\isakeyword{imports}\ Pure\isanewline
    15.8 +\isakeyword{imports}\ Base\isanewline
    15.9  \isakeyword{begin}%
   15.10  \endisatagtheory
   15.11  {\isafoldtheory}%
    16.1 --- a/doc-src/System/Thy/document/Interfaces.tex	Mon Jun 27 17:51:28 2011 +0200
    16.2 +++ b/doc-src/System/Thy/document/Interfaces.tex	Mon Jun 27 22:20:49 2011 +0200
    16.3 @@ -9,7 +9,7 @@
    16.4  \isatagtheory
    16.5  \isacommand{theory}\isamarkupfalse%
    16.6  \ Interfaces\isanewline
    16.7 -\isakeyword{imports}\ Pure\isanewline
    16.8 +\isakeyword{imports}\ Base\isanewline
    16.9  \isakeyword{begin}%
   16.10  \endisatagtheory
   16.11  {\isafoldtheory}%
    17.1 --- a/doc-src/System/Thy/document/Misc.tex	Mon Jun 27 17:51:28 2011 +0200
    17.2 +++ b/doc-src/System/Thy/document/Misc.tex	Mon Jun 27 22:20:49 2011 +0200
    17.3 @@ -9,7 +9,7 @@
    17.4  \isatagtheory
    17.5  \isacommand{theory}\isamarkupfalse%
    17.6  \ Misc\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/Presentation.tex	Mon Jun 27 17:51:28 2011 +0200
    18.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Mon Jun 27 22:20:49 2011 +0200
    18.3 @@ -9,7 +9,7 @@
    18.4  \isatagtheory
    18.5  \isacommand{theory}\isamarkupfalse%
    18.6  \ Presentation\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/TutorialI/Inductive/Advanced.thy	Mon Jun 27 17:51:28 2011 +0200
    19.2 +++ b/doc-src/TutorialI/Inductive/Advanced.thy	Mon Jun 27 22:20:49 2011 +0200
    19.3 @@ -1,4 +1,6 @@
    19.4 -(*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*)
    19.5 +(*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin
    19.6 +setup {* Antiquote_Setup.setup *}
    19.7 +(*>*)
    19.8  
    19.9  text {*
   19.10  The premises of introduction rules may contain universal quantifiers and
    20.1 --- a/doc-src/TutorialI/Inductive/Even.thy	Mon Jun 27 17:51:28 2011 +0200
    20.2 +++ b/doc-src/TutorialI/Inductive/Even.thy	Mon Jun 27 22:20:49 2011 +0200
    20.3 @@ -1,4 +1,6 @@
    20.4 -(*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin(*>*)
    20.5 +(*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin
    20.6 +setup {* Antiquote_Setup.setup *}
    20.7 +(*>*)
    20.8  
    20.9  section{* The Set of Even Numbers *}
   20.10  
    21.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Jun 27 17:51:28 2011 +0200
    21.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Jun 27 22:20:49 2011 +0200
    21.3 @@ -15,6 +15,19 @@
    21.4  %
    21.5  \endisadelimtheory
    21.6  %
    21.7 +\isadelimML
    21.8 +%
    21.9 +\endisadelimML
   21.10 +%
   21.11 +\isatagML
   21.12 +%
   21.13 +\endisatagML
   21.14 +{\isafoldML}%
   21.15 +%
   21.16 +\isadelimML
   21.17 +%
   21.18 +\endisadelimML
   21.19 +%
   21.20  \begin{isamarkuptext}%
   21.21  The premises of introduction rules may contain universal quantifiers and
   21.22  monotone functions.  A universal quantifier lets the rule 
    22.1 --- a/doc-src/TutorialI/Inductive/document/Even.tex	Mon Jun 27 17:51:28 2011 +0200
    22.2 +++ b/doc-src/TutorialI/Inductive/document/Even.tex	Mon Jun 27 22:20:49 2011 +0200
    22.3 @@ -15,6 +15,19 @@
    22.4  %
    22.5  \endisadelimtheory
    22.6  %
    22.7 +\isadelimML
    22.8 +%
    22.9 +\endisadelimML
   22.10 +%
   22.11 +\isatagML
   22.12 +%
   22.13 +\endisatagML
   22.14 +{\isafoldML}%
   22.15 +%
   22.16 +\isadelimML
   22.17 +%
   22.18 +\endisadelimML
   22.19 +%
   22.20  \isamarkupsection{The Set of Even Numbers%
   22.21  }
   22.22  \isamarkuptrue%
    23.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Mon Jun 27 17:51:28 2011 +0200
    23.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Mon Jun 27 22:20:49 2011 +0200
    23.3 @@ -9,6 +9,7 @@
    23.4  header{*Theory of Agents and Messages for Security Protocols*}
    23.5  
    23.6  theory Message imports Main uses "../../antiquote_setup.ML" begin
    23.7 +setup {* Antiquote_Setup.setup *}
    23.8  
    23.9  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
   23.10  lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
    24.1 --- a/doc-src/TutorialI/Protocol/document/Message.tex	Mon Jun 27 17:51:28 2011 +0200
    24.2 +++ b/doc-src/TutorialI/Protocol/document/Message.tex	Mon Jun 27 22:20:49 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  \isadelimproof
   24.21  %
   24.22  \endisadelimproof
    25.1 --- a/doc-src/TutorialI/Types/Setup.thy	Mon Jun 27 17:51:28 2011 +0200
    25.2 +++ b/doc-src/TutorialI/Types/Setup.thy	Mon Jun 27 22:20:49 2011 +0200
    25.3 @@ -5,4 +5,7 @@
    25.4    "../../more_antiquote.ML"
    25.5  begin
    25.6  
    25.7 +setup {* Antiquote_Setup.setup #> More_Antiquote.setup *}
    25.8 +
    25.9 +
   25.10  end
   25.11 \ No newline at end of file
    26.1 --- a/doc-src/antiquote_setup.ML	Mon Jun 27 17:51:28 2011 +0200
    26.2 +++ b/doc-src/antiquote_setup.ML	Mon Jun 27 22:20:49 2011 +0200
    26.3 @@ -4,7 +4,12 @@
    26.4  Auxiliary antiquotations for the Isabelle manuals.
    26.5  *)
    26.6  
    26.7 -structure Antiquote_Setup: sig end =
    26.8 +signature ANTIQUOTE_SETUP =
    26.9 +sig
   26.10 +  val setup: theory -> theory
   26.11 +end;
   26.12 +
   26.13 +structure Antiquote_Setup: ANTIQUOTE_SETUP =
   26.14  struct
   26.15  
   26.16  (* misc utils *)
   26.17 @@ -35,8 +40,9 @@
   26.18  
   26.19  val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
   26.20  
   26.21 -val _ = Thy_Output.antiquotation "verbatim" (Scan.lift Args.name)
   26.22 -  (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
   26.23 +val verbatim_setup =
   26.24 +  Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
   26.25 +    (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
   26.26  
   26.27  
   26.28  (* ML text *)
   26.29 @@ -87,42 +93,45 @@
   26.30  
   26.31  in
   26.32  
   26.33 -val _ = index_ml "index_ML" "" ml_val;
   26.34 -val _ = index_ml "index_ML_type" "type" ml_type;
   26.35 -val _ = index_ml "index_ML_exn" "exception" ml_exn;
   26.36 -val _ = index_ml "index_ML_structure" "structure" ml_structure;
   26.37 -val _ = index_ml "index_ML_functor" "functor" ml_functor;
   26.38 +val index_ml_setup =
   26.39 +  index_ml @{binding index_ML} "" ml_val #>
   26.40 +  index_ml @{binding index_ML_type} "type" ml_type #>
   26.41 +  index_ml @{binding index_ML_exn} "exception" ml_exn #>
   26.42 +  index_ml @{binding index_ML_structure} "structure" ml_structure #>
   26.43 +  index_ml @{binding index_ML_functor} "functor" ml_functor;
   26.44  
   26.45  end;
   26.46  
   26.47  
   26.48  (* named theorems *)
   26.49  
   26.50 -val _ = Thy_Output.antiquotation "named_thms"
   26.51 -  (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
   26.52 -  (fn {context = ctxt, ...} =>
   26.53 -    map (apfst (Thy_Output.pretty_thm ctxt))
   26.54 -    #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
   26.55 -    #> (if Config.get ctxt Thy_Output.display
   26.56 -        then
   26.57 -          map (fn (p, name) =>
   26.58 -            Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
   26.59 -            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
   26.60 -          #> space_implode "\\par\\smallskip%\n"
   26.61 -          #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   26.62 -        else
   26.63 -          map (fn (p, name) =>
   26.64 -            Output.output (Pretty.str_of p) ^
   26.65 -            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
   26.66 -          #> space_implode "\\par\\smallskip%\n"
   26.67 -          #> enclose "\\isa{" "}"));
   26.68 +val named_thms_setup =
   26.69 +  Thy_Output.antiquotation @{binding named_thms}
   26.70 +    (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
   26.71 +    (fn {context = ctxt, ...} =>
   26.72 +      map (apfst (Thy_Output.pretty_thm ctxt))
   26.73 +      #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
   26.74 +      #> (if Config.get ctxt Thy_Output.display
   26.75 +          then
   26.76 +            map (fn (p, name) =>
   26.77 +              Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
   26.78 +              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
   26.79 +            #> space_implode "\\par\\smallskip%\n"
   26.80 +            #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   26.81 +          else
   26.82 +            map (fn (p, name) =>
   26.83 +              Output.output (Pretty.str_of p) ^
   26.84 +              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
   26.85 +            #> space_implode "\\par\\smallskip%\n"
   26.86 +            #> enclose "\\isa{" "}"));
   26.87  
   26.88  
   26.89  (* theory file *)
   26.90  
   26.91 -val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
   26.92 -  (fn {context = ctxt, ...} =>
   26.93 -    fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
   26.94 +val thy_file_setup =
   26.95 +  Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
   26.96 +    (fn {context = ctxt, ...} =>
   26.97 +      fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
   26.98  
   26.99  
  26.100  (* Isabelle/Isar entities (with index) *)
  26.101 @@ -142,8 +151,8 @@
  26.102  
  26.103  fun entity check markup kind index =
  26.104    Thy_Output.antiquotation
  26.105 -    (translate (fn " " => "_" | c => c) kind ^
  26.106 -      (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))
  26.107 +    (Binding.name (translate (fn " " => "_" | c => c) kind ^
  26.108 +      (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
  26.109      (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
  26.110      (fn {context = ctxt, ...} => fn (logic, name) =>
  26.111        let
  26.112 @@ -170,32 +179,44 @@
  26.113        end);
  26.114  
  26.115  fun entity_antiqs check markup kind =
  26.116 - ((entity check markup kind NONE);
  26.117 -  (entity check markup kind (SOME true));
  26.118 -  (entity check markup kind (SOME false)));
  26.119 +  entity check markup kind NONE #>
  26.120 +  entity check markup kind (SOME true) #>
  26.121 +  entity check markup kind (SOME false);
  26.122  
  26.123  in
  26.124  
  26.125 -val _ = entity_antiqs no_check "" "syntax";
  26.126 -val _ = entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command";
  26.127 -val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword";
  26.128 -val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "element";
  26.129 -val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method";
  26.130 -val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute";
  26.131 -val _ = entity_antiqs no_check "" "fact";
  26.132 -val _ = entity_antiqs no_check "" "variable";
  26.133 -val _ = entity_antiqs no_check "" "case";
  26.134 -val _ = entity_antiqs (K Thy_Output.defined_command) "" "antiquotation";
  26.135 -val _ = entity_antiqs (K Thy_Output.defined_option) "" "antiquotation option";
  26.136 -val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
  26.137 -val _ = entity_antiqs no_check "" "inference";
  26.138 -val _ = entity_antiqs no_check "isatt" "executable";
  26.139 -val _ = entity_antiqs (K check_tool) "isatt" "tool";
  26.140 -val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
  26.141 -val _ =
  26.142 -  entity_antiqs
  26.143 -    (thy_check ML_Context.intern_antiq ML_Context.defined_antiq) "" Markup.ML_antiquotationN;
  26.144 +val entity_setup =
  26.145 +  entity_antiqs no_check "" "syntax" #>
  26.146 +  entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command" #>
  26.147 +  entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword" #>
  26.148 +  entity_antiqs (K Keyword.is_keyword) "isakeyword" "element" #>
  26.149 +  entity_antiqs (thy_check Method.intern Method.defined) "" "method" #>
  26.150 +  entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" #>
  26.151 +  entity_antiqs no_check "" "fact" #>
  26.152 +  entity_antiqs no_check "" "variable" #>
  26.153 +  entity_antiqs no_check "" "case" #>
  26.154 +  entity_antiqs (thy_check Thy_Output.intern_command Thy_Output.defined_command)
  26.155 +    "" "antiquotation" #>
  26.156 +  entity_antiqs (thy_check Thy_Output.intern_option Thy_Output.defined_option)
  26.157 +    "" "antiquotation option" #>
  26.158 +  entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" #>
  26.159 +  entity_antiqs no_check "" "inference" #>
  26.160 +  entity_antiqs no_check "isatt" "executable" #>
  26.161 +  entity_antiqs (K check_tool) "isatt" "tool" #>
  26.162 +  entity_antiqs (K (can Thy_Info.get_theory)) "" "theory" #>
  26.163 +  entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
  26.164 +    "" Markup.ML_antiquotationN;
  26.165  
  26.166  end;
  26.167  
  26.168 +
  26.169 +(* theory setup *)
  26.170 +
  26.171 +val setup =
  26.172 +  verbatim_setup #>
  26.173 +  index_ml_setup #>
  26.174 +  named_thms_setup #>
  26.175 +  thy_file_setup #>
  26.176 +  entity_setup;
  26.177 +
  26.178  end;
    27.1 --- a/doc-src/more_antiquote.ML	Mon Jun 27 17:51:28 2011 +0200
    27.2 +++ b/doc-src/more_antiquote.ML	Mon Jun 27 22:20:49 2011 +0200
    27.3 @@ -6,6 +6,7 @@
    27.4  
    27.5  signature MORE_ANTIQUOTE =
    27.6  sig
    27.7 +  val setup: theory -> theory
    27.8  end;
    27.9  
   27.10  structure More_Antiquote : MORE_ANTIQUOTE =
   27.11 @@ -40,8 +41,9 @@
   27.12  
   27.13  in
   27.14  
   27.15 -val _ = Thy_Output.antiquotation "code_thms" Args.term
   27.16 -  (fn {source, context, ...} => pretty_code_thm source context);
   27.17 +val setup =
   27.18 +  Thy_Output.antiquotation @{binding code_thms} Args.term
   27.19 +    (fn {source, context, ...} => pretty_code_thm source context);
   27.20  
   27.21  end;
   27.22  
    28.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Jun 27 17:51:28 2011 +0200
    28.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Jun 27 22:20:49 2011 +0200
    28.3 @@ -237,27 +237,28 @@
    28.4  
    28.5  (** document antiquotation **)
    28.6  
    28.7 -val _ = Thy_Output.antiquotation "datatype" (Args.type_name true)
    28.8 -  (fn {source = src, context = ctxt, ...} => fn dtco =>
    28.9 -    let
   28.10 -      val thy = Proof_Context.theory_of ctxt;
   28.11 -      val (vs, cos) = the_spec thy dtco;
   28.12 -      val ty = Type (dtco, map TFree vs);
   28.13 -      val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
   28.14 -      fun pretty_constr (co, tys) =
   28.15 -        Pretty.block (Pretty.breaks
   28.16 -          (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
   28.17 -            map pretty_typ_bracket tys));
   28.18 -      val pretty_datatype =
   28.19 -        Pretty.block
   28.20 -         (Pretty.command "datatype" :: Pretty.brk 1 ::
   28.21 -          Syntax.pretty_typ ctxt ty ::
   28.22 -          Pretty.str " =" :: Pretty.brk 1 ::
   28.23 -          flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos)));
   28.24 -    in
   28.25 -      Thy_Output.output ctxt
   28.26 -        (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
   28.27 -    end);
   28.28 +val antiq_setup =
   28.29 +  Thy_Output.antiquotation @{binding datatype} (Args.type_name true)
   28.30 +    (fn {source = src, context = ctxt, ...} => fn dtco =>
   28.31 +      let
   28.32 +        val thy = Proof_Context.theory_of ctxt;
   28.33 +        val (vs, cos) = the_spec thy dtco;
   28.34 +        val ty = Type (dtco, map TFree vs);
   28.35 +        val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
   28.36 +        fun pretty_constr (co, tys) =
   28.37 +          Pretty.block (Pretty.breaks
   28.38 +            (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
   28.39 +              map pretty_typ_bracket tys));
   28.40 +        val pretty_datatype =
   28.41 +          Pretty.block
   28.42 +           (Pretty.command "datatype" :: Pretty.brk 1 ::
   28.43 +            Syntax.pretty_typ ctxt ty ::
   28.44 +            Pretty.str " =" :: Pretty.brk 1 ::
   28.45 +            flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos)));
   28.46 +      in
   28.47 +        Thy_Output.output ctxt
   28.48 +          (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
   28.49 +      end);
   28.50  
   28.51  
   28.52  
   28.53 @@ -453,6 +454,7 @@
   28.54  
   28.55  val setup =
   28.56    trfun_setup #>
   28.57 +  antiq_setup #>
   28.58    Datatype_Interpretation.init;
   28.59  
   28.60  
    29.1 --- a/src/Pure/General/markup.ML	Mon Jun 27 17:51:28 2011 +0200
    29.2 +++ b/src/Pure/General/markup.ML	Mon Jun 27 22:20:49 2011 +0200
    29.3 @@ -73,7 +73,8 @@
    29.4    val doc_sourceN: string val doc_source: T
    29.5    val antiqN: string val antiq: T
    29.6    val ML_antiquotationN: string
    29.7 -  val doc_antiqN: string val doc_antiq: string -> T
    29.8 +  val doc_antiquotationN: string
    29.9 +  val doc_antiquotation_optionN: string
   29.10    val keyword_declN: string val keyword_decl: string -> T
   29.11    val command_declN: string val command_decl: string -> string -> T
   29.12    val keywordN: string val keyword: T
   29.13 @@ -267,7 +268,8 @@
   29.14  
   29.15  val (antiqN, antiq) = markup_elem "antiq";
   29.16  val ML_antiquotationN = "ML antiquotation";
   29.17 -val (doc_antiqN, doc_antiq) = markup_string "doc_antiq" nameN;
   29.18 +val doc_antiquotationN = "document antiquotation";
   29.19 +val doc_antiquotation_optionN = "document antiquotation option";
   29.20  
   29.21  
   29.22  (* outer syntax *)
    30.1 --- a/src/Pure/General/markup.scala	Mon Jun 27 17:51:28 2011 +0200
    30.2 +++ b/src/Pure/General/markup.scala	Mon Jun 27 22:20:49 2011 +0200
    30.3 @@ -190,7 +190,8 @@
    30.4  
    30.5    val ANTIQ = "antiq"
    30.6    val ML_ANTIQUOTATION = "ML antiquotation"
    30.7 -  val DOC_ANTIQ = "doc_antiq"
    30.8 +  val DOCUMENT_ANTIQUOTATION = "document antiquotation"
    30.9 +  val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
   30.10  
   30.11  
   30.12    /* ML syntax */
    31.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Jun 27 17:51:28 2011 +0200
    31.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Jun 27 22:20:49 2011 +0200
    31.3 @@ -384,7 +384,8 @@
    31.4  val print_methods = Toplevel.unknown_theory o
    31.5    Toplevel.keep (Method.print_methods o Toplevel.theory_of);
    31.6  
    31.7 -val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations;
    31.8 +val print_antiquotations =
    31.9 +  Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of);
   31.10  
   31.11  val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   31.12    let
    32.1 --- a/src/Pure/Thy/rail.ML	Mon Jun 27 17:51:28 2011 +0200
    32.2 +++ b/src/Pure/Thy/rail.ML	Mon Jun 27 22:20:49 2011 +0200
    32.3 @@ -259,8 +259,10 @@
    32.4  in
    32.5  
    32.6  val _ =
    32.7 -  Thy_Output.antiquotation "rail" (Scan.lift (Parse.source_position Parse.string))
    32.8 -    (fn {state, ...} => output_rules state o read);
    32.9 +  Context.>> (Context.map_theory
   32.10 +    (Thy_Output.antiquotation (Binding.name "rail")
   32.11 +      (Scan.lift (Parse.source_position Parse.string))
   32.12 +      (fn {state, ...} => output_rules state o read)));
   32.13  
   32.14  end;
   32.15  
    33.1 --- a/src/Pure/Thy/thy_output.ML	Mon Jun 27 17:51:28 2011 +0200
    33.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Jun 27 22:20:49 2011 +0200
    33.3 @@ -17,14 +17,17 @@
    33.4    val source: bool Config.T
    33.5    val break: bool Config.T
    33.6    val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
    33.7 -  val add_option: string -> (string -> Proof.context -> Proof.context) -> unit
    33.8 -  val defined_command: string -> bool
    33.9 -  val defined_option: string -> bool
   33.10 -  val print_antiquotations: unit -> unit
   33.11 +  val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
   33.12 +  val intern_command: theory -> xstring -> string
   33.13 +  val defined_command: theory -> string -> bool
   33.14 +  val intern_option: theory -> xstring -> string
   33.15 +  val defined_option: theory -> string -> bool
   33.16 +  val print_antiquotations: Proof.context -> unit
   33.17 +  val antiquotation: binding -> 'a context_parser ->
   33.18 +    ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
   33.19 +      theory -> theory
   33.20    val boolean: string -> bool
   33.21    val integer: string -> int
   33.22 -  val antiquotation: string -> 'a context_parser ->
   33.23 -    ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> unit
   33.24    datatype markup = Markup | MarkupEnv | Verbatim
   33.25    val modes: string list Unsynchronized.ref
   33.26    val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
   33.27 @@ -72,55 +75,66 @@
   33.28  
   33.29  (** maintain global antiquotations **)
   33.30  
   33.31 -local
   33.32 -
   33.33 -val global_commands =
   33.34 -  Unsynchronized.ref
   33.35 -    (Symtab.empty: (Args.src -> Toplevel.state -> Proof.context -> string) Symtab.table);
   33.36 +structure Antiquotations = Theory_Data
   33.37 +(
   33.38 +  type T =
   33.39 +    (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
   33.40 +      (string -> Proof.context -> Proof.context) Name_Space.table;
   33.41 +  val empty : T =
   33.42 +    (Name_Space.empty_table Markup.doc_antiquotationN,
   33.43 +      Name_Space.empty_table Markup.doc_antiquotation_optionN);
   33.44 +  val extend = I;
   33.45 +  fun merge ((commands1, options1), (commands2, options2)) : T =
   33.46 +    (Name_Space.merge_tables (commands1, commands2),
   33.47 +      Name_Space.merge_tables (options1, options2));
   33.48 +);
   33.49  
   33.50 -val global_options =
   33.51 -  Unsynchronized.ref (Symtab.empty: (string -> Proof.context -> Proof.context) Symtab.table);
   33.52 -
   33.53 -fun add_item kind name item tab =
   33.54 - (if not (Symtab.defined tab name) then ()
   33.55 -  else warning ("Redefined document antiquotation " ^ kind ^ ": " ^ quote name);
   33.56 -  Symtab.update (name, item) tab);
   33.57 -
   33.58 -in
   33.59 +fun add_command name cmd thy =
   33.60 +  thy |> Antiquotations.map
   33.61 +    (apfst
   33.62 +      (Name_Space.define
   33.63 +        (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, cmd) #> snd));
   33.64  
   33.65 -fun add_command name cmd =
   33.66 -  CRITICAL (fn () => Unsynchronized.change global_commands (add_item "command" name cmd));
   33.67 -fun add_option name opt =
   33.68 -  CRITICAL (fn () => Unsynchronized.change global_options (add_item "option" name opt));
   33.69 +fun add_option name opt thy =
   33.70 +  thy |> Antiquotations.map
   33.71 +    (apsnd
   33.72 +      (Name_Space.define
   33.73 +        (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, opt) #> snd));
   33.74  
   33.75 -fun defined_command name = Symtab.defined (! global_commands) name;
   33.76 -fun defined_option name = Symtab.defined (! global_options) name;
   33.77 +val intern_command = Name_Space.intern o #1 o #1 o Antiquotations.get;
   33.78 +val defined_command = Symtab.defined o #2 o #1 o Antiquotations.get;
   33.79  
   33.80 -fun command src =
   33.81 -  let val ((name, _), pos) = Args.dest_src src in
   33.82 -    (case Symtab.lookup (! global_commands) name of
   33.83 -      NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
   33.84 -    | SOME f =>
   33.85 -       (Position.report pos (Markup.doc_antiq name);
   33.86 -        (fn state => fn ctxt => f src state ctxt handle ERROR msg =>
   33.87 -          cat_error msg ("The error(s) above occurred in document antiquotation: " ^
   33.88 -            quote name ^ Position.str_of pos))))
   33.89 +val intern_option = Name_Space.intern o #1 o #2 o Antiquotations.get;
   33.90 +val defined_option = Symtab.defined o #2 o #2 o Antiquotations.get;
   33.91 +
   33.92 +fun command src state ctxt =
   33.93 +  let
   33.94 +    val thy = Proof_Context.theory_of ctxt;
   33.95 +    val ((xname, _), pos) = Args.dest_src src;
   33.96 +    val (name, f) = Name_Space.check ctxt (#1 (Antiquotations.get thy)) (xname, pos);
   33.97 +  in
   33.98 +    f src state ctxt handle ERROR msg =>
   33.99 +      cat_error msg ("The error(s) above occurred in document antiquotation: " ^
  33.100 +        quote name ^ Position.str_of pos)
  33.101    end;
  33.102  
  33.103 -fun option (name, s) ctxt =
  33.104 -  (case Symtab.lookup (! global_options) name of
  33.105 -    NONE => error ("Unknown document antiquotation option: " ^ quote name)
  33.106 -  | SOME opt => opt s ctxt);
  33.107 -
  33.108 +fun option ((xname, pos), s) ctxt =
  33.109 +  let
  33.110 +    val thy = Proof_Context.theory_of ctxt;
  33.111 +    val (_, opt) = Name_Space.check ctxt (#2 (Antiquotations.get thy)) (xname, pos);
  33.112 +  in opt s ctxt end;
  33.113  
  33.114 -fun print_antiquotations () =
  33.115 - [Pretty.big_list "document antiquotation commands:"
  33.116 -    (map Pretty.str (sort_strings (Symtab.keys (! global_commands)))),
  33.117 -  Pretty.big_list "document antiquotation options:"
  33.118 -    (map Pretty.str (sort_strings (Symtab.keys (! global_options))))]
  33.119 - |> Pretty.chunks |> Pretty.writeln;
  33.120 -
  33.121 -end;
  33.122 +fun print_antiquotations ctxt =
  33.123 +  let
  33.124 +    val thy = Proof_Context.theory_of ctxt;
  33.125 +    val (commands, options) = Antiquotations.get thy;
  33.126 +    val command_names = map #1 (Name_Space.extern_table ctxt commands);
  33.127 +    val option_names = map #1 (Name_Space.extern_table ctxt options);
  33.128 +  in
  33.129 +    [Pretty.big_list "document antiquotations:" (map Pretty.str command_names),
  33.130 +      Pretty.big_list "document antiquotation options:" (map Pretty.str option_names)]
  33.131 +    |> Pretty.chunks |> Pretty.writeln
  33.132 +  end;
  33.133  
  33.134  fun antiquotation name scan out =
  33.135    add_command name
  33.136 @@ -152,7 +166,7 @@
  33.137  local
  33.138  
  33.139  val property =
  33.140 -  Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
  33.141 +  Parse.position Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
  33.142  
  33.143  val properties =
  33.144    Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
  33.145 @@ -445,23 +459,25 @@
  33.146  
  33.147  (* options *)
  33.148  
  33.149 -val _ = add_option "show_types" (Config.put show_types o boolean);
  33.150 -val _ = add_option "show_sorts" (Config.put show_sorts o boolean);
  33.151 -val _ = add_option "show_structs" (Config.put show_structs o boolean);
  33.152 -val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
  33.153 -val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
  33.154 -val _ = add_option "names_long" (Config.put Name_Space.names_long o boolean);
  33.155 -val _ = add_option "names_short" (Config.put Name_Space.names_short o boolean);
  33.156 -val _ = add_option "names_unique" (Config.put Name_Space.names_unique o boolean);
  33.157 -val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
  33.158 -val _ = add_option "display" (Config.put display o boolean);
  33.159 -val _ = add_option "break" (Config.put break o boolean);
  33.160 -val _ = add_option "quotes" (Config.put quotes o boolean);
  33.161 -val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single);
  33.162 -val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
  33.163 -val _ = add_option "indent" (Config.put indent o integer);
  33.164 -val _ = add_option "source" (Config.put source o boolean);
  33.165 -val _ = add_option "goals_limit" (Config.put Goal_Display.goals_limit o integer);
  33.166 +val _ =
  33.167 +  Context.>> (Context.map_theory
  33.168 +   (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
  33.169 +    add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
  33.170 +    add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
  33.171 +    add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
  33.172 +    add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
  33.173 +    add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
  33.174 +    add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
  33.175 +    add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
  33.176 +    add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
  33.177 +    add_option (Binding.name "display") (Config.put display o boolean) #>
  33.178 +    add_option (Binding.name "break") (Config.put break o boolean) #>
  33.179 +    add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
  33.180 +    add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
  33.181 +    add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
  33.182 +    add_option (Binding.name "indent") (Config.put indent o integer) #>
  33.183 +    add_option (Binding.name "source") (Config.put source o boolean) #>
  33.184 +    add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer)));
  33.185  
  33.186  
  33.187  (* basic pretty printing *)
  33.188 @@ -562,22 +578,26 @@
  33.189  
  33.190  in
  33.191  
  33.192 -val _ = basic_entities_style "thm" (Term_Style.parse -- Attrib.thms) pretty_thm_style;
  33.193 -val _ = basic_entity "prop" (Term_Style.parse -- Args.prop) pretty_term_style;
  33.194 -val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style;
  33.195 -val _ = basic_entity "term_type" (Term_Style.parse -- Args.term) pretty_term_typ;
  33.196 -val _ = basic_entity "typeof" (Term_Style.parse -- Args.term) pretty_term_typeof;
  33.197 -val _ = basic_entity "const" (Args.const_proper false) pretty_const;
  33.198 -val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
  33.199 -val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
  33.200 -val _ = basic_entity "class" (Scan.lift Args.name) pretty_class;
  33.201 -val _ = basic_entity "type" (Scan.lift Args.name) pretty_type;
  33.202 -val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
  33.203 -val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
  33.204 -val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
  33.205 -val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
  33.206 -val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
  33.207 -val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
  33.208 +val _ =
  33.209 +  Context.>> (Context.map_theory
  33.210 +   (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
  33.211 +    basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
  33.212 +    basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
  33.213 +    basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
  33.214 +    basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
  33.215 +    basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
  33.216 +    basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
  33.217 +    basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
  33.218 +    basic_entity (Binding.name "class") (Scan.lift Args.name) pretty_class #>
  33.219 +    basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
  33.220 +    basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
  33.221 +    basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
  33.222 +    basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
  33.223 +    basic_entity (Binding.name "theory") (Scan.lift Args.name) pretty_theory #>
  33.224 +    basic_entities_style (Binding.name "thm_style")
  33.225 +      (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style #>
  33.226 +    basic_entity (Binding.name "term_style")
  33.227 +      (Term_Style.parse_bare -- Args.term) pretty_term_style));
  33.228  
  33.229  end;
  33.230  
  33.231 @@ -598,8 +618,10 @@
  33.232  
  33.233  in
  33.234  
  33.235 -val _ = goal_state "goals" true;
  33.236 -val _ = goal_state "subgoals" false;
  33.237 +val _ =
  33.238 +  Context.>> (Context.map_theory
  33.239 +   (goal_state (Binding.name "goals") true #>
  33.240 +    goal_state (Binding.name "subgoals") false));
  33.241  
  33.242  end;
  33.243  
  33.244 @@ -608,16 +630,19 @@
  33.245  
  33.246  val _ = Keyword.keyword "by";
  33.247  
  33.248 -val _ = antiquotation "lemma"
  33.249 -  (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
  33.250 -  (fn {source, context, ...} => fn (prop, methods) =>
  33.251 -    let
  33.252 -      val prop_src =
  33.253 -        (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
  33.254 -      val _ = context
  33.255 -        |> Proof.theorem NONE (K I) [[(prop, [])]]
  33.256 -        |> Proof.global_terminal_proof methods;
  33.257 -    in output context (maybe_pretty_source pretty_term context prop_src [prop]) end);
  33.258 +val _ =
  33.259 +  Context.>> (Context.map_theory
  33.260 +   (antiquotation (Binding.name "lemma")
  33.261 +    (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
  33.262 +    (fn {source, context, ...} => fn (prop, methods) =>
  33.263 +      let
  33.264 +        val prop_src =
  33.265 +          (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
  33.266 +        (* FIXME check proof!? *)
  33.267 +        val _ = context
  33.268 +          |> Proof.theorem NONE (K I) [[(prop, [])]]
  33.269 +          |> Proof.global_terminal_proof methods;
  33.270 +      in output context (maybe_pretty_source pretty_term context prop_src [prop]) end)));
  33.271  
  33.272  
  33.273  (* ML text *)
  33.274 @@ -642,25 +667,30 @@
  33.275  
  33.276  in
  33.277  
  33.278 -val _ = ml_text "ML" (ml_enclose "fn _ => (" ");");
  33.279 -val _ = ml_text "ML_type" (ml_enclose "val _ = NONE : (" ") option;");
  33.280 -val _ = ml_text "ML_struct" (ml_enclose "functor XXX() = struct structure XX = " " end;");
  33.281 +val _ =
  33.282 +  Context.>> (Context.map_theory
  33.283 +   (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
  33.284 +    ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
  33.285 +    ml_text (Binding.name "ML_struct")
  33.286 +      (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
  33.287  
  33.288 -val _ = ml_text "ML_functor"   (* FIXME formal treatment of functor name (!?) *)
  33.289 -  (fn pos => fn txt =>
  33.290 -    ML_Lex.read Position.none ("ML_Env.check_functor " ^
  33.291 -      ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos)))));
  33.292 +    ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
  33.293 +      (fn pos => fn txt =>
  33.294 +        ML_Lex.read Position.none ("ML_Env.check_functor " ^
  33.295 +          ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
  33.296  
  33.297 -val _ = ml_text "ML_text" (K (K []));
  33.298 +    ml_text (Binding.name "ML_text") (K (K []))));
  33.299  
  33.300  end;
  33.301  
  33.302  
  33.303  (* files *)
  33.304  
  33.305 -val _ = antiquotation "file" (Scan.lift Args.name)
  33.306 -  (fn {context, ...} => fn path =>
  33.307 -    if File.exists (Path.explode path) then verb_text path
  33.308 -    else error ("Bad file: " ^ quote path));
  33.309 +val _ =
  33.310 +  Context.>> (Context.map_theory
  33.311 +   (antiquotation (Binding.name "file") (Scan.lift Args.name)
  33.312 +    (fn _ => fn path =>
  33.313 +      if File.exists (Path.explode path) then verb_text path
  33.314 +      else error ("Bad file: " ^ quote path))));
  33.315  
  33.316  end;
    34.1 --- a/src/Tools/Code/code_target.ML	Mon Jun 27 17:51:28 2011 +0200
    34.2 +++ b/src/Tools/Code/code_target.ML	Mon Jun 27 22:20:49 2011 +0200
    34.3 @@ -60,6 +60,8 @@
    34.4    val add_include: string -> string * (string * string list) option -> theory -> theory
    34.5  
    34.6    val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
    34.7 +
    34.8 +  val setup: theory -> theory
    34.9  end;
   34.10  
   34.11  structure Code_Target : CODE_TARGET =
   34.12 @@ -143,7 +145,7 @@
   34.13  };
   34.14  
   34.15  fun make_target ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))) =
   34.16 -  Target { serial = serial, description = description, reserved = reserved, 
   34.17 +  Target { serial = serial, description = description, reserved = reserved,
   34.18      includes = includes, module_alias = module_alias, symbol_syntax = symbol_syntax };
   34.19  fun map_target f ( Target { serial, description, reserved, includes, module_alias, symbol_syntax } ) =
   34.20    make_target (f ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))));
   34.21 @@ -199,7 +201,7 @@
   34.22            | _ => true);
   34.23      val _ = if overwriting
   34.24        then warning ("Overwriting existing target " ^ quote target)
   34.25 -      else (); 
   34.26 +      else ();
   34.27    in
   34.28      thy
   34.29      |> (Targets.map o apfst o apfst o Symtab.update)
   34.30 @@ -251,7 +253,7 @@
   34.31  fun collapse_hierarchy thy =
   34.32    let
   34.33      val ((targets, _), _) = Targets.get thy;
   34.34 -    fun collapse target = 
   34.35 +    fun collapse target =
   34.36        let
   34.37          val data = case Symtab.lookup targets target
   34.38           of SOME data => data
   34.39 @@ -352,7 +354,7 @@
   34.40      val serializer = case the_description data
   34.41       of Fundamental seri => #serializer seri;
   34.42      val reserved = the_reserved data;
   34.43 -    val module_alias = the_module_alias data 
   34.44 +    val module_alias = the_module_alias data
   34.45      val { class, instance, tyco, const } = the_symbol_syntax data;
   34.46      val literals = the_literals thy target;
   34.47      val (prepared_serializer, prepared_program) = prepare_serializer thy
   34.48 @@ -396,7 +398,7 @@
   34.49      val { env_var, make_destination, make_command } =
   34.50        (#check o the_fundamental thy) target;
   34.51      fun ext_check p =
   34.52 -      let 
   34.53 +      let
   34.54          val destination = make_destination p;
   34.55          val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
   34.56            module_name args naming program names_cs);
   34.57 @@ -495,7 +497,7 @@
   34.58  fun parse_names category parse internalize lookup =
   34.59    Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
   34.60    >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs);
   34.61 -  
   34.62 +
   34.63  val parse_consts = parse_names "consts" Args.term
   34.64    Code.check_const Code_Thingol.lookup_const ;
   34.65  
   34.66 @@ -511,15 +513,17 @@
   34.67  
   34.68  in
   34.69  
   34.70 -val _ = Thy_Output.antiquotation "code_stmts"
   34.71 -  (parse_const_terms -- Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
   34.72 -    -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
   34.73 -  (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
   34.74 -    let val thy = Proof_Context.theory_of ctxt in
   34.75 -      present_code thy (mk_cs thy)
   34.76 -        (fn naming => maps (fn f => f thy naming) mk_stmtss)
   34.77 -        target some_width "Example" []
   34.78 -    end);
   34.79 +val antiq_setup =
   34.80 +  Thy_Output.antiquotation @{binding code_stmts}
   34.81 +    (parse_const_terms --
   34.82 +      Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
   34.83 +      -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
   34.84 +    (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
   34.85 +      let val thy = Proof_Context.theory_of ctxt in
   34.86 +        present_code thy (mk_cs thy)
   34.87 +          (fn naming => maps (fn f => f thy naming) mk_stmtss)
   34.88 +          target some_width "Example" []
   34.89 +      end);
   34.90  
   34.91  end;
   34.92  
   34.93 @@ -745,4 +749,9 @@
   34.94      | NONE => error ("Bad directive " ^ quote cmd_expr)
   34.95    end;
   34.96  
   34.97 +
   34.98 +(** theory setup **)
   34.99 +
  34.100 +val setup = antiq_setup;
  34.101 +
  34.102  end; (*struct*)
    35.1 --- a/src/Tools/Code_Generator.thy	Mon Jun 27 17:51:28 2011 +0200
    35.2 +++ b/src/Tools/Code_Generator.thy	Mon Jun 27 22:20:49 2011 +0200
    35.3 @@ -29,6 +29,7 @@
    35.4    Solve_Direct.setup
    35.5    #> Code_Preproc.setup
    35.6    #> Code_Simp.setup
    35.7 +  #> Code_Target.setup
    35.8    #> Code_ML.setup
    35.9    #> Code_Haskell.setup
   35.10    #> Code_Scala.setup
    36.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Mon Jun 27 17:51:28 2011 +0200
    36.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Mon Jun 27 22:20:49 2011 +0200
    36.3 @@ -115,7 +115,9 @@
    36.4        Markup.CLASS -> get_color("red"),
    36.5        Markup.TYPE -> get_color("black"),
    36.6        Markup.CONSTANT -> get_color("black"),
    36.7 -      Markup.ML_ANTIQUOTATION -> get_color("black"))
    36.8 +      Markup.ML_ANTIQUOTATION -> get_color("black"),
    36.9 +      Markup.DOCUMENT_ANTIQUOTATION -> get_color("black"),
   36.10 +      Markup.DOCUMENT_ANTIQUOTATION_OPTION -> get_color("black"))
   36.11  
   36.12    private val text_colors: Map[String, Color] =
   36.13      Map(