author | wenzelm |
Tue, 14 Mar 2017 11:16:23 +0100 | |
changeset 65223 | 844c067bc3d4 |
parent 65222 | fb8253564483 |
child 65344 | b99283eed13c |
permissions | -rw-r--r-- |
60749 | 1 |
/* Title: Pure/Tools/debugger.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Interactive debugger for Isabelle/ML. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
61016 | 10 |
import scala.collection.immutable.SortedMap |
11 |
||
12 |
||
60749 | 13 |
object Debugger |
14 |
{ |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
15 |
/* thread context */ |
60834 | 16 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
17 |
case object Update |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
18 |
|
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
19 |
sealed case class Debug_State(pos: Position.T, function: String) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
20 |
type Threads = SortedMap[String, List[Debug_State]] |
60842 | 21 |
|
61010 | 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 |
||
61014 | 35 |
def debug_index: Option[Int] = |
61010 | 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 |
|
61014 | 41 |
def debug_position: Option[Position.T] = debug_state.map(_.pos) |
61010 | 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 |
||
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
51 |
/* debugger state */ |
61016 | 52 |
|
60835 | 53 |
sealed case class State( |
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
54 |
active: Int = 0, // active views |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
55 |
break: Boolean = false, // break at next possible breakpoint |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
56 |
active_breakpoints: Set[Long] = Set.empty, // explicit breakpoint state |
61016 | 57 |
threads: Threads = SortedMap.empty, // thread name ~> stack of debug states |
61014 | 58 |
focus: Map[String, Context] = Map.empty, // thread name ~> focus |
60834 | 59 |
output: Map[String, Command.Results] = Map.empty) // thread name ~> output messages |
60 |
{ |
|
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
61 |
def set_break(b: Boolean): State = copy(break = b) |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
62 |
|
65223
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
63 |
def is_active: Boolean = active > 0 |
60898 | 64 |
def inc_active: State = copy(active = active + 1) |
65 |
def dec_active: State = copy(active = active - 1) |
|
60876 | 66 |
|
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
67 |
def toggle_breakpoint(breakpoint: Long): (Boolean, State) = |
60876 | 68 |
{ |
69 |
val active_breakpoints1 = |
|
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
70 |
if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
71 |
else active_breakpoints + breakpoint |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
72 |
(active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1)) |
60876 | 73 |
} |
74 |
||
60842 | 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 = |
|
61019
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
79 |
{ |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
80 |
val threads1 = |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
81 |
if (debug_states.nonEmpty) threads + (thread_name -> debug_states) |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
82 |
else threads - thread_name |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
83 |
val focus1 = |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
84 |
focus.get(thread_name) match { |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
85 |
case Some(c) if debug_states.nonEmpty => |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
86 |
focus + (thread_name -> Context(thread_name, debug_states)) |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
87 |
case _ => focus - thread_name |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
88 |
} |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
89 |
copy(threads = threads1, focus = focus1) |
7ce030f14aa9
reset focus after thread update (with new debug_states);
wenzelm
parents:
61018
diff
changeset
|
90 |
} |
60842 | 91 |
|
61014 | 92 |
def set_focus(c: Context): State = copy(focus = focus + (c.thread_name -> c)) |
93 |
||
60842 | 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) |
|
60834 | 102 |
} |
103 |
||
60902 | 104 |
|
105 |
/* protocol handler */ |
|
106 |
||
65222
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65219
diff
changeset
|
107 |
class Handler(session: Session) extends Session.Protocol_Handler |
60749 | 108 |
{ |
65222
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65219
diff
changeset
|
109 |
val debugger: Debugger = new Debugger(session) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
110 |
|
65219 | 111 |
private def debugger_state(msg: Prover.Protocol_Output): Boolean = |
60842 | 112 |
{ |
113 |
msg.properties match { |
|
114 |
case Markup.Debugger_State(thread_name) => |
|
60863 | 115 |
val msg_body = |
116 |
YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) |
|
60842 | 117 |
val debug_states = |
118 |
{ |
|
119 |
import XML.Decode._ |
|
120 |
list(pair(properties, Symbol.decode_string))(msg_body).map({ |
|
121 |
case (pos, function) => Debug_State(pos, function) |
|
122 |
}) |
|
123 |
} |
|
65222
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65219
diff
changeset
|
124 |
debugger.update_thread(thread_name, debug_states) |
60842 | 125 |
true |
126 |
case _ => false |
|
127 |
} |
|
128 |
} |
|
129 |
||
65219 | 130 |
private def debugger_output(msg: Prover.Protocol_Output): Boolean = |
60830 | 131 |
{ |
132 |
msg.properties match { |
|
60835 | 133 |
case Markup.Debugger_Output(thread_name) => |
65217 | 134 |
YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) match { |
60834 | 135 |
case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) => |
65218 | 136 |
val message = XML.Elem(Markup(Markup.message(name), props), body) |
65222
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65219
diff
changeset
|
137 |
debugger.add_output(thread_name, i -> session.xml_cache.elem(message)) |
60834 | 138 |
true |
139 |
case _ => false |
|
140 |
} |
|
60830 | 141 |
case _ => false |
142 |
} |
|
143 |
} |
|
144 |
||
145 |
val functions = |
|
65219 | 146 |
List( |
60842 | 147 |
Markup.DEBUGGER_STATE -> debugger_state _, |
148 |
Markup.DEBUGGER_OUTPUT -> debugger_output _) |
|
60749 | 149 |
} |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
150 |
} |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
151 |
|
65222
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65219
diff
changeset
|
152 |
class Debugger private(session: Session) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
153 |
{ |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
154 |
/* debugger state */ |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
155 |
|
65223
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
156 |
private val state = Synchronized(Debugger.State()) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
157 |
|
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
158 |
private val delay_update = |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
159 |
Standard_Thread.delay_first(session.output_delay) { |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
160 |
session.debugger_updates.post(Debugger.Update) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
161 |
} |
60765 | 162 |
|
163 |
||
164 |
/* protocol commands */ |
|
165 |
||
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
166 |
def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State]) |
60910 | 167 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
168 |
state.change(_.update_thread(thread_name, debug_states)) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
169 |
delay_update.invoke() |
60910 | 170 |
} |
171 |
||
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
172 |
def add_output(thread_name: String, entry: Command.Results.Entry) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
173 |
{ |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
174 |
state.change(_.add_output(thread_name, entry)) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
175 |
delay_update.invoke() |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
176 |
} |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
177 |
|
65223
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
178 |
def is_active(): Boolean = session.is_ready && state.value.is_active |
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
179 |
|
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
180 |
def ready() |
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
181 |
{ |
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
182 |
if (is_active()) |
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
183 |
session.protocol_command("Debugger.init") |
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
184 |
} |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
185 |
|
60910 | 186 |
def init(): Unit = |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
187 |
state.change(st => |
60889 | 188 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
189 |
val st1 = st.inc_active |
65223
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
190 |
if (session.is_ready && !st.is_active && st1.is_active) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
191 |
session.protocol_command("Debugger.init") |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
192 |
st1 |
60889 | 193 |
}) |
194 |
||
60910 | 195 |
def exit(): Unit = |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
196 |
state.change(st => |
60889 | 197 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
198 |
val st1 = st.dec_active |
65223
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
199 |
if (session.is_ready && st.is_active && !st1.is_active) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
200 |
session.protocol_command("Debugger.exit") |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
201 |
st1 |
60889 | 202 |
}) |
60876 | 203 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
204 |
def is_break(): Boolean = state.value.break |
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
205 |
def set_break(b: Boolean) |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
206 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
207 |
state.change(st => { |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
208 |
val st1 = st.set_break(b) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
209 |
session.protocol_command("Debugger.break", b.toString) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
210 |
st1 |
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
211 |
}) |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
212 |
delay_update.invoke() |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
213 |
} |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
214 |
|
60882 | 215 |
def active_breakpoint_state(breakpoint: Long): Option[Boolean] = |
60876 | 216 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
217 |
val st = state.value |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
218 |
if (st.is_active) Some(st.active_breakpoints(breakpoint)) else None |
60876 | 219 |
} |
220 |
||
60882 | 221 |
def breakpoint_state(breakpoint: Long): Boolean = |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
222 |
state.value.active_breakpoints(breakpoint) |
60882 | 223 |
|
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
224 |
def toggle_breakpoint(command: Command, breakpoint: Long) |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
225 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
226 |
state.change(st => |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
227 |
{ |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
228 |
val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
229 |
session.protocol_command( |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
230 |
"Debugger.breakpoint", |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
231 |
Symbol.encode(command.node_name.node), |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
232 |
Document_ID(command.id), |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
233 |
Value.Long(breakpoint), |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
234 |
Value.Boolean(breakpoint_state)) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
235 |
st1 |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
236 |
}) |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
237 |
} |
60876 | 238 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
239 |
def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) = |
61018 | 240 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
241 |
val st = state.value |
61018 | 242 |
val output = |
243 |
focus match { |
|
244 |
case None => Nil |
|
245 |
case Some(c) => |
|
246 |
(for { |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
247 |
(thread_name, results) <- st.output |
61018 | 248 |
if thread_name == c.thread_name |
249 |
(_, tree) <- results.iterator |
|
250 |
} yield tree).toList |
|
251 |
} |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
252 |
(st.threads, output) |
61018 | 253 |
} |
61011 | 254 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
255 |
def focus(): List[Debugger.Context] = state.value.focus.toList.map(_._2) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
256 |
def set_focus(c: Debugger.Context) |
61008 | 257 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
258 |
state.change(_.set_focus(c)) |
61008 | 259 |
delay_update.invoke() |
260 |
} |
|
60875 | 261 |
|
60854 | 262 |
def input(thread_name: String, msg: String*): Unit = |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
263 |
session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*) |
60854 | 264 |
|
60899 | 265 |
def continue(thread_name: String): Unit = input(thread_name, "continue") |
60869 | 266 |
def step(thread_name: String): Unit = input(thread_name, "step") |
267 |
def step_over(thread_name: String): Unit = input(thread_name, "step_over") |
|
268 |
def step_out(thread_name: String): Unit = input(thread_name, "step_out") |
|
60856 | 269 |
|
60901 | 270 |
def clear_output(thread_name: String) |
271 |
{ |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
272 |
state.change(_.clear_output(thread_name)) |
60902 | 273 |
delay_update.invoke() |
60901 | 274 |
} |
275 |
||
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
276 |
def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String) |
60856 | 277 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
278 |
state.change(st => { |
61014 | 279 |
input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString, |
61010 | 280 |
SML.toString, Symbol.encode(context), Symbol.encode(expression)) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
281 |
st.clear_output(c.thread_name) |
60896 | 282 |
}) |
60902 | 283 |
delay_update.invoke() |
60856 | 284 |
} |
60897 | 285 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
286 |
def print_vals(c: Debugger.Context, SML: Boolean, context: String) |
60897 | 287 |
{ |
61014 | 288 |
require(c.debug_index.isDefined) |
61010 | 289 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
290 |
state.change(st => { |
61014 | 291 |
input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString, |
61010 | 292 |
SML.toString, Symbol.encode(context)) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
293 |
st.clear_output(c.thread_name) |
60897 | 294 |
}) |
60902 | 295 |
delay_update.invoke() |
60897 | 296 |
} |
60749 | 297 |
} |