author | wenzelm |
Wed, 12 Aug 2015 02:20:06 +0200 | |
changeset 60912 | 3852e87e9b88 |
parent 60910 | 79abcf48c377 |
child 60932 | 13ee73f57c85 |
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 |
||
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), |
|
60876 | 20 |
active: Int = 0, |
21 |
active_breakpoints: Set[Long] = Set.empty, |
|
60875 | 22 |
focus: Option[Position.T] = None, // position of active GUI component |
60842 | 23 |
threads: Map[String, List[Debug_State]] = Map.empty, // thread name ~> stack of debug states |
60834 | 24 |
output: Map[String, Command.Results] = Map.empty) // thread name ~> output messages |
25 |
{ |
|
60842 | 26 |
def set_session(new_session: Session): State = |
27 |
copy(session = new_session) |
|
28 |
||
60910 | 29 |
def is_active: Boolean = active > 0 && session.is_ready |
60898 | 30 |
def inc_active: State = copy(active = active + 1) |
31 |
def dec_active: State = copy(active = active - 1) |
|
60876 | 32 |
|
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
33 |
def toggle_breakpoint(breakpoint: Long): (Boolean, State) = |
60876 | 34 |
{ |
35 |
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
|
36 |
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
|
37 |
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
|
38 |
(active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1)) |
60876 | 39 |
} |
40 |
||
60875 | 41 |
def set_focus(new_focus: Option[Position.T]): State = |
42 |
copy(focus = new_focus) |
|
43 |
||
60842 | 44 |
def get_thread(thread_name: String): List[Debug_State] = |
45 |
threads.getOrElse(thread_name, Nil) |
|
46 |
||
47 |
def update_thread(thread_name: String, debug_states: List[Debug_State]): State = |
|
60903 | 48 |
if (debug_states.isEmpty) copy(threads = threads - thread_name) |
49 |
else copy(threads = threads + (thread_name -> debug_states)) |
|
60842 | 50 |
|
51 |
def get_output(thread_name: String): Command.Results = |
|
52 |
output.getOrElse(thread_name, Command.Results.empty) |
|
53 |
||
54 |
def add_output(thread_name: String, entry: Command.Results.Entry): State = |
|
55 |
copy(output = output + (thread_name -> (get_output(thread_name) + entry))) |
|
56 |
||
57 |
def clear_output(thread_name: String): State = |
|
58 |
copy(output = output - thread_name) |
|
60834 | 59 |
} |
60 |
||
61 |
private val global_state = Synchronized(State()) |
|
62 |
||
63 |
||
60902 | 64 |
/* update events */ |
60749 | 65 |
|
60900 | 66 |
case object Update |
60749 | 67 |
|
60902 | 68 |
private val delay_update = |
69 |
Simple_Thread.delay_first(global_state.value.session.output_delay) { |
|
70 |
global_state.value.session.debugger_updates.post(Update) |
|
71 |
} |
|
72 |
||
73 |
||
74 |
/* protocol handler */ |
|
75 |
||
60749 | 76 |
class Handler extends Session.Protocol_Handler |
77 |
{ |
|
60842 | 78 |
private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean = |
79 |
{ |
|
80 |
msg.properties match { |
|
81 |
case Markup.Debugger_State(thread_name) => |
|
60863 | 82 |
val msg_body = |
83 |
YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) |
|
60842 | 84 |
val debug_states = |
85 |
{ |
|
86 |
import XML.Decode._ |
|
87 |
list(pair(properties, Symbol.decode_string))(msg_body).map({ |
|
88 |
case (pos, function) => Debug_State(pos, function) |
|
89 |
}) |
|
90 |
} |
|
91 |
global_state.change(_.update_thread(thread_name, debug_states)) |
|
60900 | 92 |
delay_update.invoke() |
60842 | 93 |
true |
94 |
case _ => false |
|
95 |
} |
|
96 |
} |
|
97 |
||
60830 | 98 |
private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean = |
99 |
{ |
|
100 |
msg.properties match { |
|
60835 | 101 |
case Markup.Debugger_Output(thread_name) => |
60834 | 102 |
val msg_body = |
103 |
prover.xml_cache.body( |
|
60863 | 104 |
YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes)))) |
60834 | 105 |
msg_body match { |
106 |
case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) => |
|
107 |
val message = XML.Elem(Markup(Markup.message(name), props), body) |
|
60835 | 108 |
global_state.change(_.add_output(thread_name, i -> message)) |
60900 | 109 |
delay_update.invoke() |
60834 | 110 |
true |
111 |
case _ => false |
|
112 |
} |
|
60830 | 113 |
case _ => false |
114 |
} |
|
115 |
} |
|
116 |
||
117 |
val functions = |
|
60842 | 118 |
Map( |
119 |
Markup.DEBUGGER_STATE -> debugger_state _, |
|
120 |
Markup.DEBUGGER_OUTPUT -> debugger_output _) |
|
60749 | 121 |
} |
60765 | 122 |
|
123 |
||
124 |
/* protocol commands */ |
|
125 |
||
60898 | 126 |
def is_active(): Boolean = global_state.value.is_active |
60889 | 127 |
|
60910 | 128 |
def init_session(session: Session) |
129 |
{ |
|
130 |
global_state.change(state => |
|
131 |
{ |
|
132 |
val state1 = state.set_session(session) |
|
133 |
if (!state.session.is_ready && state1.session.is_ready && state1.is_active) |
|
134 |
state1.session.protocol_command("Debugger.init") |
|
135 |
state1 |
|
136 |
}) |
|
137 |
} |
|
138 |
||
139 |
def init(): Unit = |
|
60889 | 140 |
global_state.change(state => |
141 |
{ |
|
60898 | 142 |
val state1 = state.inc_active |
143 |
if (!state.is_active && state1.is_active) |
|
144 |
state1.session.protocol_command("Debugger.init") |
|
60889 | 145 |
state1 |
146 |
}) |
|
147 |
||
60910 | 148 |
def exit(): Unit = |
60889 | 149 |
global_state.change(state => |
150 |
{ |
|
60898 | 151 |
val state1 = state.dec_active |
152 |
if (state.is_active && !state1.is_active) |
|
153 |
state1.session.protocol_command("Debugger.exit") |
|
60889 | 154 |
state1 |
155 |
}) |
|
60876 | 156 |
|
60882 | 157 |
def active_breakpoint_state(breakpoint: Long): Option[Boolean] = |
60876 | 158 |
{ |
60898 | 159 |
val state = global_state.value |
60912 | 160 |
if (state.is_active) Some(state.active_breakpoints(breakpoint)) else None |
60876 | 161 |
} |
162 |
||
60882 | 163 |
def breakpoint_state(breakpoint: Long): Boolean = |
60898 | 164 |
global_state.value.active_breakpoints(breakpoint) |
60882 | 165 |
|
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
166 |
def toggle_breakpoint(command: Command, breakpoint: Long) |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
167 |
{ |
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
168 |
global_state.change(state => |
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
169 |
{ |
60880
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
170 |
val (breakpoint_state, state1) = state.toggle_breakpoint(breakpoint) |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
171 |
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
|
172 |
"Debugger.breakpoint", |
fa958e24ff24
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents:
60878
diff
changeset
|
173 |
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
|
174 |
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
|
175 |
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
|
176 |
Properties.Value.Boolean(breakpoint_state)) |
60878
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
177 |
state1 |
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
178 |
}) |
1f0d2bbcf38b
added action to toggle breakpoints (on editor side);
wenzelm
parents:
60876
diff
changeset
|
179 |
} |
60876 | 180 |
|
60875 | 181 |
def focus(new_focus: Option[Position.T]): Boolean = |
182 |
global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus))) |
|
183 |
||
60898 | 184 |
def threads(): Map[String, List[Debug_State]] = global_state.value.threads |
185 |
||
186 |
def output(): Map[String, Command.Results] = global_state.value.output |
|
187 |
||
60854 | 188 |
def input(thread_name: String, msg: String*): Unit = |
60898 | 189 |
global_state.value.session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*) |
60854 | 190 |
|
60899 | 191 |
def continue(thread_name: String): Unit = input(thread_name, "continue") |
60869 | 192 |
def step(thread_name: String): Unit = input(thread_name, "step") |
193 |
def step_over(thread_name: String): Unit = input(thread_name, "step_over") |
|
194 |
def step_out(thread_name: String): Unit = input(thread_name, "step_out") |
|
60856 | 195 |
|
60901 | 196 |
def clear_output(thread_name: String) |
197 |
{ |
|
198 |
global_state.change(_.clear_output(thread_name)) |
|
60902 | 199 |
delay_update.invoke() |
60901 | 200 |
} |
201 |
||
60896 | 202 |
def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String) |
60856 | 203 |
{ |
60896 | 204 |
global_state.change(state => { |
205 |
input(thread_name, "eval", |
|
206 |
index.toString, SML.toString, Symbol.encode(context), Symbol.encode(expression)) |
|
207 |
state.clear_output(thread_name) |
|
208 |
}) |
|
60902 | 209 |
delay_update.invoke() |
60856 | 210 |
} |
60897 | 211 |
|
212 |
def print_vals(thread_name: String, index: Int, SML: Boolean, context: String) |
|
213 |
{ |
|
214 |
global_state.change(state => { |
|
215 |
input(thread_name, "print_vals", index.toString, SML.toString, Symbol.encode(context)) |
|
216 |
state.clear_output(thread_name) |
|
217 |
}) |
|
60902 | 218 |
delay_update.invoke() |
60897 | 219 |
} |
60749 | 220 |
} |