src/Pure/Tools/debugger.scala

separate channel for debugger output;
clarified thread name;

/*  Title:      Pure/Tools/debugger.scala
    Author:     Makarius

Interactive debugger for Isabelle/ML.
*/

package isabelle


object Debugger
{
  /* GUI interaction */

  case object Event


  /* manager thread */

  private lazy val manager: Consumer_Thread[Any] =
    Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)(
      consume = (arg: Any) =>
      {
        // FIXME
        true
      },
      finish = () =>
      {
        // FIXME
      }
    )


  /* protocol handler */

  class Handler extends Session.Protocol_Handler
  {
    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    {
      msg.properties match {
        case Markup.Debugger_Output(name, serial) =>
          // FIXME
          Output.writeln("debugger_output " + name + " " + serial + "\n" + msg.text)
          true
        case _ => false
      }
    }

    override def stop(prover: Prover)
    {
      manager.shutdown()
    }

    val functions =
      Map(Markup.DEBUGGER_OUTPUT -> debugger_output _)
  }


  /* protocol commands */

  def init(session: Session): Unit =
    session.protocol_command("Debugger.init")

  def cancel(session: Session, name: String): Unit =
    session.protocol_command("Debugger.cancel", name)

  def input(session: Session, name: String, msg: String*): Unit =
    session.protocol_command("Debugger.input", (name :: msg.toList):_*)
}