src/Pure/Tools/debugger.scala
author wenzelm
Tue Jul 21 19:04:36 2015 +0200 (2015-07-21)
changeset 60765 e43e71a75838
parent 60749 f727b99faaf7
child 60829 4b16b778ce0d
permissions -rw-r--r--
support for ML debugger;
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@60749
    37
    override def stop(prover: Prover)
wenzelm@60749
    38
    {
wenzelm@60749
    39
      manager.shutdown()
wenzelm@60749
    40
    }
wenzelm@60749
    41
wenzelm@60749
    42
    val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean]  // FIXME
wenzelm@60749
    43
  }
wenzelm@60765
    44
wenzelm@60765
    45
wenzelm@60765
    46
  /* protocol commands */
wenzelm@60765
    47
wenzelm@60765
    48
  def init(session: Session): Unit =
wenzelm@60765
    49
    session.protocol_command("Debugger.init")
wenzelm@60765
    50
wenzelm@60765
    51
  def cancel(session: Session, id: String): Unit =
wenzelm@60765
    52
    session.protocol_command("Debugger.cancel", id)
wenzelm@60765
    53
wenzelm@60765
    54
  def input(session: Session, id: String, msg: String*): Unit =
wenzelm@60765
    55
    session.protocol_command("Debugger.input", (id :: msg.toList):_*)
wenzelm@60749
    56
}