--- a/src/HOL/Bali/Conform.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/Bali/Conform.thy Sun Jan 15 20:03:59 2012 +0100
@@ -370,8 +370,7 @@
apply (drule_tac var_tys_Some_eq [THEN iffD1])
defer
apply (subst obj_ty_cong)
-apply(auto dest!: fields_table_SomeD obj_ty_CInst1 obj_ty_Arr1
- split add: sum.split_asm obj_tag.split_asm)
+apply (auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
done
section "state conformance"
@@ -430,7 +429,7 @@
lemma conforms_error_if [iff]:
"((error_if c err x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
-by (auto simp: abrupt_if_def split: split_if)
+by (auto simp: abrupt_if_def)
lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
by (auto simp: conforms_def Let_def)
--- a/src/HOL/Bali/DefiniteAssignment.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy Sun Jan 15 20:03:59 2012 +0100
@@ -1037,11 +1037,10 @@
lemma rmlab_other_label [simp]: "l\<noteq>l'\<Longrightarrow> (rmlab l A) l' = A l'"
by (auto simp add: rmlab_def)
-lemma range_inter_ts_subseteq [intro]: "\<forall> k. A k \<subseteq> B k \<Longrightarrow> \<Rightarrow>\<Inter>A \<subseteq> \<Rightarrow>\<Inter>B"
+lemma range_inter_ts_subseteq [intro]: "\<forall> k. A k \<subseteq> B k \<Longrightarrow> \<Rightarrow>\<Inter>A \<subseteq> \<Rightarrow>\<Inter>B"
by (auto simp add: range_inter_ts_def)
-lemma range_inter_ts_subseteq':
- "\<lbrakk>\<forall> k. A k \<subseteq> B k; x \<in> \<Rightarrow>\<Inter>A\<rbrakk> \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>B"
+lemma range_inter_ts_subseteq': "\<forall> k. A k \<subseteq> B k \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>A \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>B"
by (auto simp add: range_inter_ts_def)
lemma da_monotone:
@@ -1072,7 +1071,7 @@
where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
and A': "nrm A' = nrm C' \<inter> brk C' l" "brk A' = rmlab l (brk C')"
using Lab.prems
- by - (erule da_elim_cases,simp)
+ by cases simp
ultimately
have "nrm C \<subseteq> nrm C'" and hyp_brk: "(\<forall>l. brk C l \<subseteq> brk C' l)" by auto
then
@@ -1095,7 +1094,7 @@
where da_c1: "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
da_c2: "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'"
- by (rule da_elim_cases) auto
+ by cases auto
note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
moreover note `B \<subseteq> B'`
moreover note da_c1
@@ -1116,7 +1115,7 @@
where da_c1: "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
da_c2: "Env\<turnstile> B' \<union> assigns_if False e \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C1' \<inter> nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'"
- by (rule da_elim_cases) auto
+ by cases auto
note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1`
moreover note B' = `B \<subseteq> B'`
moreover note da_c1
@@ -1138,7 +1137,7 @@
da_c': "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
A': "nrm A' = nrm C' \<inter> (B' \<union> assigns_if False e)"
"brk A' = brk C'"
- by (rule da_elim_cases) auto
+ by cases auto
note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C`
moreover note B' = `B \<subseteq> B'`
moreover note da_c'
@@ -1168,7 +1167,7 @@
case (Jmp jump B A Env B' A')
thus ?case by (elim da_elim_cases) (auto split: jump.splits)
next
- case Throw thus ?case by - (erule da_elim_cases, auto)
+ case Throw thus ?case by (elim da_elim_cases) auto
next
case (Try Env B c1 C1 vn C c2 C2 A B' A')
note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter> brk C2`
@@ -1179,7 +1178,7 @@
\<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C1' \<inter> nrm C2'"
"brk A' = brk C1' \<Rightarrow>\<inter> brk C2'"
- by (rule da_elim_cases) auto
+ by cases auto
note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
moreover note B' = `B \<subseteq> B'`
moreover note da_c1'
@@ -1203,7 +1202,7 @@
da_c2': "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C1' \<union> nrm C2'"
"brk A' = (brk C1' \<Rightarrow>\<union>\<^sub>\<forall> nrm C2') \<Rightarrow>\<inter> (brk C2')"
- by (rule da_elim_cases) auto
+ by cases auto
note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
moreover note B' = `B \<subseteq> B'`
moreover note da_c1'
@@ -1217,19 +1216,19 @@
show ?case
by auto
next
- case Init thus ?case by - (erule da_elim_cases, auto)
+ case Init thus ?case by (elim da_elim_cases) auto
next
- case NewC thus ?case by - (erule da_elim_cases, auto)
+ case NewC thus ?case by (elim da_elim_cases) auto
next
- case NewA thus ?case by - (erule da_elim_cases, auto)
+ case NewA thus ?case by (elim da_elim_cases) auto
next
- case Cast thus ?case by - (erule da_elim_cases, auto)
+ case Cast thus ?case by (elim da_elim_cases) auto
next
- case Inst thus ?case by - (erule da_elim_cases, auto)
+ case Inst thus ?case by (elim da_elim_cases) auto
next
- case Lit thus ?case by - (erule da_elim_cases, auto)
+ case Lit thus ?case by (elim da_elim_cases) auto
next
- case UnOp thus ?case by - (erule da_elim_cases, auto)
+ case UnOp thus ?case by (elim da_elim_cases) auto
next
case (CondAnd Env B e1 E1 e2 E2 A B' A')
note A = `nrm A = B \<union>
@@ -1241,24 +1240,24 @@
assigns_if True (BinOp CondAnd e1 e2) \<inter>
assigns_if False (BinOp CondAnd e1 e2)"
"brk A' = (\<lambda>l. UNIV)"
- by (rule da_elim_cases) auto
+ by cases auto
note B' = `B \<subseteq> B'`
with A A' show ?case
by auto
next
- case CondOr thus ?case by - (erule da_elim_cases, auto)
+ case CondOr thus ?case by (elim da_elim_cases) auto
next
- case BinOp thus ?case by - (erule da_elim_cases, auto)
+ case BinOp thus ?case by (elim da_elim_cases) auto
next
- case Super thus ?case by - (erule da_elim_cases, auto)
+ case Super thus ?case by (elim da_elim_cases) auto
next
- case AccLVar thus ?case by - (erule da_elim_cases, auto)
+ case AccLVar thus ?case by (elim da_elim_cases) auto
next
- case Acc thus ?case by - (erule da_elim_cases, auto)
+ case Acc thus ?case by (elim da_elim_cases) auto
next
- case AssLVar thus ?case by - (erule da_elim_cases, auto)
+ case AssLVar thus ?case by (elim da_elim_cases) auto
next
- case Ass thus ?case by - (erule da_elim_cases, auto)
+ case Ass thus ?case by (elim da_elim_cases) auto
next
case (CondBool Env c e1 e2 B C E1 E2 A B' A')
note A = `nrm A = B \<union>
@@ -1273,7 +1272,7 @@
assigns_if True (c ? e1 : e2) \<inter>
assigns_if False (c ? e1 : e2)"
"brk A' = (\<lambda>l. UNIV)"
- by - (erule da_elim_cases,auto simp add: inj_term_simps)
+ by (elim da_elim_cases) (auto simp add: inj_term_simps)
(* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
note B' = `B \<subseteq> B'`
with A A' show ?case
@@ -1289,7 +1288,7 @@
A': "nrm A' = nrm E1' \<inter> nrm E2'"
"brk A' = (\<lambda>l. UNIV)"
using not_bool
- by - (erule da_elim_cases, auto simp add: inj_term_simps)
+ by (elim da_elim_cases) (auto simp add: inj_term_simps)
(* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
note `PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1`
moreover note B' = `B \<subseteq> B'`
@@ -1308,19 +1307,19 @@
from Call.prems and Call.hyps
show ?case by cases auto
next
- case Methd thus ?case by - (erule da_elim_cases, auto)
+ case Methd thus ?case by (elim da_elim_cases) auto
next
- case Body thus ?case by - (erule da_elim_cases, auto)
+ case Body thus ?case by (elim da_elim_cases) auto
next
- case LVar thus ?case by - (erule da_elim_cases, auto)
+ case LVar thus ?case by (elim da_elim_cases) auto
next
- case FVar thus ?case by - (erule da_elim_cases, auto)
+ case FVar thus ?case by (elim da_elim_cases) auto
next
- case AVar thus ?case by - (erule da_elim_cases, auto)
+ case AVar thus ?case by (elim da_elim_cases) auto
next
- case Nil thus ?case by - (erule da_elim_cases, auto)
+ case Nil thus ?case by (elim da_elim_cases) auto
next
- case Cons thus ?case by - (erule da_elim_cases, auto)
+ case Cons thus ?case by (elim da_elim_cases) auto
qed
qed (rule da', rule `B \<subseteq> B'`)
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Sun Jan 15 20:03:59 2012 +0100
@@ -294,8 +294,7 @@
}
ultimately show ?thesis using Getfield field "class" stk hconf wf
apply clarsimp
- apply (fastforce intro: wf_prog_ws_prog
- dest!: hconfD widen_cfs_fields oconf_objD)
+ apply (fastforce dest!: hconfD widen_cfs_fields oconf_objD)
done
next
case (Putfield F C)
--- a/src/HOL/MicroJava/BV/JVM.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Sun Jan 15 20:03:59 2012 +0100
@@ -112,11 +112,11 @@
from phi' have l: "size phi' = size bs" by simp
with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp
with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
- by (clarsimp simp add: not_Err_eq)
+ by auto
from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
also from w have "phi' = map OK (map ok_val phi')"
- by (auto simp add: wt_step_def not_Err_eq intro!: nth_equalityI)
+ by (auto simp add: wt_step_def intro!: nth_equalityI)
finally
have check_types:
"check_types G maxs maxr (map OK (map ok_val phi'))" .
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Sun Jan 15 20:03:59 2012 +0100
@@ -71,7 +71,7 @@
apply (simp add: eff_def xcpt_eff_def norm_eff_def)
apply (case_tac "bs!p")
- apply (clarsimp simp add: not_Err_eq)
+ apply clarsimp
apply (drule listE_nth_in, assumption)
apply fastforce
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Sun Jan 15 20:03:59 2012 +0100
@@ -474,14 +474,13 @@
(* to avoid automatic pair splits *)
declare split_paired_All [simp del] split_paired_Ex [simp del]
-declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C;
method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow>
distinct (gjmb_plns (gmb G C S))"
apply (frule method_wf_mdecl [THEN conjunct2], assumption, assumption)
apply (case_tac S)
-apply (simp add: wf_mdecl_def wf_java_mdecl_def galldefs distinct_append)
+apply (simp add: wf_mdecl_def wf_java_mdecl_def galldefs)
apply (simp add: unique_def map_of_in_set)
apply blast
done
@@ -809,7 +808,7 @@
(* case LAss *)
apply (intro allI impI)
apply (frule wtpd_expr_lass, erule conjE, erule conjE)
-apply (simp add: compExpr_compExprs.simps)
+apply simp
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
apply blast
@@ -884,7 +883,7 @@
apply simp
(* case Nil *)
-apply (simp add: compExpr_compExprs.simps)
+apply simp
apply (intro strip)
apply (rule progression_refl)
@@ -1261,7 +1260,6 @@
(* reinstall pair splits *)
declare split_paired_All [simp] split_paired_Ex [simp]
-declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
declare wf_prog_ws_prog [simp del]
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Sun Jan 15 20:03:59 2012 +0100
@@ -955,20 +955,20 @@
apply simp
apply (simp (no_asm_simp))+
apply simp
-apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp))
+apply (simp add: max_ssize_def) apply (simp (no_asm_simp))
(* show check_type \<dots> *)
apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
apply (simp only:)
apply (rule check_type_mono) apply assumption
-apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append max_ac)
+apply (simp (no_asm_simp) add: max_ssize_def max_ac)
apply (simp add: nth_append)
apply (erule conjE)+
apply (case_tac sttp1)
apply (simp add: check_type_def)
apply (rule states_lower, assumption)
-apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append)
+apply (simp (no_asm_simp) add: max_ssize_def)
apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def)
apply (simp (no_asm_simp))+
done
@@ -1742,7 +1742,7 @@
and ?f3.0 = "popST (Suc 0) \<box> pushST [PrimT Boolean]"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
- apply (simp add: compTpExpr_LT_ST_rewr popST_def)
+ apply simp
apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp))
apply (simp (no_asm_simp) add: length_compTpExpr)
apply (simp (no_asm_simp))
@@ -1775,7 +1775,7 @@
and ?f3.0 = "comb_nil"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
- apply (simp add: compTpExpr_LT_ST_rewr popST_def)
+ apply simp
apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp))
apply (simp (no_asm_simp) add: length_compTpExpr)
apply (simp (no_asm_simp) add: start_sttp_resp_def)
--- a/src/HOL/MicroJava/Comp/Index.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy Sun Jan 15 20:03:59 2012 +0100
@@ -35,7 +35,7 @@
apply (subgoal_tac "vn \<noteq> This")
apply simp
apply (subgoal_tac "\<forall> x \<in> set pns. (\<lambda>z. z \<noteq> vn) x")
-apply (simp add: takeWhile_append2)
+apply simp
apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars)) < length (map fst lvars)")
apply simp
apply (rule length_takeWhile)
@@ -86,7 +86,7 @@
\<Longrightarrow> index (pns, zs @ ((xvar, xval) # xys), blk, res) xvar = Suc (length pns + length zs)"
apply (simp add: index_def)
apply (subgoal_tac "(\<And>x. ((x \<in> (set pns)) \<Longrightarrow> ((\<lambda>z. (z \<noteq> xvar))x)))")
-apply (simp add: List.takeWhile_append2)
+apply simp
apply (subgoal_tac "(takeWhile (\<lambda>z. z \<noteq> xvar) (map fst zs @ xvar # map fst xys)) = map fst zs @ (takeWhile (\<lambda>z. z \<noteq> xvar) (xvar # map fst xys))")
apply simp
apply (rule List.takeWhile_append2)
@@ -114,7 +114,7 @@
disjoint_varnames pns (lvars_pre @ (vn, ty) # lvars_post)
\<Longrightarrow> index (pns, lvars_pre @ (vn, ty) # lvars_post, blk, res) vn =
Suc (length pns + length lvars_pre)"
-apply (simp add: disjoint_varnames_def index_def unique_def distinct_append)
+apply (simp add: disjoint_varnames_def index_def unique_def)
apply (subgoal_tac "vn \<noteq> This", simp)
apply (subgoal_tac
"takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars_pre @ vn # map fst lvars_post) =
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Sun Jan 15 20:03:59 2012 +0100
@@ -95,7 +95,7 @@
"(class G C = None) = (class (comp G) C = None)"
apply (simp add: class_def comp_def compClass_def)
apply (simp add: map_of_in_set)
-apply (simp add: image_compose [THEN sym] o_def split_beta del: image_compose)
+apply (simp add: image_compose [THEN sym] o_def split_beta)
done
lemma comp_is_class: "is_class (comp G) C = is_class G C"
@@ -170,7 +170,7 @@
apply (simp only: image_compose [THEN sym])
apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
(C, cno, fdls, map (compMethod G C) jmdls))) = fst")
-apply (simp del: image_compose)
+apply simp
apply (simp add: fun_eq_iff split_beta)
done
@@ -275,9 +275,9 @@
= Option.map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
apply (induct xs)
apply simp
-apply (simp del: split_paired_All)
+apply simp
apply (case_tac "k = fst a")
-apply (simp del: split_paired_All)
+apply simp
apply (subgoal_tac "(inv f (fst a, snd (f a))) = a", simp)
apply (subgoal_tac "(fst a, snd (f a)) = f a", simp)
apply (erule conjE)+
@@ -332,7 +332,7 @@
defer
apply (intro strip)
-apply (simp add: map_add_Some_iff map_of_map del: split_paired_Ex)
+apply (simp add: map_add_Some_iff map_of_map)
apply (simp add: map_add_def)
apply (subgoal_tac "inj (\<lambda>(s, m). (s, Ca, m))")
apply (drule_tac g="(Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms
--- a/src/HOL/MicroJava/DFA/Kildall.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Sun Jan 15 20:03:59 2012 +0100
@@ -320,7 +320,7 @@
apply (rule sym, assumption)
defer apply simp
apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
- apply (blast intro!: psubsetI elim: equalityE)
+ apply (blast elim: equalityE)
apply clarsimp
apply (drule bspec, assumption)
apply (drule bspec, assumption)
--- a/src/HOL/MicroJava/DFA/Semilat.thy Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Sun Jan 15 20:03:59 2012 +0100
@@ -155,7 +155,7 @@
lemma (in Semilat) le_iff_plus_unchanged: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (x \<squnion>\<^sub>f y = y)"
(*<*)
apply (rule iffI)
- apply (blast intro: antisym_r refl_r lub ub2)
+ apply (blast intro: antisym_r lub ub2)
apply (erule subst)
apply simp
done
@@ -164,7 +164,7 @@
lemma (in Semilat) le_iff_plus_unchanged2: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (y \<squnion>\<^sub>f x = y)"
(*<*)
apply (rule iffI)
- apply (blast intro: order_antisym lub order_refl ub1)
+ apply (blast intro: order_antisym lub ub1)
apply (erule subst)
apply simp
done
--- a/src/HOL/Tools/record.ML Sun Jan 15 17:27:46 2012 +0100
+++ b/src/HOL/Tools/record.ML Sun Jan 15 20:03:59 2012 +0100
@@ -331,8 +331,8 @@
update_convs: thm list,
select_defs: thm list,
update_defs: thm list,
- fold_congs: thm list,
- unfold_congs: thm list,
+ fold_congs: thm list, (* FIXME unused!? *)
+ unfold_congs: thm list, (* FIXME unused!? *)
splits: thm list,
defs: thm list,
@@ -379,9 +379,7 @@
{selectors: (int * bool) Symtab.table,
updates: string Symtab.table,
simpset: simpset,
- defset: simpset,
- foldcong: simpset,
- unfoldcong: simpset},
+ defset: simpset},
equalities: thm Symtab.table,
extinjects: thm list,
extsplit: thm Symtab.table, (*maps extension name to split rule*)
@@ -401,16 +399,12 @@
val empty =
make_data Symtab.empty
{selectors = Symtab.empty, updates = Symtab.empty,
- simpset = HOL_basic_ss, defset = HOL_basic_ss,
- foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
+ simpset = HOL_basic_ss, defset = HOL_basic_ss}
Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
val extend = I;
fun merge
({records = recs1,
- sel_upd =
- {selectors = sels1, updates = upds1,
- simpset = ss1, defset = ds1,
- foldcong = fc1, unfoldcong = uc1},
+ sel_upd = {selectors = sels1, updates = upds1, simpset = ss1, defset = ds1},
equalities = equalities1,
extinjects = extinjects1,
extsplit = extsplit1,
@@ -418,10 +412,7 @@
extfields = extfields1,
fieldext = fieldext1},
{records = recs2,
- sel_upd =
- {selectors = sels2, updates = upds2,
- simpset = ss2, defset = ds2,
- foldcong = fc2, unfoldcong = uc2},
+ sel_upd = {selectors = sels2, updates = upds2, simpset = ss2, defset = ds2},
equalities = equalities2,
extinjects = extinjects2,
extsplit = extsplit2,
@@ -433,9 +424,7 @@
{selectors = Symtab.merge (K true) (sels1, sels2),
updates = Symtab.merge (K true) (upds1, upds2),
simpset = Simplifier.merge_ss (ss1, ss2),
- defset = Simplifier.merge_ss (ds1, ds2),
- foldcong = Simplifier.merge_ss (fc1, fc2),
- unfoldcong = Simplifier.merge_ss (uc1, uc2)}
+ defset = Simplifier.merge_ss (ds1, ds2)}
(Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
(Thm.merge_thms (extinjects1, extinjects2))
(Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
@@ -482,22 +471,21 @@
| NONE => NONE)
end;
-fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
+fun put_sel_upd names more depth simps defs thy =
let
val all = names @ [more];
val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
val upds = map (suffix updateN) all ~~ all;
- val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
+ val {records, sel_upd = {selectors, updates, simpset, defset},
equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
- val data = make_data records
- {selectors = fold Symtab.update_new sels selectors,
- updates = fold Symtab.update_new upds updates,
- simpset = simpset addsimps simps,
- defset = defset addsimps defs,
- foldcong = foldcong |> fold Simplifier.add_cong folds,
- unfoldcong = unfoldcong |> fold Simplifier.add_cong unfolds}
- equalities extinjects extsplit splits extfields fieldext;
+ val data =
+ make_data records
+ {selectors = fold Symtab.update_new sels selectors,
+ updates = fold Symtab.update_new upds updates,
+ simpset = simpset addsimps simps,
+ defset = defset addsimps defs}
+ equalities extinjects extsplit splits extfields fieldext;
in Data.put data thy end;
@@ -2214,7 +2202,7 @@
val final_thy =
thms_thy'
|> put_record name info
- |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
+ |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs
|> add_equalities extension_id equality'
|> add_extinjects ext_inject
|> add_extsplit extension_name ext_split
--- a/src/Pure/PIDE/protocol.scala Sun Jan 15 17:27:46 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Sun Jan 15 20:03:59 2012 +0100
@@ -43,6 +43,11 @@
/* command status */
+ object Status
+ {
+ val init = Status()
+ }
+
sealed case class Status(
private val finished: Boolean = false,
private val failed: Boolean = false,
@@ -52,6 +57,8 @@
def is_running: Boolean = forks != 0
def is_finished: Boolean = finished && forks == 0
def is_failed: Boolean = failed && forks == 0
+ def + (that: Status): Status =
+ Status(finished || that.finished, failed || that.failed, forks + that.forks)
}
val command_status_markup: Set[String] =
@@ -68,7 +75,7 @@
}
def command_status(markups: List[Markup]): Status =
- (Status() /: markups)(command_status(_, _))
+ (Status.init /: markups)(command_status(_, _))
/* node status */
--- a/src/Tools/jEdit/src/document_view.scala Sun Jan 15 17:27:46 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Sun Jan 15 20:03:59 2012 +0100
@@ -21,7 +21,6 @@
FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
import javax.swing.event.{CaretListener, CaretEvent}
-import javax.swing.text.Segment
import org.gjt.sp.util.Log
@@ -300,10 +299,9 @@
// gutter icons
Isabelle_Rendering.gutter_message(snapshot, line_range) match {
case Some(icon) =>
- val icn = icon.icon
- val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
- val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
- icn.paintIcon(gutter, gfx, x0, y0)
+ val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
+ val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
+ icon.paintIcon(gutter, gfx, x0, y0)
case None =>
}
}
@@ -318,18 +316,19 @@
/* caret range */
def caret_range(): Text.Range =
- {
- val buffer = model.buffer
- Isabelle.buffer_lock(buffer) {
- val max = buffer.getLength
- val text = new Segment; buffer.getText(0, max, text)
- val chars = BreakIterator.getCharacterInstance(); chars.setText(text)
-
- val stop = chars.following(text_area.getCaretPosition)
- if (stop < 0) Text.Range(max, max)
- else Text.Range(chars.previous(), stop)
+ Isabelle.buffer_lock(model.buffer) {
+ def text(i: Text.Offset): Char = model.buffer.getText(i, 1).charAt(0)
+ val caret = text_area.getCaretPosition
+ try {
+ val c = text(caret)
+ if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(caret + 1)))
+ Text.Range(caret, caret + 2)
+ else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(caret - 1)))
+ Text.Range(caret - 1, caret + 1)
+ else Text.Range(caret, caret + 1)
+ }
+ catch { case _: ArrayIndexOutOfBoundsException => Text.Range(caret, caret + 1) }
}
- }
/* caret handling */
@@ -355,6 +354,12 @@
private val WIDTH = 10
private val HEIGHT = 2
+ private def line_to_y(line: Int): Int =
+ (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
+
+ private def y_to_line(y: Int): Int =
+ (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
+
setPreferredSize(new Dimension(WIDTH, 0))
setRequestFocusEnabled(false)
@@ -386,34 +391,22 @@
Isabelle.buffer_lock(buffer) {
val snapshot = update_snapshot()
- def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
- {
- try {
- val line1 = buffer.getLineOfOffset(snapshot.convert(start))
- val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
- Some((line1, line2))
- }
- catch { case e: ArrayIndexOutOfBoundsException => None }
- }
for {
- (command, start) <- snapshot.node.command_starts
- if !command.is_ignored
- (line1, line2) <- line_range(command, start)
- val y = line_to_y(line1)
- val height = HEIGHT * (line2 - line1)
- color <- Isabelle_Rendering.overview_color(snapshot, command)
+ line <- 0 until buffer.getLineCount
+ range <-
+ try {
+ Some(proper_line_range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line)))
+ }
+ catch { case e: ArrayIndexOutOfBoundsException => None }
+ color <- Isabelle_Rendering.overview_color(snapshot, range)
} {
+ val y = line_to_y(line)
+ val h = (line_to_y(line + 1) - y) max 2
gfx.setColor(color)
- gfx.fillRect(0, y, getWidth - 1, height)
+ gfx.fillRect(0, y, getWidth - 1, h)
}
}
}
-
- private def line_to_y(line: Int): Int =
- (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
-
- private def y_to_line(y: Int): Int =
- (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
}
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Sun Jan 15 17:27:46 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Sun Jan 15 20:03:59 2012 +0100
@@ -10,6 +10,7 @@
import isabelle._
import java.awt.Color
+import javax.swing.Icon
import org.lobobrowser.util.gui.ColorFactory
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
@@ -32,7 +33,7 @@
val running1_color = new Color(97, 0, 97, 100)
val light_color = new Color(240, 240, 240)
- val regular_color = new Color(192, 192, 192)
+ val writeln_color = new Color(192, 192, 192)
val warning_color = new Color(255, 140, 0)
val error_color = new Color(178, 34, 34)
val error1_color = new Color(178, 34, 34, 50)
@@ -45,48 +46,47 @@
val keyword1_color = get_color("#006699")
val keyword2_color = get_color("#009966")
- class Icon(val priority: Int, val icon: javax.swing.Icon)
- {
- def >= (that: Icon): Boolean = this.priority >= that.priority
- }
- val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png"))
- val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png"))
- val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png"))
+ private val writeln_pri = 1
+ private val warning_pri = 2
+ private val legacy_pri = 3
+ private val error_pri = 4
/* command overview */
- def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
+ def overview_color(snapshot: Document.Snapshot, range: Text.Range): Option[Color] =
{
if (snapshot.is_outdated) None
else {
- val state = snapshot.state.command_state(snapshot.version, command)
- val status = Protocol.command_status(state.status)
+ val results =
+ snapshot.cumulate_markup[(Protocol.Status, Int)](
+ range, (Protocol.Status.init, 0),
+ Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
+ {
+ case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
+ if (markup.name == Isabelle_Markup.WARNING) (status, pri max warning_pri)
+ else if (markup.name == Isabelle_Markup.ERROR) (status, pri max error_pri)
+ else (Protocol.command_status(status, markup), pri)
+ })
+ if (results.isEmpty) None
+ else {
+ val (status, pri) =
+ ((Protocol.Status.init, 0) /: results) {
+ case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
- if (status.is_unprocessed) Some(unprocessed_color)
- else if (status.is_running) Some(running_color)
- else if (status.is_finished) {
- if (state.results.exists(r => Protocol.is_error(r._2))) Some(error_color)
- else if (state.results.exists(r => Protocol.is_warning(r._2))) Some(warning_color)
+ if (pri == warning_pri) Some(warning_color)
+ else if (pri == error_pri) Some(error_color)
+ else if (status.is_unprocessed) Some(unprocessed_color)
+ else if (status.is_running) Some(running_color)
+ else if (status.is_failed) Some(error_color)
else None
}
- else if (status.is_failed) Some(error_color)
- else None
}
}
/* markup selectors */
- def message_color(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
- snapshot.select_markup(range,
- Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
- {
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
- })
-
def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
{
val msgs =
@@ -103,42 +103,82 @@
if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
}
+ private val gutter_icons = Map(
+ warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
+ legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
+ error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
+
def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
- snapshot.select_markup(range,
- Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
- {
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
- body match {
- case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
- case _ => warning_icon
- }
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
- }).map(_.info).toList.sortWith(_ >= _).headOption
+ {
+ val results =
+ snapshot.cumulate_markup[Int](range, 0,
+ Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+ {
+ case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
+ body match {
+ case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_pri
+ case _ => pri max warning_pri
+ }
+ case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
+ pri max error_pri
+ })
+ val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
+ gutter_icons.get(pri)
+ }
+
+ private val squiggly_colors = Map(
+ writeln_pri -> writeln_color,
+ warning_pri -> warning_color,
+ error_pri -> error_color)
+
+ def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
+ {
+ val results =
+ snapshot.cumulate_markup[Int](range, 0,
+ Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+ {
+ case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
+ name match {
+ case Isabelle_Markup.WRITELN => pri max writeln_pri
+ case Isabelle_Markup.WARNING => pri max warning_pri
+ case Isabelle_Markup.ERROR => pri max error_pri
+ case _ => pri
+ }
+ })
+ for {
+ Text.Info(r, pri) <- results
+ color <- squiggly_colors.get(pri)
+ } yield Text.Info(r, color)
+ }
def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
- for {
- Text.Info(r, result) <-
- snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
- range, (Some(Protocol.Status()), None),
- Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
- {
- case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
- if (Protocol.command_status_markup(markup.name)) =>
- (Some(Protocol.command_status(status, markup)), color)
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
- (None, Some(bad_color))
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
- (None, Some(hilite_color))
+ {
+ if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
+ else
+ for {
+ Text.Info(r, result) <-
+ snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
+ range, (Some(Protocol.Status.init), None),
+ Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
+ {
+ case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
+ if (Protocol.command_status_markup(markup.name)) =>
+ (Some(Protocol.command_status(status, markup)), color)
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
+ (None, Some(bad_color))
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
+ (None, Some(hilite_color))
+ })
+ color <-
+ (result match {
+ case (Some(status), _) =>
+ if (status.is_running) Some(running1_color)
+ else if (status.is_unprocessed) Some(unprocessed1_color)
+ else None
+ case (_, opt_color) => opt_color
})
- color <-
- (result match {
- case (Some(status), _) =>
- if (status.is_running) Some(running1_color)
- else if (status.is_unprocessed) Some(unprocessed1_color)
- else None
- case (_, opt_color) => opt_color
- })
- } yield Text.Info(r, color)
+ } yield Text.Info(r, color)
+ }
def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
snapshot.select_markup(range,
--- a/src/Tools/jEdit/src/text_area_painter.scala Sun Jan 15 17:27:46 2012 +0100
+++ b/src/Tools/jEdit/src/text_area_painter.scala Sun Jan 15 20:03:59 2012 +0100
@@ -1,7 +1,7 @@
/* Title: Tools/jEdit/src/text_area_painter.scala
Author: Makarius
-Painter setup for main jEdit text area.
+Painter setup for main jEdit text area, depending on common snapshot.
*/
package isabelle.jedit
@@ -16,7 +16,7 @@
import org.gjt.sp.jedit.Debug
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
-import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea}
+import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
class Text_Area_Painter(doc_view: Document_View)
@@ -26,7 +26,7 @@
private val text_area = doc_view.text_area
- /* text area ranges */
+ /* graphics range */
private class Gfx_Range(val x: Int, val y: Int, val length: Int)
@@ -66,10 +66,8 @@
first_line: Int, last_line: Int, physical_lines: Array[Int],
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
- doc_view.robust_body(()) {
- painter_snapshot = doc_view.update_snapshot()
- painter_clip = gfx.getClip
- }
+ painter_snapshot = doc_view.update_snapshot()
+ painter_clip = gfx.getClip
}
}
@@ -79,13 +77,16 @@
first_line: Int, last_line: Int, physical_lines: Array[Int],
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
- doc_view.robust_body(()) {
- painter_snapshot = null
- painter_clip = null
- }
+ painter_snapshot = null
+ painter_clip = null
}
}
+ private def robust_snapshot(body: Document.Snapshot => Unit)
+ {
+ doc_view.robust_body(()) { body(painter_snapshot) }
+ }
+
/* text background */
@@ -95,8 +96,7 @@
first_line: Int, last_line: Int, physical_lines: Array[Int],
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
- doc_view.robust_body(()) {
- val snapshot = painter_snapshot
+ robust_snapshot { snapshot =>
val ascent = text_area.getPainter.getFontMetrics.getAscent
for (i <- 0 until physical_lines.length) {
@@ -123,7 +123,7 @@
// squiggly underline
for {
- Text.Info(range, color) <- Isabelle_Rendering.message_color(snapshot, line_range)
+ Text.Info(range, color) <- Isabelle_Rendering.squiggly_underline(snapshot, line_range)
r <- gfx_range(range)
} {
gfx.setColor(color)
@@ -143,7 +143,7 @@
/* text */
- def char_width(): Int =
+ private def char_width(): Int =
{
val painter = text_area.getPainter
val font = painter.getFont
@@ -185,7 +185,7 @@
result
}
- private def paint_chunk_list(
+ private def paint_chunk_list(snapshot: Document.Snapshot,
gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
{
val clip_rect = gfx.getClipBounds
@@ -214,7 +214,7 @@
val markup =
for {
- r1 <- Isabelle_Rendering.text_color(painter_snapshot, chunk_range, chunk_color)
+ r1 <- Isabelle_Rendering.text_color(snapshot, chunk_range, chunk_color)
r2 <- r1.try_restrict(chunk_range)
} yield r2
@@ -270,7 +270,7 @@
first_line: Int, last_line: Int, physical_lines: Array[Int],
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
- doc_view.robust_body(()) {
+ robust_snapshot { snapshot =>
val clip = gfx.getClip
val x0 = text_area.getHorizontalOffset
val fm = text_area.getPainter.getFontMetrics
@@ -284,7 +284,7 @@
case None => x0
case Some(chunk) =>
gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
- val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt
+ val w = paint_chunk_list(snapshot, gfx, start(i), chunk, x0, y0).toInt
x0 + w.toInt
}
gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
@@ -307,9 +307,7 @@
first_line: Int, last_line: Int, physical_lines: Array[Int],
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
- doc_view.robust_body(()) {
- val snapshot = painter_snapshot
-
+ robust_snapshot { snapshot =>
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
val line_range = doc_view.proper_line_range(start(i), end(i))
@@ -346,7 +344,7 @@
override def paintValidLine(gfx: Graphics2D,
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
{
- doc_view.robust_body(()) {
+ robust_snapshot { _ =>
if (before) gfx.clipRect(0, 0, 0, 0)
else gfx.setClip(painter_clip)
}
@@ -363,7 +361,7 @@
override def paintValidLine(gfx: Graphics2D,
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
{
- doc_view.robust_body(()) {
+ robust_snapshot { _ =>
if (text_area.hasFocus) {
val caret = text_area.getCaretPosition
if (start <= caret && caret == end - 1) {