# HG changeset patch
# User wenzelm
# Date 1314386878 -7200
# Node ID 383a5b9efbd02da2454c289acebf3b5b38a6ebe1
# Parent  c7225307acf23e9588994234212111ed65e81966
tuned signature -- iterate subsumes both fold and get_first;

diff -r c7225307acf2 -r 383a5b9efbd0 src/Pure/General/linear_set.ML
--- a/src/Pure/General/linear_set.ML	Fri Aug 26 21:18:42 2011 +0200
+++ b/src/Pure/General/linear_set.ML	Fri Aug 26 21:27:58 2011 +0200
@@ -16,10 +16,8 @@
   val defined: 'a T -> key -> bool
   val lookup: 'a T -> key -> ('a * key option) option
   val update: key * 'a -> 'a T -> 'a T
-  val fold: key option ->
+  val iterate: key option ->
     ((key option * key) * 'a -> 'b -> 'b option) -> 'a T -> 'b -> 'b
-  val get_first: key option ->
-    ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option
   val get_after: 'a T -> key option -> key option
   val insert_after: key option -> key * 'a -> 'a T -> 'a T
   val delete_after: key option -> 'a T -> 'a T
@@ -81,7 +79,7 @@
 fun optional_start set NONE = start_of set
   | optional_start _ some = some;
 
-fun fold opt_start f set =
+fun iterate opt_start f set =
   let
     val entries = entries_of set;
     fun apply _ NONE y = y
@@ -96,17 +94,6 @@
           end;
   in apply NONE (optional_start set opt_start) end;
 
-fun get_first opt_start P set =
-  let
-    val entries = entries_of set;
-    fun first _ NONE = NONE
-      | first prev (SOME key) =
-          let
-            val (x, next) = the_entry entries key;
-            val item = ((prev, key), x);
-          in if P item then SOME item else first (SOME key) next end;
-  in first NONE (optional_start set opt_start) end;
-
 
 (* relative addressing *)
 
diff -r c7225307acf2 -r 383a5b9efbd0 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 26 21:18:42 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 26 21:27:58 2011 +0200
@@ -112,7 +112,7 @@
 fun map_entries f =
   map_node (fn (touched, header, perspective, entries, last_exec, result) =>
     (touched, header, perspective, f entries, last_exec, result));
-fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
+fun iterate_entries start f (Node {entries, ...}) = Entries.iterate start f entries;
 
 fun get_last_exec (Node {last_exec, ...}) = last_exec;
 fun set_last_exec last_exec =
@@ -387,7 +387,7 @@
       else
         let val found' = is_none exec orelse exec <> lookup_entry node0 id
         in SOME (found', (prev, visible andalso prev <> last_visible)) end;
-  in #2 (fold_entries NONE get_common node (false, (NONE, true))) end;
+  in #2 (iterate_entries NONE get_common node (false, (NONE, true))) end;
 
 fun new_exec state init command_id' (execs, exec) =
   let
@@ -448,13 +448,13 @@
 
                     val (execs, exec) = ([], common_exec) |>
                       visible ?
-                        fold_entries (after_entry node common)
+                        iterate_entries (after_entry node common)
                           (fn ((prev, id), _) => fn res =>
                             if prev = last_visible then NONE
                             else SOME (new_exec state init id res)) node;
 
                     val no_execs =
-                      fold_entries (after_entry node0 common)
+                      iterate_entries (after_entry node0 common)
                         (fn ((_, id0), exec0) => fn res =>
                           if is_none exec0 then NONE
                           else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
@@ -514,7 +514,7 @@
             (singleton o Future.forks)
               {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
                 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
-              (fold_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
+              (iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
 
     in (versions, commands, execs, execution) end);