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