# HG changeset patch # User wenzelm # Date 1376396422 -7200 # Node ID bb18eed53ed689d6af57993225ba50a8c5cd73e3 # Parent ea02bc4e9a5f3ffdd6a9e9018c8661a7725c9f27# Parent 128bec4e3fcabefcc12b086ab6d34444487d3d20 merged diff -r ea02bc4e9a5f -r bb18eed53ed6 src/HOL/MicroJava/BV/BVNoTypeError.thy --- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Aug 13 11:34:56 2013 +0200 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Aug 13 14:20:22 2013 +0200 @@ -22,13 +22,13 @@ lemma app'Store[simp]: "app' (Store idx, G, pc, maxs, rT, (ST,LT)) = (\T ST'. ST = T#ST' \ idx < length LT)" - by (cases ST, auto) + by (cases ST) auto lemma app'GetField[simp]: "app' (Getfield F C, G, pc, maxs, rT, (ST,LT)) = (\oT vT ST'. ST = oT#ST' \ is_class G C \ field (G,C) F = Some (C,vT) \ G \ oT \ Class C)" - by (cases ST, auto) + by (cases ST) auto lemma app'PutField[simp]: "app' (Putfield F C, G, pc, maxs, rT, (ST,LT)) = @@ -61,13 +61,13 @@ lemma app'Pop[simp]: "app' (Pop, G, pc, maxs, rT, (ST,LT)) = (\T ST'. ST = T#ST')" - by (cases ST, auto) + by (cases ST) auto lemma app'Dup[simp]: "app' (Dup, G, pc, maxs, rT, (ST,LT)) = (\T ST'. ST = T#ST' \ length ST < maxs)" - by (cases ST, auto) + by (cases ST) auto lemma app'Dup_x1[simp]: @@ -125,13 +125,14 @@ lemma app'Return[simp]: "app' (Return, G, pc, maxs, rT, (ST,LT)) = (\T ST'. ST = T#ST'\ G \ T \ rT)" - by (cases ST, auto) + by (cases ST) auto lemma app'Throw[simp]: "app' (Throw, G, pc, maxs, rT, (ST,LT)) = (\ST' r. ST = RefT r#ST')" - apply (cases ST, simp) + apply (cases ST) + apply simp apply (cases "hd ST") apply auto done @@ -170,7 +171,7 @@ with app show "?P ST LT" apply (clarsimp simp add: list_all2_def) - apply ((rule exI)+, (rule conjI)?)+ + apply (intro exI conjI) apply auto done qed @@ -198,9 +199,8 @@ done lemma list_all2_approx: - "\s. list_all2 (approx_val G hp) s (map OK S) = - list_all2 (conf G hp) s S" - apply (induct S) + "list_all2 (approx_val G hp) s (map OK S) = list_all2 (conf G hp) s S" + apply (induct S arbitrary: s) apply (auto simp add: list_all2_Cons2 approx_val_def) done diff -r ea02bc4e9a5f -r bb18eed53ed6 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Tue Aug 13 11:34:56 2013 +0200 +++ b/src/HOL/MicroJava/BV/Correct.thy Tue Aug 13 14:20:22 2013 +0200 @@ -65,9 +65,7 @@ lemma sup_ty_opt_OK: "(G \ X <=o (OK T')) = (\T. X = OK T \ G \ T \ T')" - apply (cases X) - apply auto - done + by (cases X) auto section {* approx-val *} @@ -91,12 +89,12 @@ lemma approx_val_heap_update: "\ hp a = Some obj'; G,hp\ v::\T; obj_ty obj = obj_ty obj'\ \ G,hp(a\obj)\ v::\T" - by (cases v, auto simp add: obj_ty_def conf_def) + by (cases v) (auto simp add: obj_ty_def conf_def) lemma approx_val_widen: "\ approx_val G hp v T; G \ T <=o T'; wf_prog wt G \ \ approx_val G hp v T'" - by (cases T', auto simp add: sup_ty_opt_OK intro: conf_widen) + by (cases T') (auto simp add: sup_ty_opt_OK intro: conf_widen) section {* approx-loc *} @@ -284,7 +282,7 @@ shows preallocated_newref: "preallocated (hp(oref\obj))" proof (cases oref) case (XcptRef x) - with none alloc have "False" by (auto elim: preallocatedE [of _ x]) + with none alloc have False by (auto elim: preallocatedE [of _ x]) thus ?thesis .. next case (Loc l) diff -r ea02bc4e9a5f -r bb18eed53ed6 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Tue Aug 13 11:34:56 2013 +0200 +++ b/src/Pure/PIDE/command.ML Tue Aug 13 14:20:22 2013 +0200 @@ -231,39 +231,42 @@ let val print_functions = Synchronized.value print_functions; + fun make_print name args {delay, pri, persistent, strict, print_fn} = + let + val exec_id = Document_ID.make (); + fun process () = + let + val {failed, command, state = st', ...} = eval_result eval; + val tr = Toplevel.exec_id exec_id command; + in + if failed andalso strict then () + else print_error tr (fn () => print_fn tr st') + end; + in + Print { + name = name, args = args, delay = delay, pri = pri, persistent = persistent, + exec_id = exec_id, print_process = memo exec_id process} + end; + + fun bad_print name args exn = + make_print name args {delay = NONE, pri = 0, persistent = false, + strict = false, print_fn = fn _ => fn _ => reraise exn}; + fun new_print name args get_pr = let - fun make_print {delay, pri, persistent, strict, print_fn} = - let - val exec_id = Document_ID.make (); - fun process () = - let - val {failed, command, state = st', ...} = eval_result eval; - val tr = Toplevel.exec_id exec_id command; - in - if failed andalso strict then () - else print_error tr (fn () => print_fn tr st') - end; - in - Print { - name = name, args = args, delay = delay, pri = pri, persistent = persistent, - exec_id = exec_id, print_process = memo exec_id process} - end; val params = {command_name = command_name, args = args}; in (case Exn.capture (Runtime.controlled_execution get_pr) params of Exn.Res NONE => NONE - | Exn.Res (SOME pr) => SOME (make_print pr) - | Exn.Exn exn => - SOME (make_print {delay = NONE, pri = 0, persistent = false, - strict = false, print_fn = fn _ => fn _ => reraise exn})) + | Exn.Res (SOME pr) => SOME (make_print name args pr) + | Exn.Exn exn => SOME (bad_print name args exn)) end; fun get_print (a, b) = (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of NONE => (case AList.lookup (op =) print_functions a of - NONE => NONE + NONE => SOME (bad_print a b (ERROR ("Missing print function " ^ quote a))) | SOME get_pr => new_print a b get_pr) | some => some); diff -r ea02bc4e9a5f -r bb18eed53ed6 src/Pure/PIDE/query_operation.scala --- a/src/Pure/PIDE/query_operation.scala Tue Aug 13 11:34:56 2013 +0200 +++ b/src/Pure/PIDE/query_operation.scala Tue Aug 13 14:20:22 2013 +0200 @@ -199,5 +199,9 @@ } def activate() { editor.session.commands_changed += main_actor } - def deactivate() { editor.session.commands_changed -= main_actor } + + def deactivate() { + editor.session.commands_changed -= main_actor + remove_overlay() + } } diff -r ea02bc4e9a5f -r bb18eed53ed6 src/Tools/adhoc_overloading.ML --- a/src/Tools/adhoc_overloading.ML Tue Aug 13 11:34:56 2013 +0200 +++ b/src/Tools/adhoc_overloading.ML Tue Aug 13 14:20:22 2013 +0200 @@ -23,16 +23,16 @@ (* errors *) -fun duplicate_variant_error oconst = +fun err_duplicate_variant oconst = error ("Duplicate variant of " ^ quote oconst); -fun not_a_variant_error oconst = +fun err_not_a_variant oconst = error ("Not a variant of " ^ quote oconst); -fun not_overloaded_error oconst = +fun err_not_overloaded oconst = error ("Constant " ^ quote oconst ^ " is not declared as overloaded"); -fun unresolved_overloading_error ctxt (c, T) t instances = +fun err_unresolved_overloading ctxt (c, T) t instances = let val ctxt' = Config.put show_variants true ctxt in cat_lines ( @@ -64,7 +64,7 @@ let fun merge_oconsts _ (oconst1, oconst2) = if oconst1 = oconst2 then oconst1 - else duplicate_variant_error oconst1; + else err_duplicate_variant oconst1; in {variants = Symtab.merge_list variants_eq (vtab1, vtab2), oconsts = Termtab.join merge_oconsts (otab1, otab2)} @@ -94,15 +94,15 @@ in map_tables (Symtab.delete_safe oconst) remove_variants context end; in if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst - else not_overloaded_error oconst + else err_not_overloaded oconst end; local fun generic_variant add oconst t context = let val ctxt = Context.proof_of context; - val _ = if is_overloaded ctxt oconst then () else not_overloaded_error oconst; - val T = t |> singleton (Variable.polymorphic ctxt) |> fastype_of; + val _ = if is_overloaded ctxt oconst then () else err_not_overloaded oconst; + val T = t |> fastype_of; val t' = Term.map_types (K dummyT) t; in if add then @@ -110,7 +110,7 @@ val _ = (case get_overloaded ctxt t' of NONE => () - | SOME oconst' => duplicate_variant_error oconst'); + | SOME oconst' => err_duplicate_variant oconst'); in map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t', oconst)) context end @@ -118,7 +118,7 @@ let val _ = if member variants_eq (the (get_variants ctxt oconst)) (t', T) then () - else not_a_variant_error oconst; + else err_not_a_variant oconst; in map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T))) (Termtab.delete_safe t') context @@ -135,65 +135,55 @@ (* check / uncheck *) -fun unifiable_with thy T1 (t, T2) = +fun unifiable_with thy T1 T2 = let val maxidx1 = Term.maxidx_of_typ T1; val T2' = Logic.incr_tvar (maxidx1 + 1) T2; val maxidx2 = Term.maxidx_typ T2' maxidx1; - in - (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME t) - handle Type.TUNIFY => NONE - end; + in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end; -fun get_instances ctxt (c, T) = - Same.function (get_variants ctxt) c - |> map_filter (unifiable_with (Proof_Context.theory_of ctxt) T); +fun get_candidates ctxt (c, T) = + get_variants ctxt c + |> Option.map (map_filter (fn (t, T') => + if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t + else NONE)); + +fun insert_variants ctxt t (oconst as Const (c, T)) = + (case get_candidates ctxt (c, T) of + SOME [] => err_unresolved_overloading ctxt (c, T) t [] + | SOME [variant] => variant + | _ => oconst) + | insert_variants _ _ oconst = oconst; -fun insert_variants_same ctxt t (Const (c, T)) = - (case get_instances ctxt (c, T) of - [] => unresolved_overloading_error ctxt (c, T) t [] - | [variant] => variant - | _ => raise Same.SAME) - | insert_variants_same _ _ _ = raise Same.SAME; +fun insert_overloaded ctxt variant = + (case try Term.type_of variant of + NONE => variant + | SOME T => + Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] + [Option.map (Const o rpair T) o get_overloaded ctxt o Term.map_types (K dummyT)] variant); -fun insert_overloaded_same ctxt variant = +fun check ctxt = + map (fn t => Term.map_aterms (insert_variants ctxt t) t); + +fun uncheck ctxt = + if Config.get ctxt show_variants then I + else map (insert_overloaded ctxt); + +fun reject_unresolved ctxt = let - val thy = Proof_Context.theory_of ctxt; - val t = Pattern.rewrite_term thy [] [fn t => - Term.map_types (K dummyT) t - |> get_overloaded ctxt - |> Option.map (Const o rpair (fastype_of variant))] variant; - in - if Term.aconv_untyped (variant, t) then raise Same.SAME - else t - end; - -fun gen_check_uncheck replace ts ctxt = - Same.capture (Same.map replace) ts - |> Option.map (rpair ctxt); - -fun check ts ctxt = gen_check_uncheck (fn t => - Term_Subst.map_aterms_same (insert_variants_same ctxt t) t) ts ctxt; - -fun uncheck ts ctxt = - if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then NONE - else gen_check_uncheck (insert_overloaded_same ctxt) ts ctxt; - -fun reject_unresolved ts ctxt = - let + val the_candidates = the o get_candidates ctxt; fun check_unresolved t = (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of - [] => () - | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t (get_instances ctxt (c, T))); - val _ = map check_unresolved ts; - in NONE end; + [] => t + | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT)); + in map check_unresolved end; (* setup *) val _ = Context.>> - (Syntax_Phases.term_check' 0 "adhoc_overloading" check - #> Syntax_Phases.term_check' 1 "adhoc_overloading_unresolved_check" reject_unresolved - #> Syntax_Phases.term_uncheck' 0 "adhoc_overloading" uncheck); + (Syntax_Phases.term_check 0 "adhoc_overloading" check + #> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved + #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck); (* commands *) @@ -216,10 +206,11 @@ fun adhoc_overloading_cmd add raw_args lthy = let fun const_name ctxt = fst o dest_Const o Proof_Context.read_const ctxt false dummyT; + fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt; val args = raw_args |> map (apfst (const_name lthy)) - |> map (apsnd (map (Syntax.read_term lthy))); + |> map (apsnd (map (read_term lthy))); in Local_Theory.declaration {syntax = true, pervasive = false} (adhoc_overloading_cmd' add args) lthy diff -r ea02bc4e9a5f -r bb18eed53ed6 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Tue Aug 13 11:34:56 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Aug 13 14:20:22 2013 +0200 @@ -76,6 +76,21 @@ def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath + /* focus of main window */ + + def request_focus_view: Unit = + { + jEdit.getActiveView() match { + case null => + case view => + view.getTextArea match { + case null => + case text_area => text_area.requestFocus + } + } + } + + /* main jEdit components */ def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator diff -r ea02bc4e9a5f -r bb18eed53ed6 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Tue Aug 13 11:34:56 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Aug 13 14:20:22 2013 +0200 @@ -170,6 +170,10 @@ if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 => Registers.copy(text_area, '$') evt.consume + case KeyEvent.VK_A + if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 => + text_area.selectAll + evt.consume case _ => } if (propagate_keys && !evt.isConsumed) @@ -194,6 +198,7 @@ getBuffer.setTokenMarker(new Token_Markup.Marker(true, None)) getBuffer.setReadOnly(true) + getBuffer.setStringProperty("noWordSep", "_'.?") rich_text_area.activate() } diff -r ea02bc4e9a5f -r bb18eed53ed6 src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Tue Aug 13 11:34:56 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Tue Aug 13 14:20:22 2013 +0200 @@ -116,7 +116,7 @@ stack = rest rest match { case top :: _ => top.request_focus - case Nil => + case Nil => JEdit_Lib.request_focus_view } case _ => } @@ -129,6 +129,7 @@ else { stack.foreach(_.hide_popup) stack = Nil + JEdit_Lib.request_focus_view true } }