equal
deleted
inserted
replaced
47 |
47 |
48 fun dialog () = |
48 fun dialog () = |
49 let |
49 let |
50 val i = serial (); |
50 val i = serial (); |
51 fun abort () = Synchronized.change dialogs (Inttab.delete_safe i); |
51 fun abort () = Synchronized.change dialogs (Inttab.delete_safe i); |
52 val promise = Future.promise abort : string future; |
52 val promise = Future.promise_name "dialog" abort : string future; |
53 val _ = Synchronized.change dialogs (Inttab.update_new (i, promise)); |
53 val _ = Synchronized.change dialogs (Inttab.update_new (i, promise)); |
54 fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result); |
54 fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result); |
55 in (result_markup, promise) end; |
55 in (result_markup, promise) end; |
56 |
56 |
57 fun dialog_text () = |
57 fun dialog_text () = |