# HG changeset patch
# User wenzelm
# Date 1201215073 -3600
# Node ID 682e84b60e5c8f8c747fc13f63c9847814bf4d0b
# Parent  03937086b1fe454bc09714d1ad0bc1cd8a27e27f
added setmp_thread_data_seq;

diff -r 03937086b1fe -r 682e84b60e5c src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Thu Jan 24 23:51:11 2008 +0100
+++ b/src/Pure/General/position.ML	Thu Jan 24 23:51:13 2008 +0100
@@ -19,6 +19,7 @@
   val properties_of: T -> Markup.property list
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
+  val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
   val str_of: T -> string
 end;
 
@@ -64,6 +65,9 @@
 fun thread_data () = the_default none (Multithreading.get_data tag);
 fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos;
 
+fun setmp_thread_data_seq pos f seq =
+  setmp_thread_data pos f seq |> Seq.wrap (fn pull => setmp_thread_data pos pull ());
+
 end;