9 |
9 |
10 object Debugger |
10 object Debugger |
11 { |
11 { |
12 /* global state */ |
12 /* global state */ |
13 |
13 |
|
14 sealed case class Debug_State( |
|
15 pos: Position.T, |
|
16 function: String) |
|
17 |
14 sealed case class State( |
18 sealed case class State( |
15 session: Session = new Session(Resources.empty), |
19 session: Session = new Session(Resources.empty), |
|
20 threads: Map[String, List[Debug_State]] = Map.empty, // thread name ~> stack of debug states |
16 output: Map[String, Command.Results] = Map.empty) // thread name ~> output messages |
21 output: Map[String, Command.Results] = Map.empty) // thread name ~> output messages |
17 { |
22 { |
18 def add_output(name: String, entry: Command.Results.Entry): State = |
23 def set_session(new_session: Session): State = |
19 copy(output = output + (name -> (output.getOrElse(name, Command.Results.empty) + entry))) |
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 |
20 } |
45 } |
21 |
46 |
22 private val global_state = Synchronized(State()) |
47 private val global_state = Synchronized(State()) |
23 def current_state(): State = global_state.value |
48 def current_state(): State = global_state.value |
24 |
49 |
39 { |
64 { |
40 updated += name |
65 updated += name |
41 delay_update.invoke() |
66 delay_update.invoke() |
42 } |
67 } |
43 |
68 |
|
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 |
44 private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean = |
88 private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean = |
45 { |
89 { |
46 msg.properties match { |
90 msg.properties match { |
47 case Markup.Debugger_Output(thread_name) => |
91 case Markup.Debugger_Output(thread_name) => |
48 val msg_body = |
92 val msg_body = |
59 case _ => false |
103 case _ => false |
60 } |
104 } |
61 } |
105 } |
62 |
106 |
63 val functions = |
107 val functions = |
64 Map(Markup.DEBUGGER_OUTPUT -> debugger_output _) |
108 Map( |
|
109 Markup.DEBUGGER_STATE -> debugger_state _, |
|
110 Markup.DEBUGGER_OUTPUT -> debugger_output _) |
65 } |
111 } |
66 |
112 |
67 |
113 |
68 /* protocol commands */ |
114 /* protocol commands */ |
69 |
115 |
70 def init(new_session: Session) |
116 def init(session: Session) |
71 { |
117 { |
72 global_state.change(_.copy(session = new_session)) |
118 global_state.change(_.set_session(session)) |
73 current_state().session.protocol_command("Debugger.init") |
119 current_state().session.protocol_command("Debugger.init") |
74 } |
120 } |
75 |
121 |
76 def cancel(name: String): Unit = |
122 def cancel(name: String): Unit = |
77 current_state().session.protocol_command("Debugger.cancel", name) |
123 current_state().session.protocol_command("Debugger.cancel", name) |