--- 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)) = (\<exists>T ST'. ST = T#ST' \<and> 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)) =
(\<exists>oT vT ST'. ST = oT#ST' \<and> is_class G C \<and>
field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> 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)) = (\<exists>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)) =
(\<exists>T ST'. ST = T#ST' \<and> 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)) =
(\<exists>T ST'. ST = T#ST'\<and> G \<turnstile> T \<preceq> rT)"
- by (cases ST, auto)
+ by (cases ST) auto
lemma app'Throw[simp]:
"app' (Throw, G, pc, maxs, rT, (ST,LT)) =
(\<exists>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:
- "\<And>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
--- 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 \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
- apply (cases X)
- apply auto
- done
+ by (cases X) auto
section {* approx-val *}
@@ -91,12 +89,12 @@
lemma approx_val_heap_update:
"\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk>
\<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>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:
"\<lbrakk> approx_val G hp v T; G \<turnstile> T <=o T'; wf_prog wt G \<rbrakk>
\<Longrightarrow> 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\<mapsto>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)
--- 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);
--- 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()
+ }
}
--- 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
--- 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
--- 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()
}
--- 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
}
}