src/Pure/Tools/debugger.scala
author wenzelm
Thu Aug 06 17:40:05 2015 +0200 (2015-08-06)
changeset 60856 eb21ae05ec43
parent 60854 8f45dd297357
child 60857 4c18d8e4fe14
permissions -rw-r--r--
clarified thread state;
support for eval operation;
     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   /* global state */
    13 
    14   sealed case class Debug_State(
    15     pos: Position.T,
    16     function: String)
    17 
    18   sealed case class State(
    19     session: Session = new Session(Resources.empty),
    20     threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
    21     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
    22   {
    23     def set_session(new_session: Session): State =
    24       copy(session = new_session)
    25 
    26     def get_thread(thread_name: String): List[Debug_State] =
    27       threads.getOrElse(thread_name, Nil)
    28 
    29     def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
    30       copy(threads = threads + (thread_name -> debug_states))
    31 
    32     def get_output(thread_name: String): Command.Results =
    33       output.getOrElse(thread_name, Command.Results.empty)
    34 
    35     def add_output(thread_name: String, entry: Command.Results.Entry): State =
    36       copy(output = output + (thread_name -> (get_output(thread_name) + entry)))
    37 
    38     def clear_output(thread_name: String): State =
    39       copy(output = output - thread_name)
    40 
    41     def purge(thread_name: String): State =
    42       if (get_thread(thread_name).isEmpty)
    43         copy(threads = threads - thread_name, output = output - thread_name)
    44       else this
    45   }
    46 
    47   private val global_state = Synchronized(State())
    48   def current_state(): State = global_state.value
    49 
    50 
    51   /* protocol handler */
    52 
    53   sealed case class Update(thread_names: Set[String])
    54 
    55   class Handler extends Session.Protocol_Handler
    56   {
    57     private var updated = Set.empty[String]
    58     private val delay_update =
    59       Simple_Thread.delay_first(current_state().session.output_delay) {
    60         current_state().session.debugger_updates.post(Update(updated))
    61         updated = Set.empty
    62       }
    63     private def update(name: String)
    64     {
    65       updated += name
    66       delay_update.invoke()
    67     }
    68 
    69     private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    70     {
    71       msg.properties match {
    72         case Markup.Debugger_State(thread_name) =>
    73           val msg_body = YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes))
    74           val debug_states =
    75           {
    76             import XML.Decode._
    77             list(pair(properties, Symbol.decode_string))(msg_body).map({
    78               case (pos, function) => Debug_State(pos, function)
    79             })
    80           }
    81           global_state.change(_.update_thread(thread_name, debug_states))
    82           update(thread_name)
    83           true
    84         case _ => false
    85       }
    86     }
    87 
    88     private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    89     {
    90       msg.properties match {
    91         case Markup.Debugger_Output(thread_name) =>
    92           val msg_body =
    93             prover.xml_cache.body(
    94               YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes)))
    95           msg_body match {
    96             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
    97               val message = XML.Elem(Markup(Markup.message(name), props), body)
    98               global_state.change(_.add_output(thread_name, i -> message))
    99               update(thread_name)
   100               true
   101             case _ => false
   102           }
   103         case _ => false
   104       }
   105     }
   106 
   107     val functions =
   108       Map(
   109         Markup.DEBUGGER_STATE -> debugger_state _,
   110         Markup.DEBUGGER_OUTPUT -> debugger_output _)
   111   }
   112 
   113 
   114   /* protocol commands */
   115 
   116   def init(session: Session)
   117   {
   118     global_state.change(_.set_session(session))
   119     current_state().session.protocol_command("Debugger.init")
   120   }
   121 
   122   def cancel(thread_name: String): Unit =
   123     current_state().session.protocol_command("Debugger.cancel", thread_name)
   124 
   125   def input(thread_name: String, msg: String*): Unit =
   126     current_state().session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
   127 
   128   def continue(thread_name: String): Unit = input(thread_name, "continue")
   129 
   130   def eval(thread_name: String, opt_index: Option[Int],
   131       language: String, context: String, expression: String): Unit =
   132   {
   133     val index = opt_index.map(_.toString).getOrElse("")
   134     input(thread_name, "eval", index, language, context, expression)
   135   }
   136 }