--- a/NEWS Fri Sep 03 22:57:21 2010 +0200
+++ b/NEWS Fri Sep 03 23:54:48 2010 +0200
@@ -30,6 +30,7 @@
ML (Config.T) Isar (attribute)
+ eta_contract eta_contract
show_question_marks show_question_marks
show_consts show_consts
--- a/doc-src/TutorialI/Sets/Examples.thy Fri Sep 03 22:57:21 2010 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy Fri Sep 03 23:54:48 2010 +0200
@@ -1,6 +1,6 @@
theory Examples imports Main Binomial begin
-ML "eta_contract := false"
+declare [[eta_contract = false]]
ML "Pretty.margin_default := 64"
text{*membership, intersection *}
--- a/src/CCL/ROOT.ML Fri Sep 03 22:57:21 2010 +0200
+++ b/src/CCL/ROOT.ML Fri Sep 03 23:54:48 2010 +0200
@@ -8,6 +8,4 @@
evaluation to weak head-normal form.
*)
-eta_contract := true;
-
use_thys ["Wfd", "Fix"];
--- a/src/CCL/Set.thy Fri Sep 03 22:57:21 2010 +0200
+++ b/src/CCL/Set.thy Fri Sep 03 23:54:48 2010 +0200
@@ -4,6 +4,8 @@
imports FOL
begin
+declare [[eta_contract]]
+
typedecl 'a set
arities set :: ("term") "term"
--- a/src/Pure/Isar/attrib.ML Fri Sep 03 22:57:21 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Sep 03 23:54:48 2010 +0200
@@ -395,6 +395,7 @@
(register_config Syntax.show_structs_value #>
register_config Syntax.show_question_marks_value #>
register_config Syntax.ambiguity_level_value #>
+ register_config Syntax.eta_contract_value #>
register_config Goal_Display.goals_limit_value #>
register_config Goal_Display.show_main_goal_value #>
register_config Goal_Display.show_consts_value #>
--- a/src/Pure/ProofGeneral/preferences.ML Fri Sep 03 22:57:21 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Fri Sep 03 23:54:48 2010 +0200
@@ -129,7 +129,7 @@
bool_pref Goal_Display.show_main_goal_default
"show-main-goal"
"Show main goal in proof state display",
- bool_pref Syntax.eta_contract
+ bool_pref Syntax.eta_contract_default
"eta-contract"
"Print terms eta-contracted"];
--- a/src/Pure/Syntax/printer.ML Fri Sep 03 22:57:21 2010 +0200
+++ b/src/Pure/Syntax/printer.ML Fri Sep 03 23:54:48 2010 +0200
@@ -172,7 +172,7 @@
fun ast_of tm =
(case strip_comb tm of
- (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' t)) (map ast_of ts)
+ (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
| ((c as Const ("_free", _)), Free (x, T) :: ts) =>
Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
| ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
--- a/src/Pure/Syntax/syn_trans.ML Fri Sep 03 22:57:21 2010 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Fri Sep 03 23:54:48 2010 +0200
@@ -6,7 +6,9 @@
signature SYN_TRANS0 =
sig
- val eta_contract: bool Unsynchronized.ref
+ val eta_contract_default: bool Unsynchronized.ref
+ val eta_contract_value: Config.value Config.T
+ val eta_contract: bool Config.T
val atomic_abs_tr': string * typ * term -> term * term
val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
@@ -49,7 +51,7 @@
signature SYN_TRANS =
sig
include SYN_TRANS1
- val abs_tr': term -> term
+ val abs_tr': Proof.context -> term -> term
val prop_tr': term -> term
val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
@@ -280,9 +282,12 @@
(*do (partial) eta-contraction before printing*)
-val eta_contract = Unsynchronized.ref true;
+val eta_contract_default = Unsynchronized.ref true;
+val eta_contract_value =
+ Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
+val eta_contract = Config.bool eta_contract_value;
-fun eta_contr tm =
+fun eta_contr ctxt tm =
let
fun is_aprop (Const ("_aprop", _)) = true
| is_aprop _ = false;
@@ -298,13 +303,13 @@
| t' => Abs (a, T, t'))
| eta_abs t = t;
in
- if ! eta_contract then eta_abs tm else tm
+ if Config.get ctxt eta_contract then eta_abs tm else tm
end;
-fun abs_tr' tm =
+fun abs_tr' ctxt tm =
uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
- (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
+ (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
fun atomic_abs_tr' (x, T, t) =
let val [xT] = Term.rename_wrt_term t [(x, T)]
--- a/src/Pure/Thy/thy_output.ML Fri Sep 03 22:57:21 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Sep 03 23:54:48 2010 +0200
@@ -451,7 +451,7 @@
val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
-val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean);
+val _ = add_option "eta_contract" (Config.put 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);
--- a/src/ZF/ZF.thy Fri Sep 03 22:57:21 2010 +0200
+++ b/src/ZF/ZF.thy Fri Sep 03 23:54:48 2010 +0200
@@ -10,7 +10,7 @@
uses "~~/src/Tools/misc_legacy.ML"
begin
-ML {* eta_contract := false *}
+declare [[eta_contract = false]]
typedecl i
arities i :: "term"