--- a/src/Pure/Tools/debugger.scala Tue Jul 28 23:29:13 2015 +0200
+++ b/src/Pure/Tools/debugger.scala Wed Jul 29 11:41:26 2015 +0200
@@ -48,9 +48,9 @@
def init(session: Session): Unit =
session.protocol_command("Debugger.init")
- def cancel(session: Session, id: String): Unit =
- session.protocol_command("Debugger.cancel", id)
+ def cancel(session: Session, name: String): Unit =
+ session.protocol_command("Debugger.cancel", name)
- def input(session: Session, id: String, msg: String*): Unit =
- session.protocol_command("Debugger.input", (id :: msg.toList):_*)
+ def input(session: Session, name: String, msg: String*): Unit =
+ session.protocol_command("Debugger.input", (name :: msg.toList):_*)
}