src/Pure/Tools/debugger.scala
author wenzelm
Wed Jul 29 13:34:04 2015 +0200 (2015-07-29)
changeset 60830 f56e189350b2
parent 60829 4b16b778ce0d
child 60834 781f1168d31e
permissions -rw-r--r--
separate channel for debugger output;
clarified thread name;
wenzelm@60749
     1
/*  Title:      Pure/Tools/debugger.scala
wenzelm@60749
     2
    Author:     Makarius
wenzelm@60749
     3
wenzelm@60749
     4
Interactive debugger for Isabelle/ML.
wenzelm@60749
     5
*/
wenzelm@60749
     6
wenzelm@60749
     7
package isabelle
wenzelm@60749
     8
wenzelm@60749
     9
wenzelm@60749
    10
object Debugger
wenzelm@60749
    11
{
wenzelm@60749
    12
  /* GUI interaction */
wenzelm@60749
    13
wenzelm@60749
    14
  case object Event
wenzelm@60749
    15
wenzelm@60749
    16
wenzelm@60749
    17
  /* manager thread */
wenzelm@60749
    18
wenzelm@60749
    19
  private lazy val manager: Consumer_Thread[Any] =
wenzelm@60749
    20
    Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)(
wenzelm@60749
    21
      consume = (arg: Any) =>
wenzelm@60749
    22
      {
wenzelm@60749
    23
        // FIXME
wenzelm@60749
    24
        true
wenzelm@60749
    25
      },
wenzelm@60749
    26
      finish = () =>
wenzelm@60749
    27
      {
wenzelm@60749
    28
        // FIXME
wenzelm@60749
    29
      }
wenzelm@60749
    30
    )
wenzelm@60749
    31
wenzelm@60749
    32
wenzelm@60749
    33
  /* protocol handler */
wenzelm@60749
    34
wenzelm@60749
    35
  class Handler extends Session.Protocol_Handler
wenzelm@60749
    36
  {
wenzelm@60830
    37
    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
wenzelm@60830
    38
    {
wenzelm@60830
    39
      msg.properties match {
wenzelm@60830
    40
        case Markup.Debugger_Output(name, serial) =>
wenzelm@60830
    41
          // FIXME
wenzelm@60830
    42
          Output.writeln("debugger_output " + name + " " + serial + "\n" + msg.text)
wenzelm@60830
    43
          true
wenzelm@60830
    44
        case _ => false
wenzelm@60830
    45
      }
wenzelm@60830
    46
    }
wenzelm@60830
    47
wenzelm@60749
    48
    override def stop(prover: Prover)
wenzelm@60749
    49
    {
wenzelm@60749
    50
      manager.shutdown()
wenzelm@60749
    51
    }
wenzelm@60749
    52
wenzelm@60830
    53
    val functions =
wenzelm@60830
    54
      Map(Markup.DEBUGGER_OUTPUT -> debugger_output _)
wenzelm@60749
    55
  }
wenzelm@60765
    56
wenzelm@60765
    57
wenzelm@60765
    58
  /* protocol commands */
wenzelm@60765
    59
wenzelm@60765
    60
  def init(session: Session): Unit =
wenzelm@60765
    61
    session.protocol_command("Debugger.init")
wenzelm@60765
    62
wenzelm@60829
    63
  def cancel(session: Session, name: String): Unit =
wenzelm@60829
    64
    session.protocol_command("Debugger.cancel", name)
wenzelm@60765
    65
wenzelm@60829
    66
  def input(session: Session, name: String, msg: String*): Unit =
wenzelm@60829
    67
    session.protocol_command("Debugger.input", (name :: msg.toList):_*)
wenzelm@60749
    68
}