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;
     1 /*  Title:      Pure/Tools/debugger.scala
     2     Author:     Makarius
     3 
     4 Interactive debugger for Isabelle/ML.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Debugger
    11 {
    12   /* GUI interaction */
    13 
    14   case object Event
    15 
    16 
    17   /* manager thread */
    18 
    19   private lazy val manager: Consumer_Thread[Any] =
    20     Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)(
    21       consume = (arg: Any) =>
    22       {
    23         // FIXME
    24         true
    25       },
    26       finish = () =>
    27       {
    28         // FIXME
    29       }
    30     )
    31 
    32 
    33   /* protocol handler */
    34 
    35   class Handler extends Session.Protocol_Handler
    36   {
    37     override def stop(prover: Prover)
    38     {
    39       manager.shutdown()
    40     }
    41 
    42     val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean]  // FIXME
    43   }
    44 
    45 
    46   /* protocol commands */
    47 
    48   def init(session: Session): Unit =
    49     session.protocol_command("Debugger.init")
    50 
    51   def cancel(session: Session, id: String): Unit =
    52     session.protocol_command("Debugger.cancel", id)
    53 
    54   def input(session: Session, id: String, msg: String*): Unit =
    55     session.protocol_command("Debugger.input", (id :: msg.toList):_*)
    56 }