src/Pure/Tools/debugger.scala
author wenzelm
Wed, 29 Jul 2015 11:41:26 +0200
changeset 60829 4b16b778ce0d
parent 60765 e43e71a75838
child 60830 f56e189350b2
permissions -rw-r--r--
clarified thread name;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/debugger.scala
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     3
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     4
Interactive debugger for Isabelle/ML.
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     5
*/
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     6
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     7
package isabelle
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     8
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     9
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    10
object Debugger
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    11
{
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    12
  /* GUI interaction */
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    13
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    14
  case object Event
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    15
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    16
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    17
  /* manager thread */
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    18
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    19
  private lazy val manager: Consumer_Thread[Any] =
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    20
    Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)(
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    21
      consume = (arg: Any) =>
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    22
      {
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    23
        // FIXME
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    24
        true
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    25
      },
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    26
      finish = () =>
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    27
      {
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    28
        // FIXME
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    29
      }
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    30
    )
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    31
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    32
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    33
  /* protocol handler */
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    34
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    35
  class Handler extends Session.Protocol_Handler
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    36
  {
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    37
    override def stop(prover: Prover)
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    38
    {
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    39
      manager.shutdown()
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    40
    }
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    41
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    42
    val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean]  // FIXME
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    43
  }
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    44
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    45
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    46
  /* protocol commands */
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    47
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    48
  def init(session: Session): Unit =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    49
    session.protocol_command("Debugger.init")
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    50
60829
4b16b778ce0d clarified thread name;
wenzelm
parents: 60765
diff changeset
    51
  def cancel(session: Session, name: String): Unit =
4b16b778ce0d clarified thread name;
wenzelm
parents: 60765
diff changeset
    52
    session.protocol_command("Debugger.cancel", name)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    53
60829
4b16b778ce0d clarified thread name;
wenzelm
parents: 60765
diff changeset
    54
  def input(session: Session, name: String, msg: String*): Unit =
4b16b778ce0d clarified thread name;
wenzelm
parents: 60765
diff changeset
    55
    session.protocol_command("Debugger.input", (name :: msg.toList):_*)
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    56
}