src/Pure/PIDE/document.ML
changeset 44247 270366301bd7
parent 44226 1ea760da0f2d
child 44270 3eaad39e520c
equal deleted inserted replaced
44246:380a4677c55d 44247:270366301bd7
   370                       val node' = node
   370                       val node' = node
   371                         |> fold update_entry assigns
   371                         |> fold update_entry assigns
   372                         |> set_result result;
   372                         |> set_result result;
   373                     in ((assigns, execs, [(name, node')]), node') end)
   373                     in ((assigns, execs, [(name, node')]), node') end)
   374               end))
   374               end))
   375       |> Future.join_results |> Exn.release_all |> map #1;
   375       |> Future.join_results |> Par_Exn.release_all |> map #1;
   376 
   376 
   377     val state' = state
   377     val state' = state
   378       |> fold (fold define_exec o #2) updates
   378       |> fold (fold define_exec o #2) updates
   379       |> define_version new_id (fold (fold put_node o #3) updates new_version);
   379       |> define_version new_id (fold (fold put_node o #3) updates new_version);
   380 
   380