# HG changeset patch # User wenzelm # Date 1309207484 -7200 # Node ID c3e4d280bdebaed59f72bf359f228000d1d4a869 # Parent 023a1d1f97bdd52c9ce32d5103d1260c8df131e1# Parent 486b56f2139ce869a483c9ce41017899eda6f457 merged diff -r 023a1d1f97bd -r c3e4d280bdeb NEWS --- a/NEWS Mon Jun 27 17:04:04 2011 +0200 +++ b/NEWS Mon Jun 27 22:44:44 2011 +0200 @@ -141,6 +141,9 @@ *** ML *** +* Antiquotations for ML and document preparation are managed as theory +data, which requires explicit setup. + * Isabelle_Process.is_active allows tools to check if the official process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop (better known as Proof General). diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/Classes/Thy/Setup.thy --- a/doc-src/Classes/Thy/Setup.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/Classes/Thy/Setup.thy Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/Codegen/Thy/Setup.thy --- a/doc-src/Codegen/Thy/Setup.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/Codegen/Thy/Setup.thy Mon Jun 27 22:44:44 2011 +0200 @@ -8,6 +8,8 @@ begin setup {* + Antiquote_Setup.setup #> + More_Antiquote.setup #> let val typ = Simple_Syntax.read_typ; in diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/Codegen/Thy/document/Foundations.tex --- a/doc-src/Codegen/Thy/document/Foundations.tex Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Mon Jun 27 22:44:44 2011 +0200 @@ -571,7 +571,7 @@ language. \ditem{\emph{Inspect code equations}.} Code equations are the central - carrier of code generation. Most problems occuring while generating + carrier of code generation. Most problems occurring while generating code can be traced to single equations which are printed as part of the error message. A closer inspection of those may offer the key for solving issues (cf.~\secref{sec:equations}). diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/IsarImplementation/Thy/Base.thy --- a/doc-src/IsarImplementation/Thy/Base.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Base.thy Mon Jun 27 22:44:44 2011 +0200 @@ -3,4 +3,6 @@ uses "../../antiquote_setup.ML" begin +setup {* Antiquote_Setup.setup *} + end diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/IsarImplementation/Thy/document/Base.tex --- a/doc-src/IsarImplementation/Thy/document/Base.tex Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Base.tex Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/IsarRef/Thy/Base.thy --- a/doc-src/IsarRef/Thy/Base.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/IsarRef/Thy/Base.thy Mon Jun 27 22:44:44 2011 +0200 @@ -4,6 +4,7 @@ begin setup {* + Antiquote_Setup.setup #> member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup *} diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/Main/Docs/Main_Doc.thy --- a/doc-src/Main/Docs/Main_Doc.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/Main/Docs/Main_Doc.thy Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/System/IsaMakefile --- a/doc-src/System/IsaMakefile Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/System/IsaMakefile Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb 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:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/System/Thy/Basics.thy Mon Jun 27 22:44:44 2011 +0200 @@ -1,5 +1,5 @@ theory Basics -imports Pure +imports Base begin chapter {* The Isabelle system environment *} diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/System/Thy/Interfaces.thy --- a/doc-src/System/Thy/Interfaces.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/System/Thy/Interfaces.thy Mon Jun 27 22:44:44 2011 +0200 @@ -1,5 +1,5 @@ theory Interfaces -imports Pure +imports Base begin chapter {* User interfaces *} diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/System/Thy/Misc.thy --- a/doc-src/System/Thy/Misc.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/System/Thy/Misc.thy Mon Jun 27 22:44:44 2011 +0200 @@ -1,5 +1,5 @@ theory Misc -imports Pure +imports Base begin chapter {* Miscellaneous tools \label{ch:tools} *} diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/System/Thy/Presentation.thy Mon Jun 27 22:44:44 2011 +0200 @@ -1,5 +1,5 @@ theory Presentation -imports Pure +imports Base begin chapter {* Presenting theories \label{ch:present} *} diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/System/Thy/ROOT.ML --- a/doc-src/System/Thy/ROOT.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/System/Thy/ROOT.ML Mon Jun 27 22:44:44 2011 +0200 @@ -1,4 +1,1 @@ -Thy_Output.source_default := true; -use "../../antiquote_setup.ML"; - use_thys ["Basics", "Interfaces", "Presentation", "Misc"]; diff -r 023a1d1f97bd -r c3e4d280bdeb 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:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/System/Thy/document/Basics.tex Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/System/Thy/document/Interfaces.tex --- a/doc-src/System/Thy/document/Interfaces.tex Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/System/Thy/document/Interfaces.tex Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/System/Thy/document/Misc.tex --- a/doc-src/System/Thy/document/Misc.tex Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/System/Thy/document/Misc.tex Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/System/Thy/document/Presentation.tex Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/TutorialI/Inductive/Advanced.thy --- a/doc-src/TutorialI/Inductive/Advanced.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/TutorialI/Inductive/Advanced.thy Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/TutorialI/Inductive/Even.thy --- a/doc-src/TutorialI/Inductive/Even.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/TutorialI/Inductive/Even.thy Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/TutorialI/Inductive/document/Advanced.tex --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/TutorialI/Inductive/document/Even.tex --- a/doc-src/TutorialI/Inductive/document/Even.tex Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Mon Jun 27 22:44:44 2011 +0200 @@ -15,6 +15,19 @@ % \endisadelimtheory % +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% \isamarkupsection{The Set of Even Numbers% } \isamarkuptrue% diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/TutorialI/Protocol/document/Message.tex --- a/doc-src/TutorialI/Protocol/document/Message.tex Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/TutorialI/Protocol/document/Message.tex Mon Jun 27 22:44:44 2011 +0200 @@ -15,6 +15,19 @@ % \endisadelimtheory % +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% \isadelimproof % \endisadelimproof diff -r 023a1d1f97bd -r c3e4d280bdeb doc-src/TutorialI/Types/Setup.thy --- a/doc-src/TutorialI/Types/Setup.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/TutorialI/Types/Setup.thy Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/antiquote_setup.ML Mon Jun 27 22:44:44 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,30 +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 no_check "" "ML antiquotation"; (* FIXME proper check *) +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 023a1d1f97bd -r c3e4d280bdeb doc-src/more_antiquote.ML --- a/doc-src/more_antiquote.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/doc-src/more_antiquote.ML Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb src/FOL/FOL.thy --- a/src/FOL/FOL.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/src/FOL/FOL.thy Mon Jun 27 22:44:44 2011 +0200 @@ -177,12 +177,15 @@ val hyp_subst_tacs = [hyp_subst_tac] ); -ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())"); - structure Basic_Classical: BASIC_CLASSICAL = Cla; open Basic_Classical; *} +setup {* + ML_Antiquote.value @{binding claset} + (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())") +*} + setup Cla.setup (*Propositional rules*) diff -r 023a1d1f97bd -r c3e4d280bdeb src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/src/HOL/HOL.thy Mon Jun 27 22:44:44 2011 +0200 @@ -853,9 +853,11 @@ structure Basic_Classical: BASIC_CLASSICAL = Classical; open Basic_Classical; +*} -ML_Antiquote.value "claset" - (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())"); +setup {* + ML_Antiquote.value @{binding claset} + (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())") *} setup Classical.setup diff -r 023a1d1f97bd -r c3e4d280bdeb src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/src/HOL/Quickcheck_Narrowing.thy Mon Jun 27 22:44:44 2011 +0200 @@ -435,6 +435,7 @@ hide_type code_int narrowing_type narrowing_term cons property hide_const int_of of_int nth error toEnum marker empty C cons conv nonEmpty "apply" sum ensure_testable all exists +hide_const (open) Var Ctr hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def diff -r 023a1d1f97bd -r c3e4d280bdeb src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Jun 27 22:44:44 2011 +0200 @@ -247,27 +247,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); @@ -463,6 +464,7 @@ val setup = trfun_setup #> + antiq_setup #> Datatype_Interpretation.init; diff -r 023a1d1f97bd -r c3e4d280bdeb src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jun 27 22:44:44 2011 +0200 @@ -320,7 +320,7 @@ do_formula pos body_t #> (if also_skolems andalso will_surely_be_skolemized then add_pconst_to_table true - (gensym skolem_prefix, PType (order_of_type abs_T, [])) + (legacy_gensym skolem_prefix, PType (order_of_type abs_T, [])) else I) and do_term_or_formula ext_arg T = diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/General/markup.ML Mon Jun 27 22:44:44 2011 +0200 @@ -72,8 +72,9 @@ val ML_sourceN: string val ML_source: T val doc_sourceN: string val doc_source: T val antiqN: string val antiq: T - val ML_antiqN: string val ML_antiq: string -> T - val doc_antiqN: string val doc_antiq: string -> T + val ML_antiquotationN: string + 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 @@ -266,8 +267,9 @@ val (doc_sourceN, doc_source) = markup_elem "doc_source"; val (antiqN, antiq) = markup_elem "antiq"; -val (ML_antiqN, ML_antiq) = markup_string "ML_antiq" nameN; -val (doc_antiqN, doc_antiq) = markup_string "doc_antiq" nameN; +val ML_antiquotationN = "ML antiquotation"; +val doc_antiquotationN = "document antiquotation"; +val doc_antiquotation_optionN = "document antiquotation option"; (* outer syntax *) diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/General/markup.scala Mon Jun 27 22:44:44 2011 +0200 @@ -189,8 +189,9 @@ val DOC_SOURCE = "doc_source" val ANTIQ = "antiq" - val ML_ANTIQ = "ML_antiq" - val DOC_ANTIQ = "doc_antiq" + val ML_ANTIQUOTATION = "ML antiquotation" + val DOCUMENT_ANTIQUOTATION = "document antiquotation" + val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option" /* ML syntax */ diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/General/name_space.ML Mon Jun 27 22:44:44 2011 +0200 @@ -50,7 +50,7 @@ val declare: Proof.context -> bool -> naming -> binding -> T -> string * T val alias: naming -> binding -> string -> T -> T type 'a table = T * 'a Symtab.table - val check: Proof.context -> 'a table -> xstring * Position.T -> string + val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a val get: 'a table -> string -> 'a val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table val empty_table: string -> 'a table @@ -383,15 +383,15 @@ -(** name spaces coupled with symbol tables **) +(** name space coupled with symbol table **) type 'a table = T * 'a Symtab.table; fun check ctxt (space, tab) (xname, pos) = let val name = intern space xname in - if Symtab.defined tab name - then (Context_Position.report ctxt pos (markup space name); name) - else error (undefined (kind_of space) name ^ Position.str_of pos) + (case Symtab.lookup tab name of + SOME x => (Context_Position.report ctxt pos (markup space name); (name, x)) + | NONE => error (undefined (kind_of space) name ^ Position.str_of pos)) end; fun get (space, tab) name = diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Mon Jun 27 22:44:44 2011 +0200 @@ -303,8 +303,12 @@ Proof.goal (Toplevel.proof_of (diag_state ())) handle Toplevel.UNDEF => error "No goal present"; -val _ = ML_Antiquote.value "Isar.state" (Scan.succeed "Isar_Cmd.diag_state ()"); -val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()"); +val _ = + Context.>> (Context.map_theory + (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state")) + (Scan.succeed "Isar_Cmd.diag_state ()") #> + ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal")) + (Scan.succeed "Isar_Cmd.diag_goal ()"))); (* present draft files *) @@ -380,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 023a1d1f97bd -r c3e4d280bdeb src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/ML/ml_antiquote.ML Mon Jun 27 22:44:44 2011 +0200 @@ -6,11 +6,11 @@ signature ML_ANTIQUOTE = sig - val macro: string -> Proof.context context_parser -> unit val variant: string -> Proof.context -> string * Proof.context - val inline: string -> string context_parser -> unit - val declaration: string -> string -> string context_parser -> unit - val value: string -> string context_parser -> unit + val macro: binding -> Proof.context context_parser -> theory -> theory + val inline: binding -> string context_parser -> theory -> theory + val declaration: string -> binding -> string context_parser -> theory -> theory + val value: binding -> string context_parser -> theory -> theory end; structure ML_Antiquote: ML_ANTIQUOTE = @@ -46,7 +46,8 @@ fun declaration kind name scan = ML_Context.add_antiq name (fn _ => scan >> (fn s => fn background => let - val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background; + val (a, background') = + variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) background; val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n"; val body = "Isabelle." ^ a; in (K (env, body), background') end)); @@ -57,48 +58,55 @@ (** misc antiquotations **) -val _ = inline "assert" - (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")"); +val _ = Context.>> (Context.map_theory + + (inline (Binding.name "assert") + (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> -val _ = inline "make_string" (Scan.succeed ml_make_string); + inline (Binding.name "make_string") (Scan.succeed ml_make_string) #> -val _ = value "binding" - (Scan.lift (Parse.position Args.name) - >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))); + value (Binding.name "binding") + (Scan.lift (Parse.position Args.name) + >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))) #> -val _ = value "theory" - (Scan.lift Args.name >> (fn name => - "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name) - || Scan.succeed "ML_Context.the_global_context ()"); + value (Binding.name "theory") + (Scan.lift Args.name >> (fn name => + "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name) + || Scan.succeed "ML_Context.the_global_context ()") #> -val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()"); + value (Binding.name "context") (Scan.succeed "ML_Context.the_local_context ()") #> -val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); -val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); -val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); + inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> + inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> + inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> -val _ = macro "let" (Args.context -- - Scan.lift - (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source))) - >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))); + macro (Binding.name "let") + (Args.context -- + Scan.lift + (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source))) + >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))) #> -val _ = macro "note" (Args.context :|-- (fn ctxt => - Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) => - ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])]))) - >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))); + macro (Binding.name "note") + (Args.context :|-- (fn ctxt => + Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms + >> (fn ((a, srcs), ths) => + ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])]))) + >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #> -val _ = value "ctyp" (Args.typ >> (fn T => - "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))); + value (Binding.name "ctyp") (Args.typ >> (fn T => + "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> -val _ = value "cterm" (Args.term >> (fn t => - "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); + value (Binding.name "cterm") (Args.term >> (fn t => + "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> -val _ = value "cprop" (Args.prop >> (fn t => - "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); + value (Binding.name "cprop") (Args.prop >> (fn t => + "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> -val _ = value "cpat" - (Args.context -- Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t => - "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); + value (Binding.name "cpat") + (Args.context -- + Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t => + "Thm.cterm_of (ML_Context.the_global_context ()) " ^ + ML_Syntax.atomic (ML_Syntax.print_term t))))); (* type classes *) @@ -108,11 +116,13 @@ |> syn ? Lexicon.mark_class |> ML_Syntax.print_string); -val _ = inline "class" (class false); -val _ = inline "class_syntax" (class true); +val _ = Context.>> (Context.map_theory + (inline (Binding.name "class") (class false) #> + inline (Binding.name "class_syntax") (class true) #> -val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => - ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))); + inline (Binding.name "sort") + (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => + ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))))); (* type constructors *) @@ -128,10 +138,15 @@ | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos)); in ML_Syntax.print_string res end); -val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c)); -val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)); -val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)); -val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Lexicon.mark_type c)); +val _ = Context.>> (Context.map_theory + (inline (Binding.name "type_name") + (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> + inline (Binding.name "type_abbrev") + (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> + inline (Binding.name "nonterminal") + (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> + inline (Binding.name "type_syntax") + (type_name "type" (fn (c, _) => Lexicon.mark_type c)))); (* constants *) @@ -144,25 +159,28 @@ handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos); in ML_Syntax.print_string res end); -val _ = inline "const_name" (const_name (fn (consts, c) => (Consts.the_type consts c; c))); -val _ = inline "const_abbrev" (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))); -val _ = inline "const_syntax" (const_name (fn (_, c) => Lexicon.mark_const c)); - +val _ = Context.>> (Context.map_theory + (inline (Binding.name "const_name") + (const_name (fn (consts, c) => (Consts.the_type consts c; c))) #> + inline (Binding.name "const_abbrev") + (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> + inline (Binding.name "const_syntax") + (const_name (fn (_, c) => Lexicon.mark_const c)) #> -val _ = inline "syntax_const" - (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) => - if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) - then ML_Syntax.print_string c - else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))); + inline (Binding.name "syntax_const") + (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) => + if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) + then ML_Syntax.print_string c + else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))) #> -val _ = inline "const" - (Args.context -- Scan.lift Args.name_source -- Scan.optional - (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] - >> (fn ((ctxt, raw_c), Ts) => - let - val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c; - val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts)); - in ML_Syntax.atomic (ML_Syntax.print_term const) end)); + inline (Binding.name "const") + (Args.context -- Scan.lift Args.name_source -- Scan.optional + (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] + >> (fn ((ctxt, raw_c), Ts) => + let + val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c; + val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts)); + in ML_Syntax.atomic (ML_Syntax.print_term const) end)))); end; diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/ML/ml_context.ML Mon Jun 27 22:44:44 2011 +0200 @@ -24,7 +24,9 @@ val ml_store_thms: string * thm list -> unit val ml_store_thm: string * thm -> unit type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context - val add_antiq: string -> (Position.T -> antiq context_parser) -> unit + val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory + val intern_antiq: theory -> xstring -> string + val defined_antiq: theory -> string -> bool val trace_raw: Config.raw val trace: bool Config.T val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T -> @@ -99,29 +101,28 @@ type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context; -local - -val global_parsers = - Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table); +structure Antiq_Parsers = Theory_Data +( + type T = (Position.T -> antiq context_parser) Name_Space.table; + val empty : T = Name_Space.empty_table Markup.ML_antiquotationN; + val extend = I; + fun merge data : T = Name_Space.merge_tables data; +); -in +fun add_antiq name scan thy = thy + |> Antiq_Parsers.map + (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy) + (name, scan) #> snd); -fun add_antiq name scan = CRITICAL (fn () => - Unsynchronized.change global_parsers (fn tab => - (if not (Symtab.defined tab name) then () - else warning ("Redefined ML antiquotation: " ^ quote name); - Symtab.update (name, scan) tab))); +val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get; +val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get; fun antiquotation src ctxt = - let val ((name, _), pos) = Args.dest_src src in - (case Symtab.lookup (! global_parsers) name of - NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) - | SOME scan => - (Context_Position.report ctxt pos (Markup.ML_antiq name); - Args.context_syntax "ML antiquotation" (scan pos) src ctxt)) - end; - -end; + let + val thy = Proof_Context.theory_of ctxt; + val ((xname, _), pos) = Args.dest_src src; + val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos); + in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end; (* parsing and evaluation *) diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/ML/ml_thms.ML Mon Jun 27 22:44:44 2011 +0200 @@ -33,7 +33,7 @@ (* fact references *) -fun thm_antiq kind scan = ML_Context.add_antiq kind +fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind) (fn _ => scan >> (fn ths => fn background => let val i = serial (); @@ -42,8 +42,10 @@ val ml = (thm_bind kind a i, "Isabelle." ^ a); in (K ml, background') end)); -val _ = thm_antiq "thm" (Attrib.thm >> single); -val _ = thm_antiq "thms" Attrib.thms; +val _ = + Context.>> (Context.map_theory + (thm_antiq "thm" (Attrib.thm >> single) #> + thm_antiq "thms" Attrib.thms)); (* ad-hoc goals *) @@ -52,25 +54,27 @@ val by = Args.$$$ "by"; val goal = Scan.unless (by || and_) Args.name; -val _ = ML_Context.add_antiq "lemma" - (fn _ => Args.context -- Args.mode "open" -- - Scan.lift (Parse.and_list1 (Scan.repeat1 goal) -- - (by |-- Method.parse -- Scan.option Method.parse)) >> - (fn ((ctxt, is_open), (raw_propss, methods)) => fn background => - let - val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; - val i = serial (); - val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation; - fun after_qed res goal_ctxt = - put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt; - val ctxt' = ctxt - |> Proof.theorem NONE after_qed propss - |> Proof.global_terminal_proof methods; - val (a, background') = background - |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i); - val ml = - (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a); - in (K ml, background') end)); +val _ = + Context.>> (Context.map_theory + (ML_Context.add_antiq (Binding.name "lemma") + (fn _ => Args.context -- Args.mode "open" -- + Scan.lift (Parse.and_list1 (Scan.repeat1 goal) -- + (by |-- Method.parse -- Scan.option Method.parse)) >> + (fn ((ctxt, is_open), (raw_propss, methods)) => fn background => + let + val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; + val i = serial (); + val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation; + fun after_qed res goal_ctxt = + put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt; + val ctxt' = ctxt + |> Proof.theorem NONE after_qed propss + |> Proof.global_terminal_proof methods; + val (a, background') = background + |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i); + val ml = + (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a); + in (K ml, background') end)))); end; diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jun 27 22:44:44 2011 +0200 @@ -41,7 +41,7 @@ if null ts then Markup.no_output else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P") else if name = Markup.sendbackN then (special "W", special "X") - else if name = Markup.bindingN then (special "F", special "A") + else if name = Markup.bindingN then (special "B", special "A") else if name = Markup.hiliteN then (special "0", special "1") else if name = Markup.tfreeN then (special "C", special "A") else if name = Markup.tvarN then (special "D", special "A") diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Mon Jun 27 22:44:44 2011 +0200 @@ -369,8 +369,8 @@ fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt; fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt); -fun read_terms ctxt = map (parse_term ctxt) #> check_terms ctxt; -fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt; +fun read_terms ctxt = Par_List.map_name "Syntax.read_terms" (parse_term ctxt) #> check_terms ctxt; +fun read_props ctxt = Par_List.map_name "Syntax.read_props" (parse_prop ctxt) #> check_props ctxt; val read_term = singleton o read_terms; val read_prop = singleton o read_props; diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/Thy/rail.ML --- a/src/Pure/Thy/rail.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/Thy/rail.ML Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/Thy/thy_output.ML Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb src/Pure/drule.ML --- a/src/Pure/drule.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/drule.ML Mon Jun 27 22:44:44 2011 +0200 @@ -313,7 +313,7 @@ case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of [] => (fth, fn i => fn x => x) (*No vars: nothing to do!*) | vars => - let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix)) + let fun newName (Var(ix,_)) = (ix, legacy_gensym (string_of_indexname ix)) val alist = map newName vars fun mk_inst (Var(v,T)) = (cterm_of thy (Var(v,T)), diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/library.ML --- a/src/Pure/library.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/library.ML Mon Jun 27 22:44:44 2011 +0200 @@ -211,7 +211,7 @@ 'a -> 'b -> 'c * 'b val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list - val gensym: string -> string + val legacy_gensym: string -> string type stamp = unit Unsynchronized.ref val stamp: unit -> stamp type serial = int @@ -1043,9 +1043,8 @@ -(* generating identifiers *) +(* generating identifiers -- often fresh *) -(** Freshly generated identifiers; supplied prefix MUST start with a letter **) local (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*) fun gensym_char i = @@ -1059,8 +1058,8 @@ val gensym_seed = Unsynchronized.ref (0: int); in - fun gensym pre = - pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed)); + fun legacy_gensym pre = + pre ^ newid (NAMED_CRITICAL "legacy_gensym" (fn () => Unsynchronized.inc gensym_seed)); end; diff -r 023a1d1f97bd -r c3e4d280bdeb src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Pure/simplifier.ML Mon Jun 27 22:44:44 2011 +0200 @@ -139,8 +139,9 @@ fun map_simpset f = Context.proof_map (map_ss f); fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt)); -val _ = ML_Antiquote.value "simpset" - (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())"); +val _ = Context.>> (Context.map_theory + (ML_Antiquote.value (Binding.name "simpset") + (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())"))); (* global simpset *) @@ -158,15 +159,16 @@ (* get simprocs *) -fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt); +fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt) #> #1; val the_simproc = Name_Space.get o get_simprocs; val _ = - ML_Antiquote.value "simproc" - (Args.context -- Scan.lift (Parse.position Args.name) - >> (fn (ctxt, name) => - "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^ - ML_Syntax.print_string (check_simproc ctxt name))); + Context.>> (Context.map_theory + (ML_Antiquote.value (Binding.name "simproc") + (Args.context -- Scan.lift (Parse.position Args.name) + >> (fn (ctxt, name) => + "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^ + ML_Syntax.print_string (check_simproc ctxt name))))); (* define simprocs *) diff -r 023a1d1f97bd -r c3e4d280bdeb src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Tools/Code/code_runtime.ML Mon Jun 27 22:44:44 2011 +0200 @@ -336,7 +336,9 @@ (** Isar setup **) -val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq); +val _ = + Context.>> (Context.map_theory + (ML_Context.add_antiq (Binding.name "code") (fn _ => Args.term >> ml_code_antiq))); local diff -r 023a1d1f97bd -r c3e4d280bdeb src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Tools/Code/code_target.ML Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Tools/Code_Generator.thy Mon Jun 27 22:44:44 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 023a1d1f97bd -r c3e4d280bdeb src/Tools/jEdit/src/isabelle_markup.scala --- a/src/Tools/jEdit/src/isabelle_markup.scala Mon Jun 27 17:04:04 2011 +0200 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Mon Jun 27 22:44:44 2011 +0200 @@ -114,7 +114,10 @@ Map( Markup.CLASS -> get_color("red"), Markup.TYPE -> get_color("black"), - Markup.CONSTANT -> get_color("black")) + Markup.CONSTANT -> 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(