--- 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).
--- 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" ("\<alpha>")
--- 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
--- 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}).
--- 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
--- 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
--- 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
*}
--- 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{*
--- 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
--- /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
--- 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 *}
--- 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 *}
--- 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} *}
--- 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} *}
--- 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"];
--- /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:
--- 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}%
--- 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}%
--- 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}%
--- 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}%
--- 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
--- 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 *}
--- 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
--- 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%
--- 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 \<union> (B \<union> A) = B \<union> A"
--- 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
--- 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
--- 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;
--- 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;
--- 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*)
--- 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
--- 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
--- 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;
--- 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 =
--- 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 *)
--- 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 */
--- 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 =
--- 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
--- 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;
--- 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 *)
--- 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;
--- 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")
--- 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;
--- 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;
--- 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;
--- 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)),
--- 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;
--- 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 *)
--- 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
--- 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*)
--- 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
--- 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(