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