lass das bang mal weg

Author: hargoniX

src/Lean/Server/RequestCancellation.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Lean.Server.ServerTask
-public import Init.System.Promise
 
 public section
 
@@ -38,10 +37,10 @@ def cancelByEdit (tk : RequestCancellationToken) : BaseIO Unit := do
   tk.editCancellationPromise.resolve ()
 
 def requestCancellationTask (tk : RequestCancellationToken): ServerTask Unit :=
-  tk.requestCancellationPromise.result!
+  tk.requestCancellationPromise.resultD ()
 
 def editCancellationTask (tk : RequestCancellationToken) : ServerTask Unit :=
-  tk.editCancellationPromise.result!
+  tk.editCancellationPromise.resultD ()
 
 def cancellationTasks (tk : RequestCancellationToken) : List (ServerTask Unit) :=
   [tk.requestCancellationTask, tk.editCancellationTask]

src/Lean/Server/ServerTask.lean

@@ -6,7 +6,7 @@ Authors: Marc Huisinga
 module
 
 prelude
-public import Init.System.IO
+public import Init.Task
 
 public section