# HG changeset patch # User wenzelm # Date 1309206049 -7200 # Node ID 9864182c6bad456e28b7fbfa1284741f992ef641 # Parent aeabb735883a3ad23cff735ce962db83e4ba61d7 document antiquotations are managed as theory data, with proper name space and entity markup; diff -r aeabb735883a -r 9864182c6bad doc-src/Classes/Thy/Setup.thy --- a/doc-src/Classes/Thy/Setup.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/Classes/Thy/Setup.thy Mon Jun 27 22:20:49 2011 +0200 @@ -5,7 +5,11 @@ "../../more_antiquote.ML" begin -setup {* Code_Target.set_default_code_width 74 *} +setup {* + Antiquote_Setup.setup #> + More_Antiquote.setup #> + Code_Target.set_default_code_width 74 +*} syntax "_alpha" :: "type" ("\") diff -r aeabb735883a -r 9864182c6bad doc-src/Codegen/Thy/Setup.thy --- a/doc-src/Codegen/Thy/Setup.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/Codegen/Thy/Setup.thy Mon Jun 27 22:20:49 2011 +0200 @@ -8,6 +8,8 @@ begin setup {* + Antiquote_Setup.setup #> + More_Antiquote.setup #> let val typ = Simple_Syntax.read_typ; in diff -r aeabb735883a -r 9864182c6bad doc-src/IsarImplementation/Thy/Base.thy --- a/doc-src/IsarImplementation/Thy/Base.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Base.thy Mon Jun 27 22:20:49 2011 +0200 @@ -3,4 +3,6 @@ uses "../../antiquote_setup.ML" begin +setup {* Antiquote_Setup.setup *} + end diff -r aeabb735883a -r 9864182c6bad doc-src/IsarImplementation/Thy/document/Base.tex --- a/doc-src/IsarImplementation/Thy/document/Base.tex Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Base.tex Mon Jun 27 22:20:49 2011 +0200 @@ -11,8 +11,37 @@ \ Base\isanewline \isakeyword{imports}\ Main\isanewline \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 -\isakeyword{begin}\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +\isanewline +% +\endisadelimtheory +% +\isadelimML \isanewline +% +\endisadelimML +% +\isatagML +\isacommand{setup}\isamarkupfalse% +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}% +\endisatagML +{\isafoldML}% +% +\isadelimML +\isanewline +% +\endisadelimML +% +\isadelimtheory +\isanewline +% +\endisadelimtheory +% +\isatagtheory \isacommand{end}\isamarkupfalse% % \endisatagtheory diff -r aeabb735883a -r 9864182c6bad doc-src/IsarRef/Thy/Base.thy --- a/doc-src/IsarRef/Thy/Base.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/IsarRef/Thy/Base.thy Mon Jun 27 22:20:49 2011 +0200 @@ -4,6 +4,7 @@ begin setup {* + Antiquote_Setup.setup #> member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup *} diff -r aeabb735883a -r 9864182c6bad doc-src/Main/Docs/Main_Doc.thy --- a/doc-src/Main/Docs/Main_Doc.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/Main/Docs/Main_Doc.thy Mon Jun 27 22:20:49 2011 +0200 @@ -3,16 +3,19 @@ imports Main begin -ML {* -fun pretty_term_type_only ctxt (t, T) = - (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () - else error "term_type_only: type mismatch"; - Syntax.pretty_typ ctxt T) - -val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev) - (fn {source, context = ctxt, ...} => fn arg => - Thy_Output.output ctxt - (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg])); +setup {* + let + fun pretty_term_type_only ctxt (t, T) = + (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () + else error "term_type_only: type mismatch"; + Syntax.pretty_typ ctxt T) + in + Thy_Output.antiquotation @{binding term_type_only} + (Args.term -- Args.typ_abbrev) + (fn {source, context = ctxt, ...} => fn arg => + Thy_Output.output ctxt + (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg])) + end *} (*>*) text{* diff -r aeabb735883a -r 9864182c6bad doc-src/System/IsaMakefile --- a/doc-src/System/IsaMakefile Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/System/IsaMakefile Mon Jun 27 22:20:49 2011 +0200 @@ -22,7 +22,7 @@ Pure-System: $(LOG)/Pure-System.gz $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \ - Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy + Thy/Base.thy Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy @$(USEDIR) -s System Pure Thy @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \ Thy/document/pdfsetup.sty Thy/document/session.tex diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/Base.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/Base.thy Mon Jun 27 22:20:49 2011 +0200 @@ -0,0 +1,10 @@ +theory Base +imports Pure +uses "../../antiquote_setup.ML" +begin + +setup {* Antiquote_Setup.setup *} + +declare [[thy_output_source]] + +end diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/System/Thy/Basics.thy Mon Jun 27 22:20:49 2011 +0200 @@ -1,5 +1,5 @@ theory Basics -imports Pure +imports Base begin chapter {* The Isabelle system environment *} diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/Interfaces.thy --- a/doc-src/System/Thy/Interfaces.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/System/Thy/Interfaces.thy Mon Jun 27 22:20:49 2011 +0200 @@ -1,5 +1,5 @@ theory Interfaces -imports Pure +imports Base begin chapter {* User interfaces *} diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/Misc.thy --- a/doc-src/System/Thy/Misc.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/System/Thy/Misc.thy Mon Jun 27 22:20:49 2011 +0200 @@ -1,5 +1,5 @@ theory Misc -imports Pure +imports Base begin chapter {* Miscellaneous tools \label{ch:tools} *} diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/System/Thy/Presentation.thy Mon Jun 27 22:20:49 2011 +0200 @@ -1,5 +1,5 @@ theory Presentation -imports Pure +imports Base begin chapter {* Presenting theories \label{ch:present} *} diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/ROOT.ML --- a/doc-src/System/Thy/ROOT.ML Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/System/Thy/ROOT.ML Mon Jun 27 22:20:49 2011 +0200 @@ -1,4 +1,1 @@ -Thy_Output.source_default := true; -use "../../antiquote_setup.ML"; - use_thys ["Basics", "Interfaces", "Presentation", "Misc"]; diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/document/Base.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/document/Base.tex Mon Jun 27 22:20:49 2011 +0200 @@ -0,0 +1,61 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Base}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Base\isanewline +\isakeyword{imports}\ Pure\isanewline +\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 +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +\isanewline +% +\endisadelimtheory +% +\isadelimML +\isanewline +% +\endisadelimML +% +\isatagML +\isacommand{setup}\isamarkupfalse% +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}% +\endisatagML +{\isafoldML}% +% +\isadelimML +\isanewline +% +\endisadelimML +\isanewline +\isacommand{declare}\isamarkupfalse% +\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}thy{\isaliteral{5F}{\isacharunderscore}}output{\isaliteral{5F}{\isacharunderscore}}source{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline +% +\isadelimtheory +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +\isanewline +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/System/Thy/document/Basics.tex Mon Jun 27 22:20:49 2011 +0200 @@ -9,7 +9,7 @@ \isatagtheory \isacommand{theory}\isamarkupfalse% \ Basics\isanewline -\isakeyword{imports}\ Pure\isanewline +\isakeyword{imports}\ Base\isanewline \isakeyword{begin}% \endisatagtheory {\isafoldtheory}% diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/document/Interfaces.tex --- a/doc-src/System/Thy/document/Interfaces.tex Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/System/Thy/document/Interfaces.tex Mon Jun 27 22:20:49 2011 +0200 @@ -9,7 +9,7 @@ \isatagtheory \isacommand{theory}\isamarkupfalse% \ Interfaces\isanewline -\isakeyword{imports}\ Pure\isanewline +\isakeyword{imports}\ Base\isanewline \isakeyword{begin}% \endisatagtheory {\isafoldtheory}% diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/document/Misc.tex --- a/doc-src/System/Thy/document/Misc.tex Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/System/Thy/document/Misc.tex Mon Jun 27 22:20:49 2011 +0200 @@ -9,7 +9,7 @@ \isatagtheory \isacommand{theory}\isamarkupfalse% \ Misc\isanewline -\isakeyword{imports}\ Pure\isanewline +\isakeyword{imports}\ Base\isanewline \isakeyword{begin}% \endisatagtheory {\isafoldtheory}% diff -r aeabb735883a -r 9864182c6bad doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/System/Thy/document/Presentation.tex Mon Jun 27 22:20:49 2011 +0200 @@ -9,7 +9,7 @@ \isatagtheory \isacommand{theory}\isamarkupfalse% \ Presentation\isanewline -\isakeyword{imports}\ Pure\isanewline +\isakeyword{imports}\ Base\isanewline \isakeyword{begin}% \endisatagtheory {\isafoldtheory}% diff -r aeabb735883a -r 9864182c6bad doc-src/TutorialI/Inductive/Advanced.thy --- a/doc-src/TutorialI/Inductive/Advanced.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/TutorialI/Inductive/Advanced.thy Mon Jun 27 22:20:49 2011 +0200 @@ -1,4 +1,6 @@ -(*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*) +(*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin +setup {* Antiquote_Setup.setup *} +(*>*) text {* The premises of introduction rules may contain universal quantifiers and diff -r aeabb735883a -r 9864182c6bad doc-src/TutorialI/Inductive/Even.thy --- a/doc-src/TutorialI/Inductive/Even.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/TutorialI/Inductive/Even.thy Mon Jun 27 22:20:49 2011 +0200 @@ -1,4 +1,6 @@ -(*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin(*>*) +(*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin +setup {* Antiquote_Setup.setup *} +(*>*) section{* The Set of Even Numbers *} diff -r aeabb735883a -r 9864182c6bad doc-src/TutorialI/Inductive/document/Advanced.tex --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Jun 27 22:20:49 2011 +0200 @@ -15,6 +15,19 @@ % \endisadelimtheory % +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% \begin{isamarkuptext}% The premises of introduction rules may contain universal quantifiers and monotone functions. A universal quantifier lets the rule diff -r aeabb735883a -r 9864182c6bad doc-src/TutorialI/Inductive/document/Even.tex --- a/doc-src/TutorialI/Inductive/document/Even.tex Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Mon Jun 27 22:20:49 2011 +0200 @@ -15,6 +15,19 @@ % \endisadelimtheory % +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% \isamarkupsection{The Set of Even Numbers% } \isamarkuptrue% diff -r aeabb735883a -r 9864182c6bad doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Mon Jun 27 22:20:49 2011 +0200 @@ -9,6 +9,7 @@ header{*Theory of Agents and Messages for Security Protocols*} theory Message imports Main uses "../../antiquote_setup.ML" begin +setup {* Antiquote_Setup.setup *} (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) lemma [simp] : "A \ (B \ A) = B \ A" diff -r aeabb735883a -r 9864182c6bad doc-src/TutorialI/Protocol/document/Message.tex --- a/doc-src/TutorialI/Protocol/document/Message.tex Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/TutorialI/Protocol/document/Message.tex Mon Jun 27 22:20:49 2011 +0200 @@ -15,6 +15,19 @@ % \endisadelimtheory % +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% \isadelimproof % \endisadelimproof diff -r aeabb735883a -r 9864182c6bad doc-src/TutorialI/Types/Setup.thy --- a/doc-src/TutorialI/Types/Setup.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/TutorialI/Types/Setup.thy Mon Jun 27 22:20:49 2011 +0200 @@ -5,4 +5,7 @@ "../../more_antiquote.ML" begin +setup {* Antiquote_Setup.setup #> More_Antiquote.setup *} + + end \ No newline at end of file diff -r aeabb735883a -r 9864182c6bad doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/antiquote_setup.ML Mon Jun 27 22:20:49 2011 +0200 @@ -4,7 +4,12 @@ Auxiliary antiquotations for the Isabelle manuals. *) -structure Antiquote_Setup: sig end = +signature ANTIQUOTE_SETUP = +sig + val setup: theory -> theory +end; + +structure Antiquote_Setup: ANTIQUOTE_SETUP = struct (* misc utils *) @@ -35,8 +40,9 @@ val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; -val _ = Thy_Output.antiquotation "verbatim" (Scan.lift Args.name) - (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")); +val verbatim_setup = + Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name) + (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")); (* ML text *) @@ -87,42 +93,45 @@ in -val _ = index_ml "index_ML" "" ml_val; -val _ = index_ml "index_ML_type" "type" ml_type; -val _ = index_ml "index_ML_exn" "exception" ml_exn; -val _ = index_ml "index_ML_structure" "structure" ml_structure; -val _ = index_ml "index_ML_functor" "functor" ml_functor; +val index_ml_setup = + index_ml @{binding index_ML} "" ml_val #> + index_ml @{binding index_ML_type} "type" ml_type #> + index_ml @{binding index_ML_exn} "exception" ml_exn #> + index_ml @{binding index_ML_structure} "structure" ml_structure #> + index_ml @{binding index_ML_functor} "functor" ml_functor; end; (* named theorems *) -val _ = Thy_Output.antiquotation "named_thms" - (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) - (fn {context = ctxt, ...} => - map (apfst (Thy_Output.pretty_thm ctxt)) - #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I) - #> (if Config.get ctxt Thy_Output.display - then - map (fn (p, name) => - Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^ - "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") - #> space_implode "\\par\\smallskip%\n" - #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" - else - map (fn (p, name) => - Output.output (Pretty.str_of p) ^ - "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") - #> space_implode "\\par\\smallskip%\n" - #> enclose "\\isa{" "}")); +val named_thms_setup = + Thy_Output.antiquotation @{binding named_thms} + (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) + (fn {context = ctxt, ...} => + map (apfst (Thy_Output.pretty_thm ctxt)) + #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I) + #> (if Config.get ctxt Thy_Output.display + then + map (fn (p, name) => + Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^ + "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") + #> space_implode "\\par\\smallskip%\n" + #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" + else + map (fn (p, name) => + Output.output (Pretty.str_of p) ^ + "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") + #> space_implode "\\par\\smallskip%\n" + #> enclose "\\isa{" "}")); (* theory file *) -val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name) - (fn {context = ctxt, ...} => - fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])); +val thy_file_setup = + Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name) + (fn {context = ctxt, ...} => + fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])); (* Isabelle/Isar entities (with index) *) @@ -142,8 +151,8 @@ fun entity check markup kind index = Thy_Output.antiquotation - (translate (fn " " => "_" | c => c) kind ^ - (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")) + (Binding.name (translate (fn " " => "_" | c => c) kind ^ + (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name)) (fn {context = ctxt, ...} => fn (logic, name) => let @@ -170,32 +179,44 @@ end); fun entity_antiqs check markup kind = - ((entity check markup kind NONE); - (entity check markup kind (SOME true)); - (entity check markup kind (SOME false))); + entity check markup kind NONE #> + entity check markup kind (SOME true) #> + entity check markup kind (SOME false); in -val _ = entity_antiqs no_check "" "syntax"; -val _ = entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command"; -val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword"; -val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "element"; -val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method"; -val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute"; -val _ = entity_antiqs no_check "" "fact"; -val _ = entity_antiqs no_check "" "variable"; -val _ = entity_antiqs no_check "" "case"; -val _ = entity_antiqs (K Thy_Output.defined_command) "" "antiquotation"; -val _ = entity_antiqs (K Thy_Output.defined_option) "" "antiquotation option"; -val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting"; -val _ = entity_antiqs no_check "" "inference"; -val _ = entity_antiqs no_check "isatt" "executable"; -val _ = entity_antiqs (K check_tool) "isatt" "tool"; -val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory"; -val _ = - entity_antiqs - (thy_check ML_Context.intern_antiq ML_Context.defined_antiq) "" Markup.ML_antiquotationN; +val entity_setup = + entity_antiqs no_check "" "syntax" #> + entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command" #> + entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword" #> + entity_antiqs (K Keyword.is_keyword) "isakeyword" "element" #> + entity_antiqs (thy_check Method.intern Method.defined) "" "method" #> + entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" #> + entity_antiqs no_check "" "fact" #> + entity_antiqs no_check "" "variable" #> + entity_antiqs no_check "" "case" #> + entity_antiqs (thy_check Thy_Output.intern_command Thy_Output.defined_command) + "" "antiquotation" #> + entity_antiqs (thy_check Thy_Output.intern_option Thy_Output.defined_option) + "" "antiquotation option" #> + entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" #> + entity_antiqs no_check "" "inference" #> + entity_antiqs no_check "isatt" "executable" #> + entity_antiqs (K check_tool) "isatt" "tool" #> + entity_antiqs (K (can Thy_Info.get_theory)) "" "theory" #> + entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq) + "" Markup.ML_antiquotationN; end; + +(* theory setup *) + +val setup = + verbatim_setup #> + index_ml_setup #> + named_thms_setup #> + thy_file_setup #> + entity_setup; + end; diff -r aeabb735883a -r 9864182c6bad doc-src/more_antiquote.ML --- a/doc-src/more_antiquote.ML Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/more_antiquote.ML Mon Jun 27 22:20:49 2011 +0200 @@ -6,6 +6,7 @@ signature MORE_ANTIQUOTE = sig + val setup: theory -> theory end; structure More_Antiquote : MORE_ANTIQUOTE = @@ -40,8 +41,9 @@ in -val _ = Thy_Output.antiquotation "code_thms" Args.term - (fn {source, context, ...} => pretty_code_thm source context); +val setup = + Thy_Output.antiquotation @{binding code_thms} Args.term + (fn {source, context, ...} => pretty_code_thm source context); end; diff -r aeabb735883a -r 9864182c6bad src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Jun 27 17:51:28 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Jun 27 22:20:49 2011 +0200 @@ -237,27 +237,28 @@ (** document antiquotation **) -val _ = Thy_Output.antiquotation "datatype" (Args.type_name true) - (fn {source = src, context = ctxt, ...} => fn dtco => - let - val thy = Proof_Context.theory_of ctxt; - val (vs, cos) = the_spec thy dtco; - val ty = Type (dtco, map TFree vs); - val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt); - fun pretty_constr (co, tys) = - Pretty.block (Pretty.breaks - (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: - map pretty_typ_bracket tys)); - val pretty_datatype = - Pretty.block - (Pretty.command "datatype" :: Pretty.brk 1 :: - Syntax.pretty_typ ctxt ty :: - Pretty.str " =" :: Pretty.brk 1 :: - flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos))); - in - Thy_Output.output ctxt - (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()]) - end); +val antiq_setup = + Thy_Output.antiquotation @{binding datatype} (Args.type_name true) + (fn {source = src, context = ctxt, ...} => fn dtco => + let + val thy = Proof_Context.theory_of ctxt; + val (vs, cos) = the_spec thy dtco; + val ty = Type (dtco, map TFree vs); + val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt); + fun pretty_constr (co, tys) = + Pretty.block (Pretty.breaks + (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: + map pretty_typ_bracket tys)); + val pretty_datatype = + Pretty.block + (Pretty.command "datatype" :: Pretty.brk 1 :: + Syntax.pretty_typ ctxt ty :: + Pretty.str " =" :: Pretty.brk 1 :: + flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos))); + in + Thy_Output.output ctxt + (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()]) + end); @@ -453,6 +454,7 @@ val setup = trfun_setup #> + antiq_setup #> Datatype_Interpretation.init; diff -r aeabb735883a -r 9864182c6bad src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Mon Jun 27 17:51:28 2011 +0200 +++ b/src/Pure/General/markup.ML Mon Jun 27 22:20:49 2011 +0200 @@ -73,7 +73,8 @@ val doc_sourceN: string val doc_source: T val antiqN: string val antiq: T val ML_antiquotationN: string - val doc_antiqN: string val doc_antiq: string -> T + val doc_antiquotationN: string + val doc_antiquotation_optionN: string val keyword_declN: string val keyword_decl: string -> T val command_declN: string val command_decl: string -> string -> T val keywordN: string val keyword: T @@ -267,7 +268,8 @@ val (antiqN, antiq) = markup_elem "antiq"; val ML_antiquotationN = "ML antiquotation"; -val (doc_antiqN, doc_antiq) = markup_string "doc_antiq" nameN; +val doc_antiquotationN = "document antiquotation"; +val doc_antiquotation_optionN = "document antiquotation option"; (* outer syntax *) diff -r aeabb735883a -r 9864182c6bad src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Mon Jun 27 17:51:28 2011 +0200 +++ b/src/Pure/General/markup.scala Mon Jun 27 22:20:49 2011 +0200 @@ -190,7 +190,8 @@ val ANTIQ = "antiq" val ML_ANTIQUOTATION = "ML antiquotation" - val DOC_ANTIQ = "doc_antiq" + val DOCUMENT_ANTIQUOTATION = "document antiquotation" + val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option" /* ML syntax */ diff -r aeabb735883a -r 9864182c6bad src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Jun 27 17:51:28 2011 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Mon Jun 27 22:20:49 2011 +0200 @@ -384,7 +384,8 @@ val print_methods = Toplevel.unknown_theory o Toplevel.keep (Method.print_methods o Toplevel.theory_of); -val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations; +val print_antiquotations = + Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of); val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => let diff -r aeabb735883a -r 9864182c6bad src/Pure/Thy/rail.ML --- a/src/Pure/Thy/rail.ML Mon Jun 27 17:51:28 2011 +0200 +++ b/src/Pure/Thy/rail.ML Mon Jun 27 22:20:49 2011 +0200 @@ -259,8 +259,10 @@ in val _ = - Thy_Output.antiquotation "rail" (Scan.lift (Parse.source_position Parse.string)) - (fn {state, ...} => output_rules state o read); + Context.>> (Context.map_theory + (Thy_Output.antiquotation (Binding.name "rail") + (Scan.lift (Parse.source_position Parse.string)) + (fn {state, ...} => output_rules state o read))); end; diff -r aeabb735883a -r 9864182c6bad src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Mon Jun 27 17:51:28 2011 +0200 +++ b/src/Pure/Thy/thy_output.ML Mon Jun 27 22:20:49 2011 +0200 @@ -17,14 +17,17 @@ val source: bool Config.T val break: bool Config.T val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context - val add_option: string -> (string -> Proof.context -> Proof.context) -> unit - val defined_command: string -> bool - val defined_option: string -> bool - val print_antiquotations: unit -> unit + val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory + val intern_command: theory -> xstring -> string + val defined_command: theory -> string -> bool + val intern_option: theory -> xstring -> string + val defined_option: theory -> string -> bool + val print_antiquotations: Proof.context -> unit + val antiquotation: binding -> 'a context_parser -> + ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> + theory -> theory val boolean: string -> bool val integer: string -> int - val antiquotation: string -> 'a context_parser -> - ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> unit datatype markup = Markup | MarkupEnv | Verbatim val modes: string list Unsynchronized.ref val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string @@ -72,55 +75,66 @@ (** maintain global antiquotations **) -local - -val global_commands = - Unsynchronized.ref - (Symtab.empty: (Args.src -> Toplevel.state -> Proof.context -> string) Symtab.table); +structure Antiquotations = Theory_Data +( + type T = + (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table * + (string -> Proof.context -> Proof.context) Name_Space.table; + val empty : T = + (Name_Space.empty_table Markup.doc_antiquotationN, + Name_Space.empty_table Markup.doc_antiquotation_optionN); + val extend = I; + fun merge ((commands1, options1), (commands2, options2)) : T = + (Name_Space.merge_tables (commands1, commands2), + Name_Space.merge_tables (options1, options2)); +); -val global_options = - Unsynchronized.ref (Symtab.empty: (string -> Proof.context -> Proof.context) Symtab.table); - -fun add_item kind name item tab = - (if not (Symtab.defined tab name) then () - else warning ("Redefined document antiquotation " ^ kind ^ ": " ^ quote name); - Symtab.update (name, item) tab); - -in +fun add_command name cmd thy = + thy |> Antiquotations.map + (apfst + (Name_Space.define + (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, cmd) #> snd)); -fun add_command name cmd = - CRITICAL (fn () => Unsynchronized.change global_commands (add_item "command" name cmd)); -fun add_option name opt = - CRITICAL (fn () => Unsynchronized.change global_options (add_item "option" name opt)); +fun add_option name opt thy = + thy |> Antiquotations.map + (apsnd + (Name_Space.define + (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, opt) #> snd)); -fun defined_command name = Symtab.defined (! global_commands) name; -fun defined_option name = Symtab.defined (! global_options) name; +val intern_command = Name_Space.intern o #1 o #1 o Antiquotations.get; +val defined_command = Symtab.defined o #2 o #1 o Antiquotations.get; -fun command src = - let val ((name, _), pos) = Args.dest_src src in - (case Symtab.lookup (! global_commands) name of - NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos) - | SOME f => - (Position.report pos (Markup.doc_antiq name); - (fn state => fn ctxt => f src state ctxt handle ERROR msg => - cat_error msg ("The error(s) above occurred in document antiquotation: " ^ - quote name ^ Position.str_of pos)))) +val intern_option = Name_Space.intern o #1 o #2 o Antiquotations.get; +val defined_option = Symtab.defined o #2 o #2 o Antiquotations.get; + +fun command src state ctxt = + let + val thy = Proof_Context.theory_of ctxt; + val ((xname, _), pos) = Args.dest_src src; + val (name, f) = Name_Space.check ctxt (#1 (Antiquotations.get thy)) (xname, pos); + in + f src state ctxt handle ERROR msg => + cat_error msg ("The error(s) above occurred in document antiquotation: " ^ + quote name ^ Position.str_of pos) end; -fun option (name, s) ctxt = - (case Symtab.lookup (! global_options) name of - NONE => error ("Unknown document antiquotation option: " ^ quote name) - | SOME opt => opt s ctxt); - +fun option ((xname, pos), s) ctxt = + let + val thy = Proof_Context.theory_of ctxt; + val (_, opt) = Name_Space.check ctxt (#2 (Antiquotations.get thy)) (xname, pos); + in opt s ctxt end; -fun print_antiquotations () = - [Pretty.big_list "document antiquotation commands:" - (map Pretty.str (sort_strings (Symtab.keys (! global_commands)))), - Pretty.big_list "document antiquotation options:" - (map Pretty.str (sort_strings (Symtab.keys (! global_options))))] - |> Pretty.chunks |> Pretty.writeln; - -end; +fun print_antiquotations ctxt = + let + val thy = Proof_Context.theory_of ctxt; + val (commands, options) = Antiquotations.get thy; + val command_names = map #1 (Name_Space.extern_table ctxt commands); + val option_names = map #1 (Name_Space.extern_table ctxt options); + in + [Pretty.big_list "document antiquotations:" (map Pretty.str command_names), + Pretty.big_list "document antiquotation options:" (map Pretty.str option_names)] + |> Pretty.chunks |> Pretty.writeln + end; fun antiquotation name scan out = add_command name @@ -152,7 +166,7 @@ local val property = - Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) ""; + Parse.position Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) ""; val properties = Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) []; @@ -445,23 +459,25 @@ (* options *) -val _ = add_option "show_types" (Config.put show_types o boolean); -val _ = add_option "show_sorts" (Config.put show_sorts o boolean); -val _ = add_option "show_structs" (Config.put show_structs o boolean); -val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean); -val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean); -val _ = add_option "names_long" (Config.put Name_Space.names_long o boolean); -val _ = add_option "names_short" (Config.put Name_Space.names_short o boolean); -val _ = add_option "names_unique" (Config.put Name_Space.names_unique o boolean); -val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean); -val _ = add_option "display" (Config.put display o boolean); -val _ = add_option "break" (Config.put break o boolean); -val _ = add_option "quotes" (Config.put quotes o boolean); -val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single); -val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer); -val _ = add_option "indent" (Config.put indent o integer); -val _ = add_option "source" (Config.put source o boolean); -val _ = add_option "goals_limit" (Config.put Goal_Display.goals_limit o integer); +val _ = + Context.>> (Context.map_theory + (add_option (Binding.name "show_types") (Config.put show_types o boolean) #> + add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #> + add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #> + add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #> + add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #> + add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #> + add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #> + add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #> + add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #> + add_option (Binding.name "display") (Config.put display o boolean) #> + add_option (Binding.name "break") (Config.put break o boolean) #> + add_option (Binding.name "quotes") (Config.put quotes o boolean) #> + add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #> + add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #> + add_option (Binding.name "indent") (Config.put indent o integer) #> + add_option (Binding.name "source") (Config.put source o boolean) #> + add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer))); (* basic pretty printing *) @@ -562,22 +578,26 @@ in -val _ = basic_entities_style "thm" (Term_Style.parse -- Attrib.thms) pretty_thm_style; -val _ = basic_entity "prop" (Term_Style.parse -- Args.prop) pretty_term_style; -val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style; -val _ = basic_entity "term_type" (Term_Style.parse -- Args.term) pretty_term_typ; -val _ = basic_entity "typeof" (Term_Style.parse -- Args.term) pretty_term_typeof; -val _ = basic_entity "const" (Args.const_proper false) pretty_const; -val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev; -val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ; -val _ = basic_entity "class" (Scan.lift Args.name) pretty_class; -val _ = basic_entity "type" (Scan.lift Args.name) pretty_type; -val _ = basic_entity "text" (Scan.lift Args.name) pretty_text; -val _ = basic_entities "prf" Attrib.thms (pretty_prf false); -val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true); -val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory; -val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style; -val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style; +val _ = + Context.>> (Context.map_theory + (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #> + basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #> + basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #> + basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #> + basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #> + basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #> + basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #> + basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #> + basic_entity (Binding.name "class") (Scan.lift Args.name) pretty_class #> + basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #> + basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #> + basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #> + basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #> + basic_entity (Binding.name "theory") (Scan.lift Args.name) pretty_theory #> + basic_entities_style (Binding.name "thm_style") + (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style #> + basic_entity (Binding.name "term_style") + (Term_Style.parse_bare -- Args.term) pretty_term_style)); end; @@ -598,8 +618,10 @@ in -val _ = goal_state "goals" true; -val _ = goal_state "subgoals" false; +val _ = + Context.>> (Context.map_theory + (goal_state (Binding.name "goals") true #> + goal_state (Binding.name "subgoals") false)); end; @@ -608,16 +630,19 @@ val _ = Keyword.keyword "by"; -val _ = antiquotation "lemma" - (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse)) - (fn {source, context, ...} => fn (prop, methods) => - let - val prop_src = - (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos)); - val _ = context - |> Proof.theorem NONE (K I) [[(prop, [])]] - |> Proof.global_terminal_proof methods; - in output context (maybe_pretty_source pretty_term context prop_src [prop]) end); +val _ = + Context.>> (Context.map_theory + (antiquotation (Binding.name "lemma") + (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse)) + (fn {source, context, ...} => fn (prop, methods) => + let + val prop_src = + (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos)); + (* FIXME check proof!? *) + val _ = context + |> Proof.theorem NONE (K I) [[(prop, [])]] + |> Proof.global_terminal_proof methods; + in output context (maybe_pretty_source pretty_term context prop_src [prop]) end))); (* ML text *) @@ -642,25 +667,30 @@ in -val _ = ml_text "ML" (ml_enclose "fn _ => (" ");"); -val _ = ml_text "ML_type" (ml_enclose "val _ = NONE : (" ") option;"); -val _ = ml_text "ML_struct" (ml_enclose "functor XXX() = struct structure XX = " " end;"); +val _ = + Context.>> (Context.map_theory + (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #> + ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #> + ml_text (Binding.name "ML_struct") + (ml_enclose "functor XXX() = struct structure XX = " " end;") #> -val _ = ml_text "ML_functor" (* FIXME formal treatment of functor name (!?) *) - (fn pos => fn txt => - ML_Lex.read Position.none ("ML_Env.check_functor " ^ - ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))); + ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *) + (fn pos => fn txt => + ML_Lex.read Position.none ("ML_Env.check_functor " ^ + ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #> -val _ = ml_text "ML_text" (K (K [])); + ml_text (Binding.name "ML_text") (K (K [])))); end; (* files *) -val _ = antiquotation "file" (Scan.lift Args.name) - (fn {context, ...} => fn path => - if File.exists (Path.explode path) then verb_text path - else error ("Bad file: " ^ quote path)); +val _ = + Context.>> (Context.map_theory + (antiquotation (Binding.name "file") (Scan.lift Args.name) + (fn _ => fn path => + if File.exists (Path.explode path) then verb_text path + else error ("Bad file: " ^ quote path)))); end; diff -r aeabb735883a -r 9864182c6bad src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Jun 27 17:51:28 2011 +0200 +++ b/src/Tools/Code/code_target.ML Mon Jun 27 22:20:49 2011 +0200 @@ -60,6 +60,8 @@ val add_include: string -> string * (string * string list) option -> theory -> theory val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit + + val setup: theory -> theory end; structure Code_Target : CODE_TARGET = @@ -143,7 +145,7 @@ }; fun make_target ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))) = - Target { serial = serial, description = description, reserved = reserved, + Target { serial = serial, description = description, reserved = reserved, includes = includes, module_alias = module_alias, symbol_syntax = symbol_syntax }; fun map_target f ( Target { serial, description, reserved, includes, module_alias, symbol_syntax } ) = make_target (f ((serial, description), ((reserved, includes), (module_alias, symbol_syntax)))); @@ -199,7 +201,7 @@ | _ => true); val _ = if overwriting then warning ("Overwriting existing target " ^ quote target) - else (); + else (); in thy |> (Targets.map o apfst o apfst o Symtab.update) @@ -251,7 +253,7 @@ fun collapse_hierarchy thy = let val ((targets, _), _) = Targets.get thy; - fun collapse target = + fun collapse target = let val data = case Symtab.lookup targets target of SOME data => data @@ -352,7 +354,7 @@ val serializer = case the_description data of Fundamental seri => #serializer seri; val reserved = the_reserved data; - val module_alias = the_module_alias data + val module_alias = the_module_alias data val { class, instance, tyco, const } = the_symbol_syntax data; val literals = the_literals thy target; val (prepared_serializer, prepared_program) = prepare_serializer thy @@ -396,7 +398,7 @@ val { env_var, make_destination, make_command } = (#check o the_fundamental thy) target; fun ext_check p = - let + let val destination = make_destination p; val _ = export (SOME destination) (invoke_serializer thy target (SOME 80) module_name args naming program names_cs); @@ -495,7 +497,7 @@ fun parse_names category parse internalize lookup = Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs); - + val parse_consts = parse_names "consts" Args.term Code.check_const Code_Thingol.lookup_const ; @@ -511,15 +513,17 @@ in -val _ = Thy_Output.antiquotation "code_stmts" - (parse_const_terms -- Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances) - -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int))) - (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) => - let val thy = Proof_Context.theory_of ctxt in - present_code thy (mk_cs thy) - (fn naming => maps (fn f => f thy naming) mk_stmtss) - target some_width "Example" [] - end); +val antiq_setup = + Thy_Output.antiquotation @{binding code_stmts} + (parse_const_terms -- + Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances) + -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int))) + (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) => + let val thy = Proof_Context.theory_of ctxt in + present_code thy (mk_cs thy) + (fn naming => maps (fn f => f thy naming) mk_stmtss) + target some_width "Example" [] + end); end; @@ -745,4 +749,9 @@ | NONE => error ("Bad directive " ^ quote cmd_expr) end; + +(** theory setup **) + +val setup = antiq_setup; + end; (*struct*) diff -r aeabb735883a -r 9864182c6bad src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/src/Tools/Code_Generator.thy Mon Jun 27 22:20:49 2011 +0200 @@ -29,6 +29,7 @@ Solve_Direct.setup #> Code_Preproc.setup #> Code_Simp.setup + #> Code_Target.setup #> Code_ML.setup #> Code_Haskell.setup #> Code_Scala.setup diff -r aeabb735883a -r 9864182c6bad src/Tools/jEdit/src/isabelle_markup.scala --- a/src/Tools/jEdit/src/isabelle_markup.scala Mon Jun 27 17:51:28 2011 +0200 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Mon Jun 27 22:20:49 2011 +0200 @@ -115,7 +115,9 @@ Markup.CLASS -> get_color("red"), Markup.TYPE -> get_color("black"), Markup.CONSTANT -> get_color("black"), - Markup.ML_ANTIQUOTATION -> get_color("black")) + Markup.ML_ANTIQUOTATION -> get_color("black"), + Markup.DOCUMENT_ANTIQUOTATION -> get_color("black"), + Markup.DOCUMENT_ANTIQUOTATION_OPTION -> get_color("black")) private val text_colors: Map[String, Color] = Map(