1/*  Title:      Pure/Tools/debugger.scala
2    Author:     Makarius
3
4Interactive debugger for Isabelle/ML.
5*/
6
7package isabelle
8
9
10import scala.collection.immutable.SortedMap
11
12
13object Debugger
14{
15  /* thread context */
16
17  case object Update
18
19  sealed case class Debug_State(pos: Position.T, function: String)
20  type Threads = SortedMap[String, List[Debug_State]]
21
22  sealed case class Context(thread_name: String, debug_states: List[Debug_State], index: Int = 0)
23  {
24    def size: Int = debug_states.length + 1
25    def reset: Context = copy(index = 0)
26    def select(i: Int) = copy(index = i + 1)
27
28    def thread_state: Option[Debug_State] = debug_states.headOption
29
30    def stack_state: Option[Debug_State] =
31      if (1 <= index && index <= debug_states.length)
32        Some(debug_states(index - 1))
33      else None
34
35    def debug_index: Option[Int] =
36      if (stack_state.isDefined) Some(index - 1)
37      else if (debug_states.nonEmpty) Some(0)
38      else None
39
40    def debug_state: Option[Debug_State] = stack_state orElse thread_state
41    def debug_position: Option[Position.T] = debug_state.map(_.pos)
42
43    override def toString: String =
44      stack_state match {
45        case None => thread_name
46        case Some(d) => d.function
47      }
48  }
49
50
51  /* debugger state */
52
53  sealed case class State(
54    active: Int = 0,  // active views
55    break: Boolean = false,  // break at next possible breakpoint
56    active_breakpoints: Set[Long] = Set.empty,  // explicit breakpoint state
57    threads: Threads = SortedMap.empty,  // thread name ~> stack of debug states
58    focus: Map[String, Context] = Map.empty,  // thread name ~> focus
59    output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
60  {
61    def set_break(b: Boolean): State = copy(break = b)
62
63    def is_active: Boolean = active > 0
64    def inc_active: State = copy(active = active + 1)
65    def dec_active: State = copy(active = active - 1)
66
67    def toggle_breakpoint(breakpoint: Long): (Boolean, State) =
68    {
69      val active_breakpoints1 =
70        if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint
71      else active_breakpoints + breakpoint
72      (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1))
73    }
74
75    def get_thread(thread_name: String): List[Debug_State] =
76      threads.getOrElse(thread_name, Nil)
77
78    def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
79    {
80      val threads1 =
81        if (debug_states.nonEmpty) threads + (thread_name -> debug_states)
82        else threads - thread_name
83      val focus1 =
84        focus.get(thread_name) match {
85          case Some(c) if debug_states.nonEmpty =>
86            focus + (thread_name -> Context(thread_name, debug_states))
87          case _ => focus - thread_name
88        }
89      copy(threads = threads1, focus = focus1)
90    }
91
92    def set_focus(c: Context): State = copy(focus = focus + (c.thread_name -> c))
93
94    def get_output(thread_name: String): Command.Results =
95      output.getOrElse(thread_name, Command.Results.empty)
96
97    def add_output(thread_name: String, entry: Command.Results.Entry): State =
98      copy(output = output + (thread_name -> (get_output(thread_name) + entry)))
99
100    def clear_output(thread_name: String): State =
101      copy(output = output - thread_name)
102  }
103
104
105  /* protocol handler */
106
107  class Handler(session: Session) extends Session.Protocol_Handler
108  {
109    val debugger: Debugger = new Debugger(session)
110
111    private def debugger_state(msg: Prover.Protocol_Output): Boolean =
112    {
113      msg.properties match {
114        case Markup.Debugger_State(thread_name) =>
115          val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes))
116          val debug_states =
117          {
118            import XML.Decode._
119            list(pair(properties, string))(msg_body).map({
120              case (pos, function) => Debug_State(pos, function)
121            })
122          }
123          debugger.update_thread(thread_name, debug_states)
124          true
125        case _ => false
126      }
127    }
128
129    private def debugger_output(msg: Prover.Protocol_Output): Boolean =
130    {
131      msg.properties match {
132        case Markup.Debugger_Output(thread_name) =>
133          Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
134            case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
135              val message = XML.Elem(Markup(Markup.message(name), props), body)
136              debugger.add_output(thread_name, i -> session.xml_cache.elem(message))
137              true
138            case _ => false
139          }
140        case _ => false
141      }
142    }
143
144    val functions =
145      List(
146        Markup.DEBUGGER_STATE -> debugger_state _,
147        Markup.DEBUGGER_OUTPUT -> debugger_output _)
148  }
149}
150
151class Debugger private(session: Session)
152{
153  /* debugger state */
154
155  private val state = Synchronized(Debugger.State())
156
157  private val delay_update =
158    Standard_Thread.delay_first(session.output_delay) {
159      session.debugger_updates.post(Debugger.Update)
160    }
161
162
163  /* protocol commands */
164
165  def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State])
166  {
167    state.change(_.update_thread(thread_name, debug_states))
168    delay_update.invoke()
169  }
170
171  def add_output(thread_name: String, entry: Command.Results.Entry)
172  {
173    state.change(_.add_output(thread_name, entry))
174    delay_update.invoke()
175  }
176
177  def is_active(): Boolean = session.is_ready && state.value.is_active
178
179  def ready()
180  {
181    if (is_active())
182      session.protocol_command("Debugger.init")
183  }
184
185  def init(): Unit =
186    state.change(st =>
187    {
188      val st1 = st.inc_active
189      if (session.is_ready && !st.is_active && st1.is_active)
190        session.protocol_command("Debugger.init")
191      st1
192    })
193
194  def exit(): Unit =
195    state.change(st =>
196    {
197      val st1 = st.dec_active
198      if (session.is_ready && st.is_active && !st1.is_active)
199        session.protocol_command("Debugger.exit")
200      st1
201    })
202
203  def is_break(): Boolean = state.value.break
204  def set_break(b: Boolean)
205  {
206    state.change(st => {
207      val st1 = st.set_break(b)
208      session.protocol_command("Debugger.break", b.toString)
209      st1
210    })
211    delay_update.invoke()
212  }
213
214  def active_breakpoint_state(breakpoint: Long): Option[Boolean] =
215  {
216    val st = state.value
217    if (st.is_active) Some(st.active_breakpoints(breakpoint)) else None
218  }
219
220  def breakpoint_state(breakpoint: Long): Boolean =
221    state.value.active_breakpoints(breakpoint)
222
223  def toggle_breakpoint(command: Command, breakpoint: Long)
224  {
225    state.change(st =>
226      {
227        val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint)
228        session.protocol_command(
229          "Debugger.breakpoint",
230          Symbol.encode(command.node_name.node),
231          Document_ID(command.id),
232          Value.Long(breakpoint),
233          Value.Boolean(breakpoint_state))
234        st1
235      })
236  }
237
238  def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) =
239  {
240    val st = state.value
241    val output =
242      focus match {
243        case None => Nil
244        case Some(c) =>
245          (for {
246            (thread_name, results) <- st.output
247            if thread_name == c.thread_name
248            (_, tree) <- results.iterator
249          } yield tree).toList
250      }
251    (st.threads, output)
252  }
253
254  def focus(): List[Debugger.Context] = state.value.focus.toList.map(_._2)
255  def set_focus(c: Debugger.Context)
256  {
257    state.change(_.set_focus(c))
258    delay_update.invoke()
259  }
260
261  def input(thread_name: String, msg: String*): Unit =
262    session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
263
264  def continue(thread_name: String): Unit = input(thread_name, "continue")
265  def step(thread_name: String): Unit = input(thread_name, "step")
266  def step_over(thread_name: String): Unit = input(thread_name, "step_over")
267  def step_out(thread_name: String): Unit = input(thread_name, "step_out")
268
269  def clear_output(thread_name: String)
270  {
271    state.change(_.clear_output(thread_name))
272    delay_update.invoke()
273  }
274
275  def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String)
276  {
277    state.change(st => {
278      input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString,
279        SML.toString, Symbol.encode(context), Symbol.encode(expression))
280      st.clear_output(c.thread_name)
281    })
282    delay_update.invoke()
283  }
284
285  def print_vals(c: Debugger.Context, SML: Boolean, context: String)
286  {
287    require(c.debug_index.isDefined)
288
289    state.change(st => {
290      input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString,
291        SML.toString, Symbol.encode(context))
292      st.clear_output(c.thread_name)
293    })
294    delay_update.invoke()
295  }
296}
297