--- a/NEWS Tue Jan 08 13:16:39 2013 +0100
+++ b/NEWS Tue Jan 08 19:02:12 2013 +0100
@@ -38,6 +38,13 @@
specifications: nesting of "context fixes ... context assumes ..."
and "class ... context ...".
+* Attribute "consumes" allows a negative value as well, which is
+interpreted relatively to the total number if premises of the rule in
+the target context. This form of declaration is stable when exported
+from a nested 'context' with additional assumptions. It is the
+preferred form for definitional packages, notably cases/rules produced
+in HOL/inductive and HOL/function.
+
* More informative error messages for Isar proof commands involving
lazy enumerations (method applications etc.).
--- a/src/Doc/IsarRef/Proof.thy Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Doc/IsarRef/Proof.thy Tue Jan 08 19:02:12 2013 +0100
@@ -1197,7 +1197,7 @@
;
@@{attribute params} ((@{syntax name} * ) + @'and')
;
- @@{attribute consumes} @{syntax nat}?
+ @@{attribute consumes} @{syntax int}?
"}
\begin{description}
@@ -1245,7 +1245,15 @@
\secref{sec:hol-inductive}). Rules without any @{attribute
consumes} declaration given are treated as if @{attribute
consumes}~@{text 0} had been specified.
-
+
+ A negative @{text n} is interpreted relatively to the total number
+ if premises of the rule in the target context. Thus its absolute
+ value specifies the remaining number of premises, after subtracting
+ the prefix of major premises as indicated above. This form of
+ declaration has the technical advantage of being stable under more
+ morphisms, notably those that export the result from a nested
+ @{command_ref context} with additional assumptions.
+
Note that explicit @{attribute consumes} declarations are only
rarely needed; this is already taken care of automatically by the
higher-level @{attribute cases}, @{attribute induct}, and
--- a/src/HOL/Nominal/nominal_inductive.ML Tue Jan 08 13:16:39 2013 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Tue Jan 08 19:02:12 2013 +0100
@@ -540,7 +540,7 @@
in
ctxt'' |>
- Proof.theorem NONE (fn thss => fn ctxt =>
+ Proof.theorem NONE (fn thss => fn ctxt => (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
let
val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
@@ -553,27 +553,27 @@
mk_ind_proof ctxt thss' |> Inductive.rulify;
val strong_cases = map (mk_cases_proof ##> Inductive.rulify)
(thsss ~~ elims ~~ cases_prems ~~ cases_prems');
+ val strong_induct_atts =
+ map (Attrib.internal o K)
+ [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
val strong_induct =
- if length names > 1 then
- (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
- else (strong_raw_induct RSN (2, rev_mp),
- [ind_case_names, Rule_Cases.consumes 1]);
+ if length names > 1 then strong_raw_induct
+ else strong_raw_induct RSN (2, rev_mp);
val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
- ((rec_qualified (Binding.name "strong_induct"),
- map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
+ ((rec_qualified (Binding.name "strong_induct"), strong_induct_atts), [strong_induct]);
val strong_inducts =
Project_Rule.projects ctxt (1 upto length names) strong_induct';
in
ctxt' |>
- Local_Theory.note
- ((rec_qualified (Binding.name "strong_inducts"),
- [Attrib.internal (K ind_case_names),
- Attrib.internal (K (Rule_Cases.consumes 1))]),
- strong_inducts) |> snd |>
+ Local_Theory.notes
+ [((rec_qualified (Binding.name "strong_inducts"), []),
+ strong_inducts |> map (fn th => ([th],
+ [Attrib.internal (K ind_case_names),
+ Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd |>
Local_Theory.notes (map (fn ((name, elim), (_, cases)) =>
((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
[Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
- Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
+ Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim)))]), [([elim], [])]))
(strong_cases ~~ induct_cases')) |> snd
end)
(map (map (rulify_term thy #> rpair [])) vc_compat)
--- a/src/HOL/Nominal/nominal_inductive2.ML Tue Jan 08 13:16:39 2013 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Jan 08 19:02:12 2013 +0100
@@ -443,7 +443,7 @@
in
ctxt'' |>
- Proof.theorem NONE (fn thss => fn ctxt =>
+ Proof.theorem NONE (fn thss => fn ctxt => (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
let
val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
@@ -454,28 +454,27 @@
val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
val strong_raw_induct =
mk_ind_proof ctxt thss' |> Inductive.rulify;
+ val strong_induct_atts =
+ map (Attrib.internal o K)
+ [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
val strong_induct =
- if length names > 1 then
- (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
- else (strong_raw_induct RSN (2, rev_mp),
- [ind_case_names, Rule_Cases.consumes 1]);
+ if length names > 1 then strong_raw_induct
+ else strong_raw_induct RSN (2, rev_mp);
val (induct_name, inducts_name) =
case alt_name of
NONE => (rec_qualified (Binding.name "strong_induct"),
rec_qualified (Binding.name "strong_inducts"))
| SOME s => (Binding.name s, Binding.name (s ^ "s"));
val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
- ((induct_name,
- map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
+ ((induct_name, strong_induct_atts), [strong_induct]);
val strong_inducts =
Project_Rule.projects ctxt' (1 upto length names) strong_induct'
in
ctxt' |>
- Local_Theory.note
- ((inducts_name,
+ Local_Theory.notes [((inducts_name, []),
+ strong_inducts |> map (fn th => ([th],
[Attrib.internal (K ind_case_names),
- Attrib.internal (K (Rule_Cases.consumes 1))]),
- strong_inducts) |> snd
+ Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd
end)
(map (map (rulify_term thy #> rpair [])) vc_compat)
end;
--- a/src/HOL/Tools/Function/function.ML Tue Jan 08 13:16:39 2013 +0100
+++ b/src/HOL/Tools/Function/function.ML Tue Jan 08 19:02:12 2013 +0100
@@ -105,14 +105,15 @@
val addsmps = add_simps fnames post sort_cont
- val (((psimps', pinducts'), (_, [termination'])), lthy) =
+ val (((psimps', [pinducts']), (_, [termination'])), lthy) =
lthy
|> addsmps (conceal_partial o Binding.qualify false "partial")
"psimps" conceal_partial psimp_attribs psimps
- ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
+ ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []),
+ simple_pinducts |> map (fn th => ([th],
[Attrib.internal (K (Rule_Cases.case_names cnames)),
- Attrib.internal (K (Rule_Cases.consumes 1)),
- Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
+ Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
+ Attrib.internal (K (Induct.induct_pred ""))])))]
||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
||> (snd o Local_Theory.note ((qualify "cases",
[Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
--- a/src/HOL/Tools/inductive.ML Tue Jan 08 13:16:39 2013 +0100
+++ b/src/HOL/Tools/inductive.ML Tue Jan 08 19:02:12 2013 +0100
@@ -860,12 +860,17 @@
val ind_case_names = Rule_Cases.case_names intr_names;
val induct =
if coind then
- (raw_induct, [Rule_Cases.case_names [rec_name],
+ (raw_induct,
+ [Rule_Cases.case_names [rec_name],
Rule_Cases.case_conclusion (rec_name, intr_names),
- Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)])
+ Rule_Cases.consumes (1 - Thm.nprems_of raw_induct),
+ Induct.coinduct_pred (hd cnames)])
else if no_ind orelse length cnames > 1 then
- (raw_induct, [ind_case_names, Rule_Cases.consumes 0])
- else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
+ (raw_induct,
+ [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))])
+ else
+ (raw_induct RSN (2, rev_mp),
+ [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))]);
val (intrs', lthy1) =
lthy |>
@@ -883,7 +888,7 @@
Local_Theory.note
((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
[Attrib.internal (K (Rule_Cases.case_names cases)),
- Attrib.internal (K (Rule_Cases.consumes 1)),
+ Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim))),
Attrib.internal (K (Rule_Cases.constraints k)),
Attrib.internal (K (Induct.cases_pred name)),
Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
@@ -906,7 +911,7 @@
Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
inducts |> map (fn (name, th) => ([th],
[Attrib.internal (K ind_case_names),
- Attrib.internal (K (Rule_Cases.consumes 1)),
+ Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
end;
in (intrs', elims', eqs', induct', inducts, lthy4) end;
--- a/src/HOL/Tools/inductive_set.ML Tue Jan 08 13:16:39 2013 +0100
+++ b/src/HOL/Tools/inductive_set.ML Tue Jan 08 19:02:12 2013 +0100
@@ -156,7 +156,7 @@
(* where s and p are parameters *)
(***********************************************************)
-structure PredSetConvData = Generic_Data
+structure Data = Generic_Data
(
type T =
{(* rules for converting predicates to sets *)
@@ -269,13 +269,15 @@
(**** declare rules for converting predicates to sets ****)
-fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
- case prop_of thm of
+exception Malformed of string;
+
+fun add context thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
+ (case prop_of thm of
Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ lhs $ rhs) =>
(case body_type T of
@{typ bool} =>
let
- val thy = Context.theory_of ctxt;
+ val thy = Context.theory_of context;
fun factors_of t fs = case strip_abs_body t of
Const (@{const_name Set.member}, _) $ u $ S =>
if is_Free S orelse is_Var S then
@@ -289,7 +291,7 @@
Abs _ => (case strip_abs_body rhs of
Const (@{const_name Set.member}, _) $ u $ S =>
(strip_comb S, SOME (HOLogic.flat_tuple_paths u))
- | _ => error "member symbol on right-hand side expected")
+ | _ => raise Malformed "member symbol on right-hand side expected")
| _ => (strip_comb rhs, NONE))
in
case (name_type_of h, name_type_of h') of
@@ -308,13 +310,16 @@
(T', (map (AList.lookup op = fs) ts', fs'))) set_arities,
pred_arities = Symtab.insert_list op = (s,
(T, (pfs, fs'))) pred_arities}
- | _ => error "set / predicate constant expected"
+ | _ => raise Malformed "set / predicate constant expected"
end
- | _ => error "equation between predicates expected")
- | _ => error "equation expected";
+ | _ => raise Malformed "equation between predicates expected")
+ | _ => raise Malformed "equation expected")
+ handle Malformed msg =>
+ (warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
+ "\n" ^ Display.string_of_thm (Context.proof_of context) thm); tab);
val pred_set_conv_att = Thm.declaration_attribute
- (fn thm => fn ctxt => PredSetConvData.map (add ctxt thm) ctxt);
+ (fn thm => fn ctxt => Data.map (add ctxt thm) ctxt);
(**** convert theorem in set notation to predicate notation ****)
@@ -340,7 +345,7 @@
let
val thy = Context.theory_of ctxt;
val {to_pred_simps, set_arities, pred_arities, ...} =
- fold (add ctxt) thms (PredSetConvData.get ctxt);
+ fold (add ctxt) thms (Data.get ctxt);
val fs = filter (is_Var o fst)
(infer_arities thy set_arities (NONE, prop_of thm) []);
(* instantiate each set parameter with {(x, y). p x y} *)
@@ -363,7 +368,7 @@
let
val thy = Context.theory_of ctxt;
val {to_set_simps, pred_arities, ...} =
- fold (add ctxt) thms (PredSetConvData.get ctxt);
+ fold (add ctxt) thms (Data.get ctxt);
val fs = filter (is_Var o fst)
(infer_arities thy pred_arities (NONE, prop_of thm) []);
(* instantiate each predicate parameter with %x y. (x, y) : s *)
@@ -397,7 +402,7 @@
fun codegen_preproc thy =
let
val {to_pred_simps, set_arities, pred_arities, ...} =
- PredSetConvData.get (Context.Theory thy);
+ Data.get (Context.Theory thy);
fun preproc thm =
if exists_Const (fn (s, _) => case Symtab.lookup set_arities s of
NONE => false
@@ -422,7 +427,7 @@
let
val thy = Proof_Context.theory_of lthy;
val {set_arities, pred_arities, to_pred_simps, ...} =
- PredSetConvData.get (Context.Proof lthy);
+ Data.get (Context.Proof lthy);
fun infer (Abs (_, _, t)) = infer t
| infer (Const (@{const_name Set.member}, _) $ t $ u) =
infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
--- a/src/Pure/Isar/attrib.ML Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Jan 08 19:02:12 2013 +0100
@@ -391,7 +391,7 @@
"rename bound variables in abstractions" #>
setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
setup (Binding.name "folded") folded "folded definitions" #>
- setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
+ setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
"number of consumed facts" #>
setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
"number of equality constraints" #>
--- a/src/Pure/axclass.ML Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Pure/axclass.ML Tue Jan 08 19:02:12 2013 +0100
@@ -107,9 +107,8 @@
params2 params1;
(*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
- val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
- val proven_arities' =
- Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);
+ val proven_classrels' = Symreltab.merge (K true) (proven_classrels1, proven_classrels2);
+ val proven_arities' = Symtab.merge_list (eq_fst op =) (proven_arities1, proven_arities2);
val inst_params' =
(Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
@@ -188,11 +187,7 @@
let
fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) =
let
- val proven = is_classrel thy1;
- val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
- val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs [];
-
- fun complete c1 c2 (finished2, thy2) =
+ fun compl c1 c2 (finished2, thy2) =
if is_classrel thy2 (c1, c2) then (finished2, thy2)
else
(false,
@@ -201,12 +196,17 @@
(the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
|> Drule.instantiate' [SOME (ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
|> Thm.close_derivation));
- in fold_product complete preds succs (finished1, thy1) end;
- val (finished', thy') =
- Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy);
+ val proven = is_classrel thy1;
+ val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
+ val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs [];
+ in
+ fold_product compl preds succs (finished1, thy1)
+ end;
in
- if finished' then NONE else SOME thy'
+ (case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of
+ (true, _) => NONE
+ | (_, thy') => SOME thy')
end;
@@ -257,7 +257,8 @@
let
val arities = proven_arities_of thy;
val (finished, arities') =
- Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars) arities (true, arities);
+ Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars)
+ arities (true, arities);
in
if finished then NONE
else SOME (map_proven_arities (K arities') thy)
@@ -388,8 +389,9 @@
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
val rel = Logic.dest_classrel prop handle TERM _ => err ();
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
- val (th', thy') = Global_Theory.store_thm
- (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
+ val (th', thy') =
+ Global_Theory.store_thm
+ (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
val th'' = th'
|> Thm.unconstrainT
|> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
@@ -408,8 +410,9 @@
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
- val (th', thy') = Global_Theory.store_thm
- (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
+ val (th', thy') =
+ Global_Theory.store_thm
+ (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
val args = Name.invent_names Name.context Name.aT Ss;
val T = Type (t, map TFree args);
--- a/src/Pure/consts.ML Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Pure/consts.ML Tue Jan 08 19:02:12 2013 +0100
@@ -318,7 +318,7 @@
Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
let
val decls' = Name_Space.merge_tables (decls1, decls2);
- val constraints' = Symtab.join (K fst) (constraints1, constraints2);
+ val constraints' = Symtab.merge (K true) (constraints1, constraints2);
val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
in make_consts (decls', constraints', rev_abbrevs') end;
--- a/src/Tools/Code/code_target.ML Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Tools/Code/code_target.ML Tue Jan 08 19:02:12 2013 +0100
@@ -110,7 +110,7 @@
fun merge_symbol_syntax_data
(Symbol_Syntax_Data { class = class1, instance = instance1, tyco = tyco1, const = const1 },
Symbol_Syntax_Data { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
- make_symbol_syntax_data (
+ make_symbol_syntax_data ( (* FIXME proper merge order!? prefer fst!? *)
(Symtab.join (K snd) (class1, class2),
Symreltab.join (K snd) (instance1, instance2)),
(Symtab.join (K snd) (tyco1, tyco2),
@@ -158,7 +158,9 @@
module_alias = module_alias2, symbol_syntax = symbol_syntax2 }) =
if serial1 = serial2 orelse not strict then
make_target ((serial1, description),
- ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
+ ((merge (op =) (reserved1, reserved2),
+ (* FIXME proper merge order!? prefer fst!? *)
+ Symtab.join (K snd) (includes1, includes2)),
(Symtab.join (K snd) (module_alias1, module_alias2),
merge_symbol_syntax_data (symbol_syntax1, symbol_syntax2))
))
--- a/src/Tools/adhoc_overloading.ML Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Tools/adhoc_overloading.ML Tue Jan 08 19:02:12 2013 +0100
@@ -53,7 +53,7 @@
fun merge
({internalize = int1, externalize = ext1},
{internalize = int2, externalize = ext2}) : T =
- {internalize = Symtab.join (K (Library.merge (op =))) (int1, int2),
+ {internalize = Symtab.merge_list (op =) (int1, int2),
externalize = Symtab.join merge_ext (ext1, ext2)};
);
--- a/src/Tools/jEdit/src/document_view.scala Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Tue Jan 08 19:02:12 2013 +0100
@@ -189,24 +189,24 @@
changed.commands.exists(snapshot.node.commands.contains)))
Swing_Thread.later { overview.delay_repaint.invoke() }
- JEdit_Lib.visible_range(text_area) match {
- case Some(visible) =>
- if (changed.assignment) JEdit_Lib.invalidate_range(text_area, 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
- start = text_area.getScreenLineStartOffset(line) if start >= 0
- end = text_area.getScreenLineEndOffset(line) if end >= 0
- range = Text.Range(start, end)
- line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
- if line_cmds.exists(changed.commands)
- } text_area.invalidateScreenLineRange(line, line)
- }
+ val visible_lines = text_area.getVisibleLines
+ if (visible_lines > 0) {
+ if (changed.assignment) text_area.invalidateScreenLineRange(0, visible_lines)
+ else {
+ val visible_range = JEdit_Lib.visible_range(text_area).get
+ val visible_cmds =
+ snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+ if (visible_cmds.exists(changed.commands)) {
+ for {
+ line <- 0 until visible_lines
+ start = text_area.getScreenLineStartOffset(line) if start >= 0
+ end = text_area.getScreenLineEndOffset(line) if end >= 0
+ range = Text.Range(start, end)
+ 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.scala Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Jan 08 19:02:12 2013 +0100
@@ -55,7 +55,7 @@
def change_font_size(view: View, change: Int => Int)
{
- val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
+ val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
jEdit.setIntegerProperty("view.fontsize", size)
jEdit.propertiesChanged()
jEdit.saveSettings()
--- a/src/Tools/jEdit/src/output_dockable.scala Tue Jan 08 13:16:39 2013 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Tue Jan 08 19:02:12 2013 +0100
@@ -93,7 +93,8 @@
case _: Session.Global_Options =>
Swing_Thread.later { handle_resize() }
case changed: Session.Commands_Changed =>
- Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
+ val restriction = if (changed.assignment) None else Some(changed.commands)
+ Swing_Thread.later { handle_update(do_update, restriction) }
case Session.Caret_Focus =>
Swing_Thread.later { handle_update(do_update, None) }
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)