author | wenzelm |
Mon, 24 Aug 2015 20:32:32 +0200 | |
changeset 61018 | 32cc7d219c38 |
parent 61016 | 7c5a877b0f8e |
child 61019 | 7ce030f14aa9 |
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 |
{ |
|
61010 | 15 |
/* context */ |
60834 | 16 |
|
60842 | 17 |
sealed case class Debug_State( |
18 |
pos: Position.T, |
|
19 |
function: String) |
|
20 |
||
61010 | 21 |
sealed case class Context(thread_name: String, debug_states: List[Debug_State], index: Int = 0) |
22 |
{ |
|
23 |
def size: Int = debug_states.length + 1 |
|
24 |
def reset: Context = copy(index = 0) |
|
25 |
def select(i: Int) = copy(index = i + 1) |
|
26 |
||
27 |
def thread_state: Option[Debug_State] = debug_states.headOption |
|
28 |
||
29 |
def stack_state: Option[Debug_State] = |
|
30 |
if (1 <= index && index <= debug_states.length) |
|
31 |
Some(debug_states(index - 1)) |
|
32 |
else None |
|
33 |
||
61014 | 34 |
def debug_index: Option[Int] = |
61010 | 35 |
if (stack_state.isDefined) Some(index - 1) |
36 |
else if (debug_states.nonEmpty) Some(0) |
|
37 |
else None |
|
38 |
||
39 |
def debug_state: Option[Debug_State] = stack_state orElse thread_state |
|
61014 | 40 |
def debug_position: Option[Position.T] = debug_state.map(_.pos) |
61010 | 41 |
|
42 |
override def toString: String = |
|
43 |
stack_state match { |
|
44 |
case None => thread_name |
|
45 |
case Some(d) => d.function |
|
46 |
} |
|
47 |
} |
|
48 |
||
49 |
||
50 |
/* global state */ |
|
51 |
||
61016 | 52 |
type Threads = SortedMap[String, List[Debug_State]] |
53 |
||
60835 | 54 |
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
|
55 |
session: Session = new Session(Resources.empty), // implicit session |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
56 |
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
|
57 |
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
|
58 |
active_breakpoints: Set[Long] = Set.empty, // explicit breakpoint state |
61016 | 59 |
threads: Threads = SortedMap.empty, // thread name ~> stack of debug states |
61014 | 60 |
focus: Map[String, Context] = Map.empty, // thread name ~> focus |
60834 | 61 |
output: Map[String, Command.Results] = Map.empty) // thread name ~> output messages |
62 |
{ |
|
60842 | 63 |
def set_session(new_session: Session): State = |
64 |
copy(session = new_session) |
|
65 |
||
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
66 |
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
|
67 |
|
60910 | 68 |
def is_active: Boolean = active > 0 && session.is_ready |
60898 | 69 |
def inc_active: State = copy(active = active + 1) |
70 |
def dec_active: State = copy(active = active - 1) |
|
60876 | 71 |
|
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
72 |
def toggle_breakpoint(breakpoint: Long): (Boolean, State) = |
60876 | 73 |
{ |
74 |
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
|
75 |
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
|
76 |
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
|
77 |
(active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1)) |
60876 | 78 |
} |
79 |
||
60842 | 80 |
def get_thread(thread_name: String): List[Debug_State] = |
81 |
threads.getOrElse(thread_name, Nil) |
|
82 |
||
83 |
def update_thread(thread_name: String, debug_states: List[Debug_State]): State = |
|
61014 | 84 |
if (debug_states.isEmpty) copy(threads = threads - thread_name, focus = focus - thread_name) |
60903 | 85 |
else copy(threads = threads + (thread_name -> debug_states)) |
60842 | 86 |
|
61014 | 87 |
def set_focus(c: Context): State = copy(focus = focus + (c.thread_name -> c)) |
88 |
||
60842 | 89 |
def get_output(thread_name: String): Command.Results = |
90 |
output.getOrElse(thread_name, Command.Results.empty) |
|
91 |
||
92 |
def add_output(thread_name: String, entry: Command.Results.Entry): State = |
|
93 |
copy(output = output + (thread_name -> (get_output(thread_name) + entry))) |
|
94 |
||
95 |
def clear_output(thread_name: String): State = |
|
96 |
copy(output = output - thread_name) |
|
60834 | 97 |
} |
98 |
||
99 |
private val global_state = Synchronized(State()) |
|
100 |
||
101 |
||
60902 | 102 |
/* update events */ |
60749 | 103 |
|
60900 | 104 |
case object Update |
60749 | 105 |
|
60902 | 106 |
private val delay_update = |
107 |
Simple_Thread.delay_first(global_state.value.session.output_delay) { |
|
108 |
global_state.value.session.debugger_updates.post(Update) |
|
109 |
} |
|
110 |
||
111 |
||
112 |
/* protocol handler */ |
|
113 |
||
60749 | 114 |
class Handler extends Session.Protocol_Handler |
115 |
{ |
|
60842 | 116 |
private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean = |
117 |
{ |
|
118 |
msg.properties match { |
|
119 |
case Markup.Debugger_State(thread_name) => |
|
60863 | 120 |
val msg_body = |
121 |
YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) |
|
60842 | 122 |
val debug_states = |
123 |
{ |
|
124 |
import XML.Decode._ |
|
125 |
list(pair(properties, Symbol.decode_string))(msg_body).map({ |
|
126 |
case (pos, function) => Debug_State(pos, function) |
|
127 |
}) |
|
128 |
} |
|
129 |
global_state.change(_.update_thread(thread_name, debug_states)) |
|
60900 | 130 |
delay_update.invoke() |
60842 | 131 |
true |
132 |
case _ => false |
|
133 |
} |
|
134 |
} |
|
135 |
||
60830 | 136 |
private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean = |
137 |
{ |
|
138 |
msg.properties match { |
|
60835 | 139 |
case Markup.Debugger_Output(thread_name) => |
60834 | 140 |
val msg_body = |
141 |
prover.xml_cache.body( |
|
60863 | 142 |
YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes)))) |
60834 | 143 |
msg_body match { |
144 |
case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) => |
|
145 |
val message = XML.Elem(Markup(Markup.message(name), props), body) |
|
60835 | 146 |
global_state.change(_.add_output(thread_name, i -> message)) |
60900 | 147 |
delay_update.invoke() |
60834 | 148 |
true |
149 |
case _ => false |
|
150 |
} |
|
60830 | 151 |
case _ => false |
152 |
} |
|
153 |
} |
|
154 |
||
155 |
val functions = |
|
60842 | 156 |
Map( |
157 |
Markup.DEBUGGER_STATE -> debugger_state _, |
|
158 |
Markup.DEBUGGER_OUTPUT -> debugger_output _) |
|
60749 | 159 |
} |
60765 | 160 |
|
161 |
||
162 |
/* protocol commands */ |
|
163 |
||
60898 | 164 |
def is_active(): Boolean = global_state.value.is_active |
60889 | 165 |
|
60910 | 166 |
def init_session(session: Session) |
167 |
{ |
|
168 |
global_state.change(state => |
|
169 |
{ |
|
170 |
val state1 = state.set_session(session) |
|
171 |
if (!state.session.is_ready && state1.session.is_ready && state1.is_active) |
|
172 |
state1.session.protocol_command("Debugger.init") |
|
173 |
state1 |
|
174 |
}) |
|
175 |
} |
|
176 |
||
177 |
def init(): Unit = |
|
60889 | 178 |
global_state.change(state => |
179 |
{ |
|
60898 | 180 |
val state1 = state.inc_active |
181 |
if (!state.is_active && state1.is_active) |
|
182 |
state1.session.protocol_command("Debugger.init") |
|
60889 | 183 |
state1 |
184 |
}) |
|
185 |
||
60910 | 186 |
def exit(): Unit = |
60889 | 187 |
global_state.change(state => |
188 |
{ |
|
60898 | 189 |
val state1 = state.dec_active |
190 |
if (state.is_active && !state1.is_active) |
|
191 |
state1.session.protocol_command("Debugger.exit") |
|
60889 | 192 |
state1 |
193 |
}) |
|
60876 | 194 |
|
60932
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
195 |
def is_break(): Boolean = global_state.value.break |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
196 |
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
|
197 |
{ |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
198 |
global_state.change(state => { |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
199 |
val state1 = state.set_break(b) |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
200 |
state1.session.protocol_command("Debugger.break", b.toString) |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
201 |
state1 |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
202 |
}) |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
203 |
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
|
204 |
} |
13ee73f57c85
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents:
60912
diff
changeset
|
205 |
|
60882 | 206 |
def active_breakpoint_state(breakpoint: Long): Option[Boolean] = |
60876 | 207 |
{ |
60898 | 208 |
val state = global_state.value |
60912 | 209 |
if (state.is_active) Some(state.active_breakpoints(breakpoint)) else None |
60876 | 210 |
} |
211 |
||
60882 | 212 |
def breakpoint_state(breakpoint: Long): Boolean = |
60898 | 213 |
global_state.value.active_breakpoints(breakpoint) |
60882 | 214 |
|
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
215 |
def toggle_breakpoint(command: Command, breakpoint: Long) |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
216 |
{ |
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
217 |
global_state.change(state => |
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
218 |
{ |
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
219 |
val (breakpoint_state, state1) = state.toggle_breakpoint(breakpoint) |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
220 |
state1.session.protocol_command( |
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
221 |
"Debugger.breakpoint", |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
222 |
Symbol.encode(command.node_name.node), |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
223 |
Document_ID(command.id), |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
224 |
Properties.Value.Long(breakpoint), |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
225 |
Properties.Value.Boolean(breakpoint_state)) |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
226 |
state1 |
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
227 |
}) |
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
228 |
} |
60876 | 229 |
|
61018 | 230 |
def status(focus: Option[Context]): (Threads, List[XML.Tree]) = |
231 |
{ |
|
232 |
val state = global_state.value |
|
233 |
val output = |
|
234 |
focus match { |
|
235 |
case None => Nil |
|
236 |
case Some(c) => |
|
237 |
(for { |
|
238 |
(thread_name, results) <- state.output |
|
239 |
if thread_name == c.thread_name |
|
240 |
(_, tree) <- results.iterator |
|
241 |
} yield tree).toList |
|
242 |
} |
|
243 |
(state.threads, output) |
|
244 |
} |
|
61011 | 245 |
|
61014 | 246 |
def focus(): List[Context] = global_state.value.focus.toList.map(_._2) |
247 |
def set_focus(c: Context) |
|
61008 | 248 |
{ |
61014 | 249 |
global_state.change(_.set_focus(c)) |
61008 | 250 |
delay_update.invoke() |
251 |
} |
|
60875 | 252 |
|
60854 | 253 |
def input(thread_name: String, msg: String*): Unit = |
60898 | 254 |
global_state.value.session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*) |
60854 | 255 |
|
60899 | 256 |
def continue(thread_name: String): Unit = input(thread_name, "continue") |
60869 | 257 |
def step(thread_name: String): Unit = input(thread_name, "step") |
258 |
def step_over(thread_name: String): Unit = input(thread_name, "step_over") |
|
259 |
def step_out(thread_name: String): Unit = input(thread_name, "step_out") |
|
60856 | 260 |
|
60901 | 261 |
def clear_output(thread_name: String) |
262 |
{ |
|
263 |
global_state.change(_.clear_output(thread_name)) |
|
60902 | 264 |
delay_update.invoke() |
60901 | 265 |
} |
266 |
||
61010 | 267 |
def eval(c: Context, SML: Boolean, context: String, expression: String) |
60856 | 268 |
{ |
60896 | 269 |
global_state.change(state => { |
61014 | 270 |
input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString, |
61010 | 271 |
SML.toString, Symbol.encode(context), Symbol.encode(expression)) |
272 |
state.clear_output(c.thread_name) |
|
60896 | 273 |
}) |
60902 | 274 |
delay_update.invoke() |
60856 | 275 |
} |
60897 | 276 |
|
61010 | 277 |
def print_vals(c: Context, SML: Boolean, context: String) |
60897 | 278 |
{ |
61014 | 279 |
require(c.debug_index.isDefined) |
61010 | 280 |
|
60897 | 281 |
global_state.change(state => { |
61014 | 282 |
input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString, |
61010 | 283 |
SML.toString, Symbol.encode(context)) |
284 |
state.clear_output(c.thread_name) |
|
60897 | 285 |
}) |
60902 | 286 |
delay_update.invoke() |
60897 | 287 |
} |
60749 | 288 |
} |