src/Pure/PIDE/document.ML
changeset 40449 9c390868d255
parent 40398 cdda2847a91e
child 40481 da2c56aaaa68
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Nov 09 21:13:06 2010 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Nov 09 21:44:19 2010 +0100
     1.3 @@ -34,16 +34,7 @@
     1.4  type exec_id = id;
     1.5  
     1.6  val no_id = 0;
     1.7 -
     1.8 -local
     1.9 -  val id_count = Synchronized.var "id" 0;
    1.10 -in
    1.11 -  fun new_id () =
    1.12 -    Synchronized.change_result id_count
    1.13 -      (fn i =>
    1.14 -        let val i' = i + 1
    1.15 -        in (i', i') end);
    1.16 -end;
    1.17 +val new_id = Synchronized.counter ();
    1.18  
    1.19  val parse_id = Markup.parse_int;
    1.20  val print_id = Markup.print_int;