# HG changeset patch # User wenzelm # Date 1326654239 -3600 # Node ID bed0a3584faf064a1db8813de0179ee7a186a9ac # Parent d0a2c4a80a00f499c5ab4eee921cac7636017423# Parent d8286601e7df9edfe60ad40e1fb23d2533bf6ee4 merged diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/Bali/Conform.thy --- 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)\\(G, L)) = ((x, s)\\(G, L))" -by (auto simp: abrupt_if_def split: split_if) +by (auto simp: abrupt_if_def) lemma conforms_NormI: "(x, s)\\(G, L) \ Norm s\\(G, L)" by (auto simp: conforms_def Let_def) diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/Bali/DefiniteAssignment.thy --- 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\l'\ (rmlab l A) l' = A l'" by (auto simp add: rmlab_def) -lemma range_inter_ts_subseteq [intro]: "\ k. A k \ B k \ \\A \ \\B" +lemma range_inter_ts_subseteq [intro]: "\ k. A k \ B k \ \\A \ \\B" by (auto simp add: range_inter_ts_def) -lemma range_inter_ts_subseteq': - "\\ k. A k \ B k; x \ \\A\ \ x \ \\B" +lemma range_inter_ts_subseteq': "\ k. A k \ B k \ x \ \\A \ x \ \\B" by (auto simp add: range_inter_ts_def) lemma da_monotone: @@ -1072,7 +1071,7 @@ where "Env\ B' \\c\\ C'" and A': "nrm A' = nrm C' \ 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 \ nrm C'" and hyp_brk: "(\l. brk C l \ brk C' l)" by auto then @@ -1095,7 +1094,7 @@ where da_c1: "Env\ B' \\c1\\ C1'" and da_c2: "Env\ nrm C1' \\c2\\ C2'" and A': "nrm A' = nrm C2'" "brk A' = brk C1' \\ brk C2'" - by (rule da_elim_cases) auto + by cases auto note `PROP ?Hyp Env B \c1\ C1` moreover note `B \ B'` moreover note da_c1 @@ -1116,7 +1115,7 @@ where da_c1: "Env\ B' \ assigns_if True e \\c1\\ C1'" and da_c2: "Env\ B' \ assigns_if False e \\c2\\ C2'" and A': "nrm A' = nrm C1' \ nrm C2'" "brk A' = brk C1' \\ brk C2'" - by (rule da_elim_cases) auto + by cases auto note `PROP ?Hyp Env (B \ assigns_if True e) \c1\ C1` moreover note B' = `B \ B'` moreover note da_c1 @@ -1138,7 +1137,7 @@ da_c': "Env\ B' \ assigns_if True e \\c\\ C'" and A': "nrm A' = nrm C' \ (B' \ assigns_if False e)" "brk A' = brk C'" - by (rule da_elim_cases) auto + by cases auto note `PROP ?Hyp Env (B \ assigns_if True e) \c\ C` moreover note B' = `B \ 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 \ nrm C2` `brk A = brk C1 \\ brk C2` @@ -1179,7 +1178,7 @@ \\c2\\ C2'" and A': "nrm A' = nrm C1' \ nrm C2'" "brk A' = brk C1' \\ brk C2'" - by (rule da_elim_cases) auto + by cases auto note `PROP ?Hyp Env B \c1\ C1` moreover note B' = `B \ B'` moreover note da_c1' @@ -1203,7 +1202,7 @@ da_c2': "Env\ B' \\c2\\ C2'" and A': "nrm A' = nrm C1' \ nrm C2'" "brk A' = (brk C1' \\\<^sub>\ nrm C2') \\ (brk C2')" - by (rule da_elim_cases) auto + by cases auto note `PROP ?Hyp Env B \c1\ C1` moreover note B' = `B \ 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 \ @@ -1241,24 +1240,24 @@ assigns_if True (BinOp CondAnd e1 e2) \ assigns_if False (BinOp CondAnd e1 e2)" "brk A' = (\l. UNIV)" - by (rule da_elim_cases) auto + by cases auto note B' = `B \ 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 \ @@ -1273,7 +1272,7 @@ assigns_if True (c ? e1 : e2) \ assigns_if False (c ? e1 : e2)" "brk A' = (\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 \\) *) note B' = `B \ B'` with A A' show ?case @@ -1289,7 +1288,7 @@ A': "nrm A' = nrm E1' \ nrm E2'" "brk A' = (\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 \\) *) note `PROP ?Hyp Env (B \ assigns_if True c) \e1\ E1` moreover note B' = `B \ 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 \ B'`) diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/MicroJava/BV/BVNoTypeError.thy --- 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) diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/MicroJava/BV/JVM.thy --- 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 \ 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'))" . diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/MicroJava/BV/Typing_Framework_JVM.thy --- 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 diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/MicroJava/Comp/CorrComp.thy --- 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: "\ wf_java_prog G; is_class G C; method (G, C) S = Some (D, rT, pns, lvars, blk, res) \ \ 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] diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/MicroJava/Comp/CorrCompTp.thy --- 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 \ *) 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) \ 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) diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/MicroJava/Comp/Index.thy --- 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 \ This") apply simp apply (subgoal_tac "\ x \ set pns. (\z. z \ vn) x") -apply (simp add: takeWhile_append2) +apply simp apply (subgoal_tac "length (takeWhile (\z. z \ vn) (map fst lvars)) < length (map fst lvars)") apply simp apply (rule length_takeWhile) @@ -86,7 +86,7 @@ \ index (pns, zs @ ((xvar, xval) # xys), blk, res) xvar = Suc (length pns + length zs)" apply (simp add: index_def) apply (subgoal_tac "(\x. ((x \ (set pns)) \ ((\z. (z \ xvar))x)))") -apply (simp add: List.takeWhile_append2) +apply simp apply (subgoal_tac "(takeWhile (\z. z \ xvar) (map fst zs @ xvar # map fst xys)) = map fst zs @ (takeWhile (\z. z \ 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) \ 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 \ This", simp) apply (subgoal_tac "takeWhile (\z. z \ vn) (map fst lvars_pre @ vn # map fst lvars_post) = diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/MicroJava/Comp/LemmasComp.thy --- 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 (\(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 (\ 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 (\(s, m). (s, Ca, m))") apply (drule_tac g="(Fun.comp (\(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/MicroJava/DFA/Kildall.thy --- 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 "\q t. \((q, t) \ set qs \ t +_f ss ! q \ ss ! q)") - apply (blast intro!: psubsetI elim: equalityE) + apply (blast elim: equalityE) apply clarsimp apply (drule bspec, assumption) apply (drule bspec, assumption) diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/MicroJava/DFA/Semilat.thy --- 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: "\ x \ A; y \ A \ \ (x \\<^sub>r y) = (x \\<^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: "\ x \ A; y \ A \ \ (x \\<^sub>r y) = (y \\<^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 diff -r d0a2c4a80a00 -r bed0a3584faf src/HOL/Tools/record.ML --- 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 diff -r d0a2c4a80a00 -r bed0a3584faf src/Pure/PIDE/protocol.scala --- 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 */ diff -r d0a2c4a80a00 -r bed0a3584faf src/Tools/jEdit/src/document_view.scala --- 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 } diff -r d0a2c4a80a00 -r bed0a3584faf src/Tools/jEdit/src/isabelle_rendering.scala --- 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, diff -r d0a2c4a80a00 -r bed0a3584faf src/Tools/jEdit/src/text_area_painter.scala --- 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) {