src/Pure/General/position.ML
changeset 33097 9d501e11084a
parent 32573 62b5b538408d
child 37043 f8e24980af05
--- a/src/Pure/General/position.ML	Sat Oct 24 20:54:08 2009 +0200
+++ b/src/Pure/General/position.ML	Sat Oct 24 21:30:33 2009 +0200
@@ -37,6 +37,7 @@
   val range: T -> T -> range
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
+  val default: T -> T
 end;
 
 structure Position: POSITION =
@@ -178,4 +179,8 @@
 
 end;
 
+fun default pos =
+  if pos = none then thread_data ()
+  else pos;
+
 end;