--- a/NEWS Wed Jan 13 15:46:21 2016 +0100
+++ b/NEWS Wed Jan 13 15:59:37 2016 +0100
@@ -50,9 +50,6 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
-* Update to jedit-5.3.0, with improved GUI scaling and support of
-high-resolution displays (e.g. 4K).
-
* IDE support for the source-level debugger of Poly/ML, to work with
Isabelle/ML and official Standard ML. Configuration option "ML_debugger"
and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
@@ -114,6 +111,9 @@
works better with GUI scaling for very high-resolution displays (e.g.
4K). Moreover, it is generally more robust than "Nimbus".
+* Update to jedit-5.3.0, with improved GUI scaling and support of
+high-resolution displays (e.g. 4K).
+
* The main Isabelle executable is managed as single-instance Desktop
application uniformly on all platforms: Linux, Windows, Mac OS X.
--- a/src/HOL/Eisbach/match_method.ML Wed Jan 13 15:46:21 2016 +0100
+++ b/src/HOL/Eisbach/match_method.ML Wed Jan 13 15:59:37 2016 +0100
@@ -34,10 +34,6 @@
end;
-fun Item_Net_filter f net =
- fold (fn item => not (f item) ? Item_Net.remove item) (Item_Net.content net) net
-
-
datatype match_kind =
Match_Term of term Item_Net.T
| Match_Fact of thm Item_Net.T
@@ -686,14 +682,14 @@
val (_, after_prems) = focus_prems inner_ctxt;
val removed_prems =
- Item_Net_filter (null o Item_Net.lookup after_prems) before_prems
+ Item_Net.filter (null o Item_Net.lookup after_prems) before_prems
val removed_local_prems = Item_Net.content removed_prems
|> filter (fn (id, _) => member (op =) local_premids id)
|> map (fn (_, prem) => Thm.prop_of prem)
fun filter_removed_prems prems =
- Item_Net_filter (null o Item_Net.lookup removed_prems) prems;
+ Item_Net.filter (null o Item_Net.lookup removed_prems) prems;
val outer_ctxt' = outer_ctxt
|> Focus_Data.map (@{apply 3(1)} (apsnd filter_removed_prems));
--- a/src/Pure/item_net.ML Wed Jan 13 15:46:21 2016 +0100
+++ b/src/Pure/item_net.ML Wed Jan 13 15:59:37 2016 +0100
@@ -18,6 +18,7 @@
val merge: 'a T * 'a T -> 'a T
val remove: 'a -> 'a T -> 'a T
val update: 'a -> 'a T -> 'a T
+ val filter: ('a -> bool) -> 'a T -> 'a T
end;
structure Item_Net: ITEM_NET =
@@ -76,4 +77,7 @@
fun update x items = cons x (remove x items);
+fun filter pred items =
+ fold (fn x => not (pred x) ? remove x) (content items) items;
+
end;