src/Pure/Tools/debugger.scala
author wenzelm
Mon Aug 10 16:05:41 2015 +0200 (2015-08-10)
changeset 60876 52edced9cce5
parent 60875 ee23c1d21ac3
child 60878 1f0d2bbcf38b
permissions -rw-r--r--
rendering for debugger/breakpoint active state;
     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     active: Int = 0,
    21     active_breakpoints: Set[Long] = Set.empty,
    22     focus: Option[Position.T] = None,  // position of active GUI component
    23     threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
    24     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
    25   {
    26     def set_session(new_session: Session): State =
    27       copy(session = new_session)
    28 
    29     def inc_active: State = copy(active = active + 1)
    30     def dec_active: State = copy(active = active - 1)
    31 
    32     def toggle_breakpoint(serial: Long): State =
    33     {
    34       val active_breakpoints1 =
    35         if (active_breakpoints(serial)) active_breakpoints - serial
    36       else active_breakpoints + serial
    37       copy(active_breakpoints = active_breakpoints1)
    38     }
    39 
    40     def set_focus(new_focus: Option[Position.T]): State =
    41       copy(focus = new_focus)
    42 
    43     def get_thread(thread_name: String): List[Debug_State] =
    44       threads.getOrElse(thread_name, Nil)
    45 
    46     def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
    47       copy(threads = threads + (thread_name -> debug_states))
    48 
    49     def get_output(thread_name: String): Command.Results =
    50       output.getOrElse(thread_name, Command.Results.empty)
    51 
    52     def add_output(thread_name: String, entry: Command.Results.Entry): State =
    53       copy(output = output + (thread_name -> (get_output(thread_name) + entry)))
    54 
    55     def clear_output(thread_name: String): State =
    56       copy(output = output - thread_name)
    57 
    58     def purge(thread_name: String): State =
    59       if (get_thread(thread_name).isEmpty)
    60         copy(threads = threads - thread_name, output = output - thread_name)
    61       else this
    62   }
    63 
    64   private val global_state = Synchronized(State())
    65   def current_state(): State = global_state.value
    66 
    67 
    68   /* protocol handler */
    69 
    70   sealed case class Update(thread_names: Set[String])
    71 
    72   class Handler extends Session.Protocol_Handler
    73   {
    74     private var updated = Set.empty[String]
    75     private val delay_update =
    76       Simple_Thread.delay_first(current_state().session.output_delay) {
    77         current_state().session.debugger_updates.post(Update(updated))
    78         updated = Set.empty
    79       }
    80     private def update(name: String)
    81     {
    82       updated += name
    83       delay_update.invoke()
    84     }
    85 
    86     private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    87     {
    88       msg.properties match {
    89         case Markup.Debugger_State(thread_name) =>
    90           val msg_body =
    91             YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes)))
    92           val debug_states =
    93           {
    94             import XML.Decode._
    95             list(pair(properties, Symbol.decode_string))(msg_body).map({
    96               case (pos, function) => Debug_State(pos, function)
    97             })
    98           }
    99           global_state.change(_.update_thread(thread_name, debug_states))
   100           update(thread_name)
   101           true
   102         case _ => false
   103       }
   104     }
   105 
   106     private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
   107     {
   108       msg.properties match {
   109         case Markup.Debugger_Output(thread_name) =>
   110           val msg_body =
   111             prover.xml_cache.body(
   112               YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))))
   113           msg_body match {
   114             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
   115               val message = XML.Elem(Markup(Markup.message(name), props), body)
   116               global_state.change(_.add_output(thread_name, i -> message))
   117               update(thread_name)
   118               true
   119             case _ => false
   120           }
   121         case _ => false
   122       }
   123     }
   124 
   125     val functions =
   126       Map(
   127         Markup.DEBUGGER_STATE -> debugger_state _,
   128         Markup.DEBUGGER_OUTPUT -> debugger_output _)
   129   }
   130 
   131 
   132   /* protocol commands */
   133 
   134   def init(session: Session)
   135   {
   136     global_state.change(_.set_session(session))
   137     current_state().session.protocol_command("Debugger.init")
   138   }
   139 
   140   def is_active(): Boolean = current_state().active > 0
   141   def inc_active(): Unit = global_state.change(_.inc_active)
   142   def dec_active(): Unit = global_state.change(_.dec_active)
   143 
   144   def breakpoint_active(serial: Long): Option[Boolean] =
   145   {
   146     val state = current_state()
   147     if (state.active > 0) Some(state.active_breakpoints(serial)) else None
   148   }
   149 
   150   def toggle_breakpoint(serial: Long): Unit =
   151     global_state.change(_.toggle_breakpoint(serial))
   152 
   153   def focus(new_focus: Option[Position.T]): Boolean =
   154     global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus)))
   155 
   156   def cancel(thread_name: String): Unit =
   157     current_state().session.protocol_command("Debugger.cancel", thread_name)
   158 
   159   def input(thread_name: String, msg: String*): Unit =
   160     current_state().session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
   161 
   162   def step(thread_name: String): Unit = input(thread_name, "step")
   163   def step_over(thread_name: String): Unit = input(thread_name, "step_over")
   164   def step_out(thread_name: String): Unit = input(thread_name, "step_out")
   165   def continue(thread_name: String): Unit = input(thread_name, "continue")
   166 
   167   def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String): Unit =
   168   {
   169     input(thread_name, "eval",
   170       index.toString, SML.toString, Symbol.encode(context), Symbol.encode(expression))
   171   }
   172 }