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;