--- a/NEWS Wed Mar 14 17:19:30 2012 +0000
+++ b/NEWS Wed Mar 14 22:34:18 2012 +0100
@@ -371,6 +371,12 @@
*** ML ***
+* Local_Theory.define no longer hard-wires default theorem name
+"foo_def": definitional packages need to make this explicit, and may
+choose to omit theorem bindings for definitions by using
+Binding.empty/Attrib.empty_binding. Potential INCOMPATIBILITY for
+derived definitional packages.
+
* Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
conformance with similar operations in structure Term and Logic.
--- a/src/HOL/Library/Multiset.thy Wed Mar 14 17:19:30 2012 +0000
+++ b/src/HOL/Library/Multiset.thy Wed Mar 14 22:34:18 2012 +0100
@@ -118,8 +118,8 @@
lemma count_union [simp]: "count (M + N) a = count M a + count N a"
by (simp add: union_def in_multiset multiset_typedef)
-instance multiset :: (type) cancel_comm_monoid_add proof
-qed (simp_all add: multiset_eq_iff)
+instance multiset :: (type) cancel_comm_monoid_add
+ by default (simp_all add: multiset_eq_iff)
subsubsection {* Difference *}
@@ -270,8 +270,8 @@
definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
-instance proof
-qed (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
+instance
+ by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
end
@@ -377,10 +377,11 @@
definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
multiset_inter_def: "inf_multiset A B = A - (A - B)"
-instance proof -
+instance
+proof -
have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
- show "OFCLASS('a multiset, semilattice_inf_class)" proof
- qed (auto simp add: multiset_inter_def mset_le_def aux)
+ show "OFCLASS('a multiset, semilattice_inf_class)"
+ by default (auto simp add: multiset_inter_def mset_le_def aux)
qed
end
@@ -822,7 +823,8 @@
lemma multiset_of_eq_length:
assumes "multiset_of xs = multiset_of ys"
shows "length xs = length ys"
-using assms proof (induct xs arbitrary: ys)
+using assms
+proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
@@ -845,7 +847,8 @@
next
case True
moreover have "z \<in># multiset_of ys" using assms True by simp
- show ?thesis using assms proof (induct xs arbitrary: ys)
+ show ?thesis using assms
+ proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
@@ -864,7 +867,8 @@
assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
and equiv: "multiset_of xs = multiset_of ys"
shows "fold f xs = fold f ys"
-using f equiv [symmetric] proof (induct xs arbitrary: ys)
+using f equiv [symmetric]
+proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
@@ -898,7 +902,8 @@
and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
and "sorted (map f ys)"
shows "sort_key f xs = ys"
-using assms proof (induct xs arbitrary: ys)
+using assms
+proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
@@ -994,10 +999,12 @@
proof (cases xs)
case Nil then show ?thesis by simp
next
- case (Cons _ ys) note hyps = Cons show ?thesis proof (cases ys)
+ case (Cons _ ys) note hyps = Cons show ?thesis
+ proof (cases ys)
case Nil with hyps show ?thesis by simp
next
- case (Cons _ zs) note hyps = hyps Cons show ?thesis proof (cases zs)
+ case (Cons _ zs) note hyps = hyps Cons show ?thesis
+ proof (cases zs)
case Nil with hyps show ?thesis by auto
next
case Cons
@@ -1224,8 +1231,8 @@
definition
[code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
-instance proof
-qed (simp add: equal_multiset_def eq_iff)
+instance
+ by default (simp add: equal_multiset_def eq_iff)
end
@@ -1512,8 +1519,8 @@
qed
have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
- show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
- qed (auto simp add: le_multiset_def irrefl dest: trans)
+ show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
+ by default (auto simp add: le_multiset_def irrefl dest: trans)
qed
lemma mult_less_irrefl [elim!]: "M \<subset># (M::'a::order multiset) ==> R"
@@ -1785,14 +1792,12 @@
enriched_type image_mset: image_mset
proof -
- fix f g
- show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
+ fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
proof
fix A
show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
by (induct A) simp_all
qed
-next
show "image_mset id = id"
proof
fix A
--- a/src/HOL/Statespace/state_space.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/HOL/Statespace/state_space.ML Wed Mar 14 22:34:18 2012 +0100
@@ -15,7 +15,7 @@
val namespace_definition :
bstring ->
typ ->
- Expression.expression ->
+ (xstring, string) Expression.expr * (binding * string option * mixfix) list ->
string list -> string list -> theory -> theory
val define_statespace :
@@ -139,9 +139,12 @@
val get_silent = #silent o NameSpaceData.get;
+fun expression_no_pos (expr, fixes) : Expression.expression =
+ (map (fn (name, inst) => ((name, Position.none), inst)) expr, fixes);
+
fun prove_interpretation_in ctxt_tac (name, expr) thy =
thy
- |> Expression.sublocale_cmd I name expr []
+ |> Expression.sublocale_cmd I (name, Position.none) (expression_no_pos expr) []
|> Proof.global_terminal_proof
(Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
|> Proof_Context.theory_of
@@ -154,7 +157,7 @@
fun add_locale_cmd name expr elems thy =
thy
- |> Expression.add_locale_cmd I (Binding.name name) Binding.empty expr elems
+ |> Expression.add_locale_cmd I (Binding.name name) Binding.empty (expression_no_pos expr) elems
|> snd
|> Local_Theory.exit;
--- a/src/HOL/Tools/inductive.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/HOL/Tools/inductive.ML Wed Mar 14 22:34:18 2012 +0100
@@ -562,9 +562,12 @@
fun gen_inductive_cases prep_att prep_prop args lthy =
let
val thy = Proof_Context.theory_of lthy;
- val facts = args |> grouped 10 Par_List.map (fn ((a, atts), props) =>
- ((a, map (prep_att thy) atts),
- map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
+ val thmss =
+ map snd args
+ |> burrow (grouped 10 Par_List.map (mk_cases lthy o prep_prop lthy));
+ val facts =
+ map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
+ args thmss;
in lthy |> Local_Theory.notes facts |>> map snd end;
val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
@@ -809,7 +812,7 @@
|> Local_Theory.conceal
|> Local_Theory.define
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
- ((Binding.empty, @{attributes [nitpick_unfold]}),
+ ((Thm.def_binding rec_name, @{attributes [nitpick_unfold]}),
fold_rev lambda params
(Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
||> Local_Theory.restore_naming lthy;
--- a/src/Pure/Isar/class.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/class.ML Wed Mar 14 22:34:18 2012 +0100
@@ -37,7 +37,6 @@
-> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
val read_multi_arity: theory -> xstring list * xstring list * xstring
-> string list * (string * sort) list * sort
- val type_name: string -> string
val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
@@ -57,7 +56,7 @@
(** class data **)
-datatype class_data = ClassData of {
+datatype class_data = Class_Data of {
(* static part *)
consts: (string * string) list
@@ -78,23 +77,23 @@
fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
(defs, operations)) =
- ClassData { consts = consts, base_sort = base_sort,
+ Class_Data {consts = consts, base_sort = base_sort,
base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
- of_class = of_class, axiom = axiom, defs = defs, operations = operations };
-fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro,
- of_class, axiom, defs, operations }) =
+ of_class = of_class, axiom = axiom, defs = defs, operations = operations};
+fun map_class_data f (Class_Data {consts, base_sort, base_morph, export_morph, assm_intro,
+ of_class, axiom, defs, operations}) =
make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
(defs, operations)));
-fun merge_class_data _ (ClassData { consts = consts,
+fun merge_class_data _ (Class_Data {consts = consts,
base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
- of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
- ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
- of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
+ of_class = of_class, axiom = axiom, defs = defs1, operations = operations1},
+ Class_Data {consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
+ of_class = _, axiom = _, defs = defs2, operations = operations2}) =
make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
(Thm.merge_thms (defs1, defs2),
AList.merge (op =) (K true) (operations1, operations2)));
-structure ClassData = Theory_Data
+structure Class_Data = Theory_Data
(
type T = class_data Graph.T
val empty = Graph.empty;
@@ -105,18 +104,20 @@
(* queries *)
-fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class
- of SOME (ClassData data) => SOME data
- | NONE => NONE;
+fun lookup_class_data thy class =
+ (case try (Graph.get_node (Class_Data.get thy)) class of
+ SOME (Class_Data data) => SOME data
+ | NONE => NONE);
-fun the_class_data thy class = case lookup_class_data thy class
- of NONE => error ("Undeclared class " ^ quote class)
- | SOME data => data;
+fun the_class_data thy class =
+ (case lookup_class_data thy class of
+ NONE => error ("Undeclared class " ^ quote class)
+ | SOME data => data);
val is_class = is_some oo lookup_class_data;
-val ancestry = Graph.all_succs o ClassData.get;
-val heritage = Graph.all_preds o ClassData.get;
+val ancestry = Graph.all_succs o Class_Data.get;
+val heritage = Graph.all_preds o Class_Data.get;
fun these_params thy =
let
@@ -133,20 +134,21 @@
val base_sort = #base_sort oo the_class_data;
fun rules thy class =
- let val { axiom, of_class, ... } = the_class_data thy class
+ let val {axiom, of_class, ...} = the_class_data thy class
in (axiom, of_class) end;
fun all_assm_intros thy =
- Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm)
- (the_list assm_intro)) (ClassData.get thy) [];
+ Graph.fold (fn (_, (Class_Data {assm_intro, ...}, _)) => fold (insert Thm.eq_thm)
+ (the_list assm_intro)) (Class_Data.get thy) [];
fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
val base_morphism = #base_morph oo the_class_data;
-fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class])
- of SOME eq_morph => base_morphism thy class $> eq_morph
- | NONE => base_morphism thy class;
+fun morphism thy class =
+ (case Element.eq_morphism thy (these_defs thy [class]) of
+ SOME eq_morph => base_morphism thy class $> eq_morph
+ | NONE => base_morphism thy class);
val export_morphism = #export_morph oo the_class_data;
fun print_classes ctxt =
@@ -195,13 +197,14 @@
make_class_data (((map o pairself) fst params, base_sort,
base_morph, export_morph, assm_intro, of_class, axiom), ([], operations)))
#> fold (curry Graph.add_edge class) sups;
- in ClassData.map add_class thy end;
+ in Class_Data.map add_class thy end;
-fun activate_defs class thms thy = case Element.eq_morphism thy thms
- of SOME eq_morph => fold (fn cls => fn thy =>
+fun activate_defs class thms thy =
+ (case Element.eq_morphism thy thms of
+ SOME eq_morph => fold (fn cls => fn thy =>
Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
(eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
- | NONE => thy;
+ | NONE => thy);
fun register_operation class (c, (t, some_def)) thy =
let
@@ -213,7 +216,7 @@
val ty' = Term.fastype_of t';
in
thy
- |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
+ |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd)
(fn (defs, operations) =>
(fold cons (the_list some_def) defs,
(c, (class, (ty', t'))) :: operations))
@@ -231,14 +234,15 @@
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
|> filter (is_class thy);
- val add_dependency = case some_dep_morph
- of SOME dep_morph => Locale.add_dependency sub
+ val add_dependency =
+ (case some_dep_morph of
+ SOME dep_morph => Locale.add_dependency sub
(sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) NONE export
- | NONE => I
+ | NONE => I);
in
thy
|> AxClass.add_classrel classrel
- |> ClassData.map (Graph.add_edge (sub, sup))
+ |> Class_Data.map (Graph.add_edge (sub, sup))
|> activate_defs sub (these_defs thy diff_sort)
|> add_dependency
end;
@@ -265,17 +269,19 @@
(map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
val secondary_constraints =
(map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
- fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
- of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
- of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
- of SOME (_, ty' as TVar (vi, sort)) =>
- if Type_Infer.is_param vi
- andalso Sorts.sort_le algebra (base_sort, sort)
- then SOME (ty', TFree (Name.aT, base_sort))
- else NONE
+ fun improve (c, ty) =
+ (case AList.lookup (op =) primary_constraints c of
+ SOME ty' =>
+ (case try (Type.raw_match (ty', ty)) Vartab.empty of
+ SOME tyenv =>
+ (case Vartab.lookup tyenv (Name.aT, 0) of
+ SOME (_, ty' as TVar (vi, sort)) =>
+ if Type_Infer.is_param vi andalso Sorts.sort_le algebra (base_sort, sort)
+ then SOME (ty', TFree (Name.aT, base_sort))
+ else NONE
| _ => NONE)
| NONE => NONE)
- | NONE => NONE)
+ | NONE => NONE);
fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
val unchecks = these_unchecks thy sort;
in
@@ -398,20 +404,24 @@
structure Instantiation = Proof_Data
(
- type T = instantiation
- fun init _ = Instantiation { arities = ([], [], []), params = [] };
+ type T = instantiation;
+ fun init _ = Instantiation {arities = ([], [], []), params = []};
);
fun mk_instantiation (arities, params) =
- Instantiation { arities = arities, params = params };
-fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy)
- of Instantiation data => data;
-fun map_instantiation f = (Local_Theory.target o Instantiation.map)
- (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
+ Instantiation {arities = arities, params = params};
+
+val get_instantiation =
+ (fn Instantiation data => data) o Instantiation.get o Local_Theory.target_of;
-fun the_instantiation lthy = case get_instantiation lthy
- of { arities = ([], [], []), ... } => error "No instantiation target"
- | data => data;
+fun map_instantiation f =
+ (Local_Theory.target o Instantiation.map)
+ (fn Instantiation {arities, params} => mk_instantiation (f (arities, params)));
+
+fun the_instantiation lthy =
+ (case get_instantiation lthy of
+ {arities = ([], [], []), ...} => error "No instantiation target"
+ | data => data);
val instantiation_params = #params o get_instantiation;
@@ -434,20 +444,21 @@
fun synchronize_inst_syntax ctxt =
let
- val Instantiation { params, ... } = Instantiation.get ctxt;
+ val Instantiation {params, ...} = Instantiation.get ctxt;
val lookup_inst_param = AxClass.lookup_inst_param
(Sign.consts_of (Proof_Context.theory_of ctxt)) params;
- fun subst (c, ty) = case lookup_inst_param (c, ty)
- of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
- | NONE => NONE;
+ fun subst (c, ty) =
+ (case lookup_inst_param (c, ty) of
+ SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
+ | NONE => NONE);
val unchecks =
map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
in
ctxt
|> Overloading.map_improvable_syntax
- (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
- (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
+ (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
+ (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
end;
fun resort_terms ctxt algebra consts constraints ts =
@@ -467,53 +478,35 @@
(* target *)
-val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*)
- let
- fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
- orelse s = "'" orelse s = "_";
- val is_junk = not o is_valid andf Symbol.is_regular;
- val junk = Scan.many is_junk;
- val scan_valids = Symbol.scanner "Malformed input"
- ((junk |--
- (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
- --| junk))
- ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
- in
- raw_explode #> scan_valids #> implode
- end;
-
-val type_name = sanitize_name o Long_Name.base_name;
-
fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.background_theory_result
(AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
##> Local_Theory.target synchronize_inst_syntax;
fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
- case instantiation_param lthy b
- of SOME c => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
- else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
- | NONE => lthy |>
- Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+ (case instantiation_param lthy b of
+ SOME c =>
+ if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
+ else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
+ | NONE => lthy |>
+ Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params));
fun pretty lthy =
let
- val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
+ val {arities = (tycos, vs, sort), params} = the_instantiation lthy;
fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
fun pr_param ((c, _), (v, ty)) =
Pretty.block (Pretty.breaks
[Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
Pretty.str "::", Syntax.pretty_typ lthy ty]);
- in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
+ in Pretty.command "instantiation" :: map pr_arity tycos @ map pr_param params end;
fun conclude lthy =
let
val (tycos, vs, sort) = #arities (the_instantiation lthy);
val thy = Proof_Context.theory_of lthy;
val _ = tycos |> List.app (fn tyco =>
- if Sign.of_sort thy
- (Type (tyco, map TFree vs), sort)
- then ()
+ if Sign.of_sort thy (Type (tyco, map TFree vs), sort) then ()
else error ("Missing instance proof for type " ^ quote (Proof_Context.extern_type lthy tyco)));
in lthy end;
@@ -524,7 +517,7 @@
fun get_param tyco (param, (_, (c, ty))) =
if can (AxClass.param_of_inst thy) (c, tyco)
then NONE else SOME ((c, tyco),
- (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
+ (param ^ "_" ^ Long_Name.base_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
val params = map_product get_param tycos class_params |> map_filter I;
val primary_constraints = map (apsnd
(map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
--- a/src/Pure/Isar/class_declaration.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/class_declaration.ML Wed Mar 14 22:34:18 2012 +0100
@@ -198,10 +198,11 @@
fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =
let
+ val thy_ctxt = Proof_Context.init_global thy;
(* prepare import *)
val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
- val sups = Sign.minimize_sort thy (map (prep_class thy) raw_supclasses);
+ val sups = Sign.minimize_sort thy (map (prep_class thy_ctxt) raw_supclasses);
val _ =
(case filter_out (Class.is_class thy) sups of
[] => ()
@@ -219,7 +220,7 @@
val sup_sort = inter_sort base_sort sups;
(* process elements as class specification *)
- val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy);
+ val class_ctxt = Class.begin sups base_sort thy_ctxt;
val ((_, _, syntax_elems), _) = class_ctxt
|> Expression.cert_declaration supexpr I inferred_elems;
fun check_vars e vs =
@@ -243,7 +244,7 @@
in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end;
val cert_class_spec = prep_class_spec (K I) cert_class_elems;
-val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
+val read_class_spec = prep_class_spec Proof_Context.read_class read_class_elems;
(* class establishment *)
--- a/src/Pure/Isar/expression.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/expression.ML Wed Mar 14 22:34:18 2012 +0100
@@ -8,9 +8,9 @@
sig
(* Locale expressions *)
datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
- type 'term expr = (string * ((string * bool) * 'term map)) list
- type expression_i = term expr * (binding * typ option * mixfix) list
- type expression = string expr * (binding * string option * mixfix) list
+ type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list
+ type expression_i = (string, term) expr * (binding * typ option * mixfix) list
+ type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
(* Processing of context statements *)
val cert_statement: Element.context_i list -> (term * term list) list list ->
@@ -41,7 +41,7 @@
(term list list * (string * morphism) list * morphism) * Proof.context
val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
(Attrib.binding * term) list -> theory -> Proof.state
- val sublocale_cmd: (local_theory -> local_theory) -> string -> expression ->
+ val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
(Attrib.binding * string) list -> theory -> Proof.state
val interpretation: expression_i -> (Attrib.binding * term) list ->
theory -> Proof.state
@@ -68,15 +68,15 @@
Positional of 'term option list |
Named of (string * 'term) list;
-type 'term expr = (string * ((string * bool) * 'term map)) list;
+type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list;
-type expression = string expr * (binding * string option * mixfix) list;
-type expression_i = term expr * (binding * typ option * mixfix) list;
+type expression_i = (string, term) expr * (binding * typ option * mixfix) list;
+type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list;
(** Internalise locale names in expr **)
-fun intern thy instances = map (apfst (Locale.intern thy)) instances;
+fun check_expr thy instances = map (apfst (Locale.check thy)) instances;
(** Parameters of expression **)
@@ -343,7 +343,8 @@
local
-fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
+fun prep_full_context_statement
+ parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
{strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
let
val thy = Proof_Context.theory_of ctxt1;
@@ -417,7 +418,7 @@
fun read_full_context_statement x =
prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
- parse_inst Proof_Context.read_vars intern x;
+ parse_inst Proof_Context.read_vars check_expr x;
end;
@@ -903,10 +904,10 @@
export thy) (deps ~~ witss))
end;
-fun gen_sublocale prep_expr intern parse_prop prep_attr
+fun gen_sublocale prep_expr prep_loc parse_prop prep_attr
before_exit raw_target expression equations thy =
let
- val target = intern thy raw_target;
+ val target = prep_loc thy raw_target;
val target_ctxt = Named_Target.init before_exit target thy;
val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
@@ -923,7 +924,7 @@
fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
fun sublocale_cmd x =
- gen_sublocale read_goal_expression Locale.intern Syntax.parse_prop Attrib.intern_src x;
+ gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;
end;
--- a/src/Pure/Isar/generic_target.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/generic_target.ML Wed Mar 14 22:34:18 2012 +0100
@@ -48,13 +48,11 @@
(* define *)
-fun define foundation ((b, mx), ((proto_b_def, atts), rhs)) lthy =
+fun define foundation ((b, mx), ((b_def, atts), rhs)) lthy =
let
val thy = Proof_Context.theory_of lthy;
val thy_ctxt = Proof_Context.init_global thy;
- val b_def = Thm.def_binding_optional b proto_b_def;
-
(*term and type parameters*)
val crhs = Thm.cterm_of thy rhs;
val ((defs, _), rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
@@ -202,7 +200,8 @@
val lhs = list_comb (const, type_params @ term_params);
val ((_, def), lthy3) = lthy2
|> Local_Theory.background_theory_result
- (Thm.add_def lthy2 false false (b_def, Logic.mk_equals (lhs, rhs)));
+ (Thm.add_def lthy2 false false
+ (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
in ((lhs, def), lthy3) end;
fun theory_notes kind global_facts lthy =
--- a/src/Pure/Isar/isar_cmd.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/isar_cmd.ML Wed Mar 14 22:34:18 2012 +0100
@@ -50,8 +50,8 @@
val print_configs: Toplevel.transition -> Toplevel.transition
val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
val print_locales: Toplevel.transition -> Toplevel.transition
- val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
- val print_registrations: string -> Toplevel.transition -> Toplevel.transition
+ val print_locale: bool * (xstring * Position.T) -> Toplevel.transition -> Toplevel.transition
+ val print_registrations: xstring * Position.T -> Toplevel.transition -> Toplevel.transition
val print_dependencies: bool * Expression.expression -> Toplevel.transition
-> Toplevel.transition
val print_attributes: Toplevel.transition -> Toplevel.transition
--- a/src/Pure/Isar/isar_syn.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/isar_syn.ML Wed Mar 14 22:34:18 2012 +0100
@@ -91,13 +91,13 @@
val _ =
Outer_Syntax.command "classes" "declare type classes" Keyword.thy_decl
(Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
- Parse.!!! (Parse.list1 Parse.xname)) [])
+ Parse.!!! (Parse.list1 Parse.class)) [])
>> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
val _ =
Outer_Syntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
- (Parse.and_list1 (Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
- |-- Parse.!!! Parse.xname))
+ (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
+ |-- Parse.!!! Parse.class))
>> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
val _ =
@@ -421,7 +421,7 @@
val _ =
Outer_Syntax.command "sublocale"
"prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
- (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
+ (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
parse_interpretation_arguments false
>> (fn (loc, (expr, equations)) =>
Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
@@ -445,7 +445,7 @@
(* classes *)
val class_val =
- Parse_Spec.class_expr --
+ Parse_Spec.class_expression --
Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
Scan.repeat1 Parse_Spec.context_element >> pair [];
@@ -458,7 +458,7 @@
val _ =
Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
- (Parse.xname >> Class_Declaration.subclass_cmd I);
+ (Parse.class >> Class_Declaration.subclass_cmd I);
val _ =
Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
@@ -468,8 +468,8 @@
val _ =
Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
- ((Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.xname)
- >> Class.classrel_cmd ||
+ ((Parse.class --
+ ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
Parse.multi_arity >> Class.instance_arity_cmd)
>> (Toplevel.print oo Toplevel.theory_to_proof) ||
Scan.succeed
@@ -831,12 +831,12 @@
val _ =
Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
- (opt_bang -- Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
+ (opt_bang -- Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
val _ =
Outer_Syntax.improper_command "print_interps"
"print interpretations of locale for this theory or proof context" Keyword.diag
- (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
+ (Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
val _ =
Outer_Syntax.improper_command "print_dependencies"
--- a/src/Pure/Isar/keyword.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/keyword.ML Wed Mar 14 22:34:18 2012 +0100
@@ -32,7 +32,6 @@
val prf_asm_goal: T
val prf_script: T
val kinds: string list
- val update_tags: string -> string list -> string list
val tag: string -> T -> T
val tags_of: T -> string list
val tag_theory: T -> T
@@ -108,9 +107,7 @@
(* tags *)
-fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
-
-fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
+fun tag t (Keyword (s, ts)) = Keyword (s, update (op =) t ts);
fun tags_of (Keyword (_, ts)) = ts;
val tag_theory = tag "theory";
--- a/src/Pure/Isar/locale.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/locale.ML Wed Mar 14 22:34:18 2012 +0100
@@ -79,8 +79,8 @@
(* Diagnostic *)
val all_locales: theory -> string list
val print_locales: theory -> unit
- val print_locale: theory -> bool -> xstring -> unit
- val print_registrations: Proof.context -> string -> unit
+ val print_locale: theory -> bool -> xstring * Position.T -> unit
+ val print_registrations: Proof.context -> xstring * Position.T -> unit
val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
val locale_deps: theory ->
{params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
@@ -618,7 +618,7 @@
fun print_locale thy show_facts raw_name =
let
- val name = intern thy raw_name;
+ val name = check thy raw_name;
val ctxt = init name thy;
fun cons_elem (elem as Notes _) = show_facts ? cons elem
| cons_elem elem = cons elem;
@@ -633,8 +633,7 @@
fun print_registrations ctxt raw_name =
let
val thy = Proof_Context.theory_of ctxt;
- val name = intern thy raw_name;
- val _ = the_locale thy name; (* error if locale unknown *)
+ val name = check thy raw_name;
in
(case registrations_of (Context.Proof ctxt) (* FIXME *) name of
[] => Pretty.str "no interpretations"
--- a/src/Pure/Isar/overloading.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/overloading.ML Wed Mar 14 22:34:18 2012 +0100
@@ -147,15 +147,16 @@
in
ctxt
|> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
- end
+ end;
fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
Local_Theory.background_theory_result
(Thm.add_def_global (not checked) true
- (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
+ (Thm.def_binding_optional (Binding.name v) b_def,
+ Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
##> Local_Theory.target synchronize_syntax
- #-> (fn (_, def) => pair (Const (c, U), def))
+ #-> (fn (_, def) => pair (Const (c, U), def));
fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
(case operation lthy b of
@@ -173,7 +174,7 @@
Pretty.block (Pretty.breaks
[Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
Pretty.str "::", Syntax.pretty_typ lthy ty]);
- in Pretty.str "overloading" :: map pr_operation overloading end;
+ in Pretty.command "overloading" :: map pr_operation overloading end;
fun conclude lthy =
let
--- a/src/Pure/Isar/parse.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/parse.ML Wed Mar 14 22:34:18 2012 +0100
@@ -69,7 +69,9 @@
val liberal_name: xstring parser
val parname: string parser
val parbinding: binding parser
+ val class: string parser
val sort: string parser
+ val type_const: string parser
val arity: (string * string list * string) parser
val multi_arity: (string list * string list * string) parser
val type_args: string list parser
@@ -93,7 +95,6 @@
val prop_group: string parser
val term: string parser
val prop: string parser
- val type_const: string parser
val const: string parser
val literal_fact: string parser
val propp: (string * string list) parser
@@ -257,14 +258,18 @@
val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
-(* sorts and arities *)
+(* type classes *)
+
+val class = group (fn () => "type class") (inner_syntax xname);
val sort = group (fn () => "sort") (inner_syntax xname);
-val arity = xname -- ($$$ "::" |-- !!!
+val type_const = inner_syntax (group (fn () => "type constructor") xname);
+
+val arity = type_const -- ($$$ "::" |-- !!!
(Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
-val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
+val multi_arity = and_list1 type_const -- ($$$ "::" |-- !!!
(Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
@@ -343,7 +348,6 @@
val term = inner_syntax term_group;
val prop = inner_syntax prop_group;
-val type_const = inner_syntax (group (fn () => "type constructor") xname);
val const = inner_syntax (group (fn () => "constant") xname);
val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
--- a/src/Pure/Isar/parse_spec.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/parse_spec.ML Wed Mar 14 22:34:18 2012 +0100
@@ -22,7 +22,7 @@
val locale_mixfix: mixfix parser
val locale_fixes: (binding * string option * mixfix) list parser
val locale_insts: (string option list * (Attrib.binding * string) list) parser
- val class_expr: string list parser
+ val class_expression: string list parser
val locale_expression: bool -> Expression.expression parser
val locale_keyword: string parser
val context_element: Element.context parser
@@ -125,11 +125,11 @@
Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
Parse.$$$ "defines" || Parse.$$$ "notes";
-val class_expr = plus1_unless locale_keyword Parse.xname;
+val class_expression = plus1_unless locale_keyword Parse.class;
fun locale_expression mandatory =
let
- val expr2 = Parse.xname;
+ val expr2 = Parse.position Parse.xname;
val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
val expr0 = plus1_unless locale_keyword expr1;
--- a/src/Pure/Isar/proof_context.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 14 22:34:18 2012 +0100
@@ -55,8 +55,6 @@
val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
val read_class: Proof.context -> xstring -> class
- val read_arity: Proof.context -> xstring * string list * string -> arity
- val cert_arity: Proof.context -> arity -> arity
val read_typ: Proof.context -> string -> typ
val read_typ_syntax: Proof.context -> string -> typ
val read_typ_abbrev: Proof.context -> string -> typ
@@ -70,6 +68,8 @@
val read_type_name_proper: Proof.context -> bool -> string -> typ
val read_const_proper: Proof.context -> bool -> string -> term
val read_const: Proof.context -> bool -> typ -> string -> term
+ val read_arity: Proof.context -> xstring * string list * string -> arity
+ val cert_arity: Proof.context -> arity -> arity
val allow_dummies: Proof.context -> Proof.context
val prepare_sorts: Proof.context -> typ list -> typ list
val check_tfree: Proof.context -> string * sort -> string * sort
@@ -367,22 +367,6 @@
in c end;
-(* type arities *)
-
-local
-
-fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
- let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
- in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
-
-in
-
-val read_arity = prep_arity intern_type Syntax.read_sort;
-val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
-
-end;
-
-
(* types *)
fun read_typ_mode mode ctxt s =
@@ -504,6 +488,23 @@
end;
+(* type arities *)
+
+local
+
+fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
+ let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
+ in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
+
+in
+
+val read_arity =
+ prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
+val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
+
+end;
+
+
(* skolem variables *)
fun intern_skolem ctxt x =
--- a/src/Pure/Thy/thy_output.ML Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Pure/Thy/thy_output.ML Wed Mar 14 22:34:18 2012 +0100
@@ -291,7 +291,7 @@
val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
val (tag, tags) = tag_stack;
- val tag' = try hd (fold Keyword.update_tags cmd_tags (the_list tag));
+ val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
val active_tag' =
if is_some tag' then tag'
@@ -586,7 +586,7 @@
basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity (Binding.name "class") (Scan.lift Args.name) pretty_class #>
+ basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
--- a/src/Tools/jEdit/src/document_model.scala Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/document_model.scala Wed Mar 14 22:34:18 2012 +0100
@@ -61,12 +61,15 @@
/* header */
def node_header(): Document.Node_Header =
- Isabelle.swing_buffer_lock(buffer) {
+ {
+ Swing_Thread.require()
+ Isabelle.buffer_lock(buffer) {
Exn.capture {
Isabelle.thy_load.check_header(name,
Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
}
}
+ }
/* perspective */
--- a/src/Tools/jEdit/src/document_view.scala Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/document_view.scala Wed Mar 14 22:34:18 2012 +0100
@@ -233,13 +233,15 @@
private val mouse_motion_listener = new MouseMotionAdapter {
override def mouseMoved(e: MouseEvent) {
+ Swing_Thread.assert()
+
control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
val x = e.getX()
val y = e.getY()
if (!model.buffer.isLoaded) exit_control()
else
- Isabelle.swing_buffer_lock(model.buffer) {
+ Isabelle.buffer_lock(model.buffer) {
val snapshot = update_snapshot()
if (control) init_popup(snapshot, x, y)
@@ -284,13 +286,15 @@
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
robust_body(()) {
+ Swing_Thread.assert()
+
val gutter = text_area.getGutter
val width = GutterOptionPane.getSelectionAreaWidth
val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
val FOLD_MARKER_SIZE = 12
if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
- Isabelle.swing_buffer_lock(model.buffer) {
+ Isabelle.buffer_lock(model.buffer) {
val snapshot = update_snapshot()
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
@@ -365,32 +369,36 @@
react {
case changed: Session.Commands_Changed =>
val buffer = model.buffer
- Isabelle.swing_buffer_lock(buffer) {
- val (updated, snapshot) = flush_snapshot()
+ Swing_Thread.later {
+ Isabelle.buffer_lock(buffer) {
+ if (model.buffer == text_area.getBuffer) {
+ val (updated, snapshot) = flush_snapshot()
- if (updated ||
- (changed.nodes.contains(model.name) &&
- changed.commands.exists(snapshot.node.commands.contains)))
- overview.delay_repaint(true)
+ if (updated ||
+ (changed.nodes.contains(model.name) &&
+ changed.commands.exists(snapshot.node.commands.contains)))
+ overview.delay_repaint(true)
- visible_range() match {
- case None =>
- case Some(visible) =>
- if (updated) invalidate_range(visible)
- else {
- val visible_cmds =
- snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
- if (visible_cmds.exists(changed.commands)) {
- for {
- line <- 0 until text_area.getVisibleLines
- val start = text_area.getScreenLineStartOffset(line) if start >= 0
- val end = text_area.getScreenLineEndOffset(line) if end >= 0
- val range = proper_line_range(start, end)
- val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
- if line_cmds.exists(changed.commands)
- } text_area.invalidateScreenLineRange(line, line)
- }
+ visible_range() match {
+ case Some(visible) =>
+ if (updated) invalidate_range(visible)
+ else {
+ val visible_cmds =
+ snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
+ if (visible_cmds.exists(changed.commands)) {
+ for {
+ line <- 0 until text_area.getVisibleLines
+ val start = text_area.getScreenLineStartOffset(line) if start >= 0
+ val end = text_area.getScreenLineEndOffset(line) if end >= 0
+ val range = proper_line_range(start, end)
+ val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+ if line_cmds.exists(changed.commands)
+ } text_area.invalidateScreenLineRange(line, line)
+ }
+ }
+ case None =>
}
+ }
}
}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Mar 14 22:34:18 2012 +0100
@@ -81,8 +81,10 @@
override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
{
+ Swing_Thread.assert()
+
val buffer = pane.getBuffer
- Isabelle.swing_buffer_lock(buffer) {
+ Isabelle.buffer_lock(buffer) {
Document_Model(buffer) match {
case None => null
case Some(model) =>
--- a/src/Tools/jEdit/src/plugin.scala Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/plugin.scala Wed Mar 14 22:34:18 2012 +0100
@@ -386,7 +386,7 @@
case phase: Session.Phase =>
phase match {
case Session.Failed =>
- Swing_Thread.now {
+ Swing_Thread.later {
val text = new scala.swing.TextArea(Isabelle.session.current_syslog())
text.editable = false
Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
@@ -445,7 +445,7 @@
}
case msg: PropertiesChanged =>
- Swing_Thread.now { Isabelle.setup_tooltips() }
+ Isabelle.setup_tooltips()
Isabelle.session.global_settings.event(Session.Global_Settings)
case _ =>
--- a/src/Tools/jEdit/src/protocol_dockable.scala Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Wed Mar 14 22:34:18 2012 +0100
@@ -29,10 +29,10 @@
loop {
react {
case input: Isabelle_Process.Input =>
- Swing_Thread.now { text_area.append(input.toString + "\n") }
+ Swing_Thread.later { text_area.append(input.toString + "\n") }
case output: Isabelle_Process.Output =>
- Swing_Thread.now { text_area.append(output.message.toString + "\n") }
+ Swing_Thread.later { text_area.append(output.message.toString + "\n") }
case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Wed Mar 14 22:34:18 2012 +0100
@@ -31,7 +31,7 @@
react {
case output: Isabelle_Process.Output =>
if (output.is_stdout || output.is_stderr)
- Swing_Thread.now { text_area.append(XML.content(output.message).mkString) }
+ Swing_Thread.later { text_area.append(XML.content(output.message).mkString) }
case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
}
--- a/src/Tools/jEdit/src/session_dockable.scala Wed Mar 14 17:19:30 2012 +0000
+++ b/src/Tools/jEdit/src/session_dockable.scala Wed Mar 14 22:34:18 2012 +0100
@@ -175,13 +175,13 @@
react {
case output: Isabelle_Process.Output =>
if (output.is_syslog)
- Swing_Thread.now {
+ Swing_Thread.later {
val text = Isabelle.session.current_syslog()
if (text != syslog.text) syslog.text = text
}
case phase: Session.Phase =>
- Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
+ Swing_Thread.later { session_phase.text = " " + phase.toString + " " }
case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))