author | wenzelm |
Sat, 01 Apr 2017 19:17:15 +0200 | |
changeset 65344 | b99283eed13c |
parent 65223 | 844c067bc3d4 |
child 71601 | 97ccf48c2f0c |
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) => |
|
65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65223
diff
changeset
|
115 |
val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) |
60842 | 116 |
val debug_states = |
117 |
{ |
|
118 |
import XML.Decode._ |
|
65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65223
diff
changeset
|
119 |
list(pair(properties, string))(msg_body).map({ |
60842 | 120 |
case (pos, function) => Debug_State(pos, function) |
121 |
}) |
|
122 |
} |
|
65222
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65219
diff
changeset
|
123 |
debugger.update_thread(thread_name, debug_states) |
60842 | 124 |
true |
125 |
case _ => false |
|
126 |
} |
|
127 |
} |
|
128 |
||
65219 | 129 |
private def debugger_output(msg: Prover.Protocol_Output): Boolean = |
60830 | 130 |
{ |
131 |
msg.properties match { |
|
60835 | 132 |
case Markup.Debugger_Output(thread_name) => |
65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65223
diff
changeset
|
133 |
Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match { |
60834 | 134 |
case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) => |
65218 | 135 |
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
|
136 |
debugger.add_output(thread_name, i -> session.xml_cache.elem(message)) |
60834 | 137 |
true |
138 |
case _ => false |
|
139 |
} |
|
60830 | 140 |
case _ => false |
141 |
} |
|
142 |
} |
|
143 |
||
144 |
val functions = |
|
65219 | 145 |
List( |
60842 | 146 |
Markup.DEBUGGER_STATE -> debugger_state _, |
147 |
Markup.DEBUGGER_OUTPUT -> debugger_output _) |
|
60749 | 148 |
} |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
149 |
} |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
150 |
|
65222
fb8253564483
more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents:
65219
diff
changeset
|
151 |
class Debugger private(session: Session) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
152 |
{ |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
153 |
/* debugger state */ |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
154 |
|
65223
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
155 |
private val state = Synchronized(Debugger.State()) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
156 |
|
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
157 |
private val delay_update = |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
158 |
Standard_Thread.delay_first(session.output_delay) { |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
159 |
session.debugger_updates.post(Debugger.Update) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
160 |
} |
60765 | 161 |
|
162 |
||
163 |
/* protocol commands */ |
|
164 |
||
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
165 |
def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State]) |
60910 | 166 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
167 |
state.change(_.update_thread(thread_name, debug_states)) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
168 |
delay_update.invoke() |
60910 | 169 |
} |
170 |
||
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
171 |
def add_output(thread_name: String, entry: Command.Results.Entry) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
172 |
{ |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
173 |
state.change(_.add_output(thread_name, entry)) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
174 |
delay_update.invoke() |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
175 |
} |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
176 |
|
65223
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
177 |
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
|
178 |
|
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
179 |
def ready() |
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
180 |
{ |
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
181 |
if (is_active()) |
844c067bc3d4
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
wenzelm
parents:
65222
diff
changeset
|
182 |
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
|
183 |
} |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
184 |
|
60910 | 185 |
def init(): Unit = |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
186 |
state.change(st => |
60889 | 187 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
188 |
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
|
189 |
if (session.is_ready && !st.is_active && st1.is_active) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
190 |
session.protocol_command("Debugger.init") |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
191 |
st1 |
60889 | 192 |
}) |
193 |
||
60910 | 194 |
def exit(): Unit = |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
195 |
state.change(st => |
60889 | 196 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
197 |
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
|
198 |
if (session.is_ready && st.is_active && !st1.is_active) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
199 |
session.protocol_command("Debugger.exit") |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
200 |
st1 |
60889 | 201 |
}) |
60876 | 202 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
203 |
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
|
204 |
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
|
205 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
206 |
state.change(st => { |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
207 |
val st1 = st.set_break(b) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
208 |
session.protocol_command("Debugger.break", b.toString) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
209 |
st1 |
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
210 |
}) |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
211 |
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
|
212 |
} |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
213 |
|
60882 | 214 |
def active_breakpoint_state(breakpoint: Long): Option[Boolean] = |
60876 | 215 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
216 |
val st = state.value |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
217 |
if (st.is_active) Some(st.active_breakpoints(breakpoint)) else None |
60876 | 218 |
} |
219 |
||
60882 | 220 |
def breakpoint_state(breakpoint: Long): Boolean = |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
221 |
state.value.active_breakpoints(breakpoint) |
60882 | 222 |
|
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
223 |
def toggle_breakpoint(command: Command, breakpoint: Long) |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
224 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
225 |
state.change(st => |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
226 |
{ |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
227 |
val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
228 |
session.protocol_command( |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
229 |
"Debugger.breakpoint", |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
230 |
Symbol.encode(command.node_name.node), |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
231 |
Document_ID(command.id), |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
232 |
Value.Long(breakpoint), |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
233 |
Value.Boolean(breakpoint_state)) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
234 |
st1 |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
235 |
}) |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
236 |
} |
60876 | 237 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
238 |
def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) = |
61018 | 239 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
240 |
val st = state.value |
61018 | 241 |
val output = |
242 |
focus match { |
|
243 |
case None => Nil |
|
244 |
case Some(c) => |
|
245 |
(for { |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
246 |
(thread_name, results) <- st.output |
61018 | 247 |
if thread_name == c.thread_name |
248 |
(_, tree) <- results.iterator |
|
249 |
} yield tree).toList |
|
250 |
} |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
251 |
(st.threads, output) |
61018 | 252 |
} |
61011 | 253 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
254 |
def focus(): List[Debugger.Context] = state.value.focus.toList.map(_._2) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
255 |
def set_focus(c: Debugger.Context) |
61008 | 256 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
257 |
state.change(_.set_focus(c)) |
61008 | 258 |
delay_update.invoke() |
259 |
} |
|
60875 | 260 |
|
60854 | 261 |
def input(thread_name: String, msg: String*): Unit = |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
262 |
session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*) |
60854 | 263 |
|
60899 | 264 |
def continue(thread_name: String): Unit = input(thread_name, "continue") |
60869 | 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") |
|
60856 | 268 |
|
60901 | 269 |
def clear_output(thread_name: String) |
270 |
{ |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
271 |
state.change(_.clear_output(thread_name)) |
60902 | 272 |
delay_update.invoke() |
60901 | 273 |
} |
274 |
||
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
275 |
def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String) |
60856 | 276 |
{ |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
277 |
state.change(st => { |
61014 | 278 |
input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString, |
61010 | 279 |
SML.toString, Symbol.encode(context), Symbol.encode(expression)) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
280 |
st.clear_output(c.thread_name) |
60896 | 281 |
}) |
60902 | 282 |
delay_update.invoke() |
60856 | 283 |
} |
60897 | 284 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
285 |
def print_vals(c: Debugger.Context, SML: Boolean, context: String) |
60897 | 286 |
{ |
61014 | 287 |
require(c.debug_index.isDefined) |
61010 | 288 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
289 |
state.change(st => { |
61014 | 290 |
input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString, |
61010 | 291 |
SML.toString, Symbol.encode(context)) |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
63805
diff
changeset
|
292 |
st.clear_output(c.thread_name) |
60897 | 293 |
}) |
60902 | 294 |
delay_update.invoke() |
60897 | 295 |
} |
60749 | 296 |
} |