--- a/src/Pure/CPure.thy Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/CPure.thy Thu Mar 27 15:32:15 2008 +0100
@@ -8,6 +8,14 @@
imports Pure
begin
-setup -- {* Some syntax modifications, see ROOT.ML *}
+no_syntax
+ "_appl" :: "('b => 'a) => args => logic" ("(1_/(1'(_')))" [1000, 0] 1000)
+ "_appl" :: "('b => 'a) => args => aprop" ("(1_/(1'(_')))" [1000, 0] 1000)
+
+syntax
+ "" :: "'a => cargs" ("_")
+ "_cargs" :: "'a => cargs => cargs" ("_/ _" [1000, 1000] 1000)
+ "_applC" :: "('b => 'a) => cargs => logic" ("(1_/ _)" [1000, 1000] 999)
+ "_applC" :: "('b => 'a) => cargs => aprop" ("(1_/ _)" [1000, 1000] 999)
end
--- a/src/Pure/Isar/attrib.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/attrib.ML Thu Mar 27 15:32:15 2008 +0100
@@ -276,7 +276,7 @@
(* theory setup *)
-val _ = Context.add_setup
+val _ = Context.>>
(add_attributes
[("attribute", internal_att, "internal attribute"),
("tagged", tagged, "tagged theorem"),
@@ -379,7 +379,7 @@
(* theory setup *)
-val _ = Context.add_setup
+val _ = Context.>>
(register_config Unify.trace_bound_value #>
register_config Unify.search_bound_value #>
register_config Unify.trace_simp_value #>
--- a/src/Pure/Isar/calculation.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/calculation.ML Thu Mar 27 15:32:15 2008 +0100
@@ -92,7 +92,7 @@
val trans_att = Attrib.add_del_args trans_add trans_del;
val sym_att = Attrib.add_del_args sym_add sym_del;
-val _ = Context.add_setup
+val _ = Context.>>
(Attrib.add_attributes
[("trans", trans_att, "declaration of transitivity rule"),
("sym", sym_att, "declaration of symmetry rule"),
--- a/src/Pure/Isar/class.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/class.ML Thu Mar 27 15:32:15 2008 +0100
@@ -395,7 +395,7 @@
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
default_intro_classes_tac facts;
-val _ = Context.add_setup (Method.add_methods
+val _ = Context.>> (Method.add_methods
[("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
"back-chain introduction rules of classes"),
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
--- a/src/Pure/Isar/code.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/code.ML Thu Mar 27 15:32:15 2008 +0100
@@ -107,7 +107,7 @@
val code_attr = Attrib.syntax (Scan.peek (fn context =>
List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
in
- Context.add_setup (Attrib.add_attributes
+ Context.>> (Attrib.add_attributes
[("code", code_attr, "declare theorems for code generation")])
end;
@@ -387,7 +387,7 @@
in (exec, ref data) end;
);
-val _ = Context.add_setup CodeData.init;
+val _ = Context.>> CodeData.init;
fun thy_data f thy = f ((snd o CodeData.get) thy);
@@ -864,7 +864,7 @@
(remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
(*fully applied in order to get right context for mk_rew!*)
-val _ = Context.add_setup
+val _ = Context.>>
(let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
fun add_simple_attribute (name, f) =
--- a/src/Pure/Isar/context_rules.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/context_rules.ML Thu Mar 27 15:32:15 2008 +0100
@@ -198,7 +198,7 @@
val elim_query = rule_add elim_queryK I;
val dest_query = rule_add elim_queryK Tactic.make_elim;
-val _ = Context.add_setup
+val _ = Context.>>
(snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
@@ -215,6 +215,6 @@
("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
"remove declaration of intro/elim/dest rule")];
-val _ = Context.add_setup (Attrib.add_attributes rule_atts);
+val _ = Context.>> (Attrib.add_attributes rule_atts);
end;
--- a/src/Pure/Isar/isar_cmd.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Thu Mar 27 15:32:15 2008 +0100
@@ -7,7 +7,7 @@
signature ISAR_CMD =
sig
- val generic_setup: (string * Position.T) option -> theory -> theory
+ val generic_setup: string * Position.T -> theory -> theory
val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
val parse_translation: bool * (string * Position.T) -> theory -> theory
val print_translation: bool * (string * Position.T) -> theory -> theory
@@ -134,10 +134,9 @@
(* generic_setup *)
-fun generic_setup NONE = (fn thy => thy |> Context.setup ())
- | generic_setup (SOME (txt, pos)) =
- ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt
- |> Context.theory_map;
+fun generic_setup (txt, pos) =
+ ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt
+ |> Context.theory_map;
(* translation functions *)
--- a/src/Pure/Isar/isar_syn.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML Thu Mar 27 15:32:15 2008 +0100
@@ -323,7 +323,7 @@
val _ =
OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
- (Scan.option (P.position P.text) >> (Toplevel.theory o IsarCmd.generic_setup));
+ (P.position P.text >> (Toplevel.theory o IsarCmd.generic_setup));
val _ =
OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
--- a/src/Pure/Isar/locale.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/locale.ML Thu Mar 27 15:32:15 2008 +0100
@@ -2000,7 +2000,7 @@
end;
-val _ = Context.add_setup
+val _ = Context.>>
(add_locale_i (SOME "") "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
snd #> ProofContext.theory_of #>
add_locale_i (SOME "") "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
@@ -2041,7 +2041,7 @@
Method.intros_tac (wits @ intros) facts st
end;
-val _ = Context.add_setup (Method.add_methods
+val _ = Context.>> (Method.add_methods
[("intro_locales",
Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
"back-chain introduction rules of locales without unfolding predicates"),
--- a/src/Pure/Isar/method.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/method.ML Thu Mar 27 15:32:15 2008 +0100
@@ -554,7 +554,7 @@
(* theory setup *)
-val _ = Context.add_setup (add_methods
+val _ = Context.>> (add_methods
[("fail", no_args fail, "force failure"),
("succeed", no_args succeed, "succeed"),
("-", no_args insert_facts, "do nothing (insert current facts only)"),
--- a/src/Pure/Isar/object_logic.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/object_logic.ML Thu Mar 27 15:32:15 2008 +0100
@@ -193,7 +193,7 @@
val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
-val _ = Context.add_setup (add_rulify Drule.norm_hhf_eq);
+val _ = Context.>> (add_rulify Drule.norm_hhf_eq);
(* atomize *)
--- a/src/Pure/Isar/proof_context.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Mar 27 15:32:15 2008 +0100
@@ -571,7 +571,7 @@
fun standard_term_uncheck ctxt =
map (contract_abbrevs ctxt);
-fun add eq what f = Context.add_setup
+fun add eq what f = Context.>>
(Context.theory_map (what (fn xs => fn ctxt =>
let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end)));
@@ -922,7 +922,7 @@
in
-val _ = Context.add_setup
+val _ = Context.>>
(Sign.add_syntax
[("_context_const", "id => 'a", Delimfix "CONST _"),
("_context_const", "longid => 'a", Delimfix "CONST _"),
--- a/src/Pure/Isar/rule_insts.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/rule_insts.ML Thu Mar 27 15:32:15 2008 +0100
@@ -218,7 +218,7 @@
(* setup *)
-val _ = Context.add_setup (Attrib.add_attributes
+val _ = Context.>> (Attrib.add_attributes
[("where", where_att, "named instantiation of theorem"),
("of", of_att, "positional instantiation of theorem")]);
@@ -367,7 +367,7 @@
(* setup *)
-val _ = Context.add_setup (Method.add_methods
+val _ = Context.>> (Method.add_methods
[("rule_tac", inst_args_var res_inst_meth,
"apply rule (dynamic instantiation)"),
("erule_tac", inst_args_var eres_inst_meth,
--- a/src/Pure/Isar/skip_proof.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/skip_proof.ML Thu Mar 27 15:32:15 2008 +0100
@@ -24,7 +24,7 @@
if ! quick_and_dirty then prop
else error "Proof may be skipped in quick_and_dirty mode only!";
-val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
+val _ = Context.>> (Theory.add_oracle ("skip_proof", skip_proof));
(* basic cheating *)
--- a/src/Pure/Proof/extraction.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Proof/extraction.ML Thu Mar 27 15:32:15 2008 +0100
@@ -395,7 +395,7 @@
(** Pure setup **)
-val _ = Context.add_setup
+val _ = Context.>>
(add_types [("prop", ([], NONE))] #>
add_typeof_eqns
--- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Mar 27 15:32:15 2008 +0100
@@ -187,7 +187,7 @@
in rew' end;
fun rprocs b = [("Pure/meta_equality", rew b)];
-val _ = Context.add_setup (fold Proofterm.add_prf_rproc (rprocs false));
+val _ = Context.>> (fold Proofterm.add_prf_rproc (rprocs false));
(**** apply rewriting function to all terms in proof ****)
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Mar 27 15:32:15 2008 +0100
@@ -92,7 +92,7 @@
in
-val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
+val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 27 15:32:15 2008 +0100
@@ -105,7 +105,7 @@
in
-val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
+val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
end;
--- a/src/Pure/Pure.thy Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Pure.thy Thu Mar 27 15:32:15 2008 +0100
@@ -2,10 +2,7 @@
ID: $Id$
*)
-section {* The Pure theory *}
-
-setup -- {* Common setup of internal components *}
-
+section {* Further content for the Pure theory *}
subsection {* Meta-level connectives in assumptions *}
--- a/src/Pure/Thy/html.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Thy/html.ML Thu Mar 27 15:32:15 2008 +0100
@@ -267,7 +267,7 @@
("var", var_or_skolem),
("xstr", style "xstr")];
-val _ = Context.add_setup (Sign.add_mode_tokentrfuns htmlN html_trans);
+val _ = Context.>> (Sign.add_mode_tokentrfuns htmlN html_trans);
--- a/src/Pure/Thy/term_style.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Thy/term_style.ML Thu Mar 27 15:32:15 2008 +0100
@@ -65,7 +65,7 @@
" in propositon: " ^ Syntax.string_of_term ctxt t)
end;
-val _ = Context.add_setup
+val _ = Context.>>
(add_style "lhs" (fst oo style_binargs) #>
add_style "rhs" (snd oo style_binargs) #>
add_style "prem1" (style_parm_premise 1) #>
--- a/src/Pure/Tools/isabelle_process.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.ML Thu Mar 27 15:32:15 2008 +0100
@@ -160,7 +160,7 @@
in
-val _ = Context.add_setup (Sign.add_tokentrfuns token_trans);
+val _ = Context.>> (Sign.add_tokentrfuns token_trans);
end;
--- a/src/Pure/assumption.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/assumption.ML Thu Mar 27 15:32:15 2008 +0100
@@ -78,7 +78,7 @@
(* named prems -- legacy feature *)
-val _ = Context.add_setup
+val _ = Context.>>
(PureThy.add_thms_dynamic ("prems",
fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt));
--- a/src/Pure/codegen.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/codegen.ML Thu Mar 27 15:32:15 2008 +0100
@@ -339,7 +339,7 @@
end)
in add_preprocessor prep end;
-val _ = Context.add_setup
+val _ = Context.>>
(let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
in
@@ -786,7 +786,7 @@
(add_edge (node_id, dep) gr'', p module''))
end);
-val _ = Context.add_setup
+val _ = Context.>>
(add_codegen "default" default_codegen #>
add_tycodegen "default" default_tycodegen);
@@ -1026,7 +1026,7 @@
else state
end;
-val _ = Context.add_setup
+val _ = Context.>>
(Context.theory_map (Specification.add_theorem_hook test_goal'));
@@ -1078,7 +1078,7 @@
let val {thy, t, ...} = rep_cterm ct
in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
-val _ = Context.add_setup
+val _ = Context.>>
(Theory.add_oracle ("evaluation", evaluation_oracle));
--- a/src/Pure/context.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/context.ML Thu Mar 27 15:32:15 2008 +0100
@@ -68,9 +68,6 @@
val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
val >> : (theory -> theory) -> unit
val >>> : (theory -> 'a * theory) -> 'a
- (*delayed setup*)
- val add_setup: (theory -> theory) -> unit
- val setup: unit -> theory -> theory
end;
signature PRIVATE_CONTEXT =
@@ -537,17 +534,6 @@
val _ = set_thread_data (SOME (Theory pre_pure_thy));
-
-
-(** delayed theory setup **)
-
-local
- val setup_fn = ref (I: theory -> theory);
-in
- fun add_setup f = CRITICAL (fn () => setup_fn := (! setup_fn #> f));
- fun setup () = CRITICAL (fn () => let val f = ! setup_fn in setup_fn := I; f end);
-end;
-
end;
structure BasicContext: BASIC_CONTEXT = Context;
--- a/src/Pure/pure_setup.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/pure_setup.ML Thu Mar 27 15:32:15 2008 +0100
@@ -22,9 +22,6 @@
Context.set_thread_data NONE;
ThyInfo.register_theory Pure.thy;
-Context.add_setup
- (Sign.del_modesyntax_i Syntax.mode_default PureThy.appl_syntax #>
- Sign.add_syntax_i PureThy.applC_syntax);
use_thy "CPure";
structure CPure = struct val thy = theory "CPure" end;
--- a/src/Pure/simplifier.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/simplifier.ML Thu Mar 27 15:32:15 2008 +0100
@@ -105,7 +105,7 @@
fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
);
-val _ = Context.add_setup GlobalSimpset.init;
+val _ = Context.>> GlobalSimpset.init;
fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
val get_simpset = ! o GlobalSimpset.get;
@@ -369,7 +369,7 @@
(* setup attributes *)
-val _ = Context.add_setup
+val _ = Context.>>
(Attrib.add_attributes
[(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
(congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),