src/Pure/PIDE/document.ML
changeset 44301 65f60d9ac4bf
parent 44300 349cc426d929
child 44302 0a1934c5c104
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 19 16:13:26 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 19 17:39:37 2011 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    type state
     1.5    val init_state: state
     1.6    val join_commands: state -> unit
     1.7 -  val cancel_execution: state -> unit future
     1.8 +  val cancel_execution: state -> Future.task list
     1.9    val define_command: command_id -> string -> state -> state
    1.10    val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
    1.11    val execute: version_id -> state -> state