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