1/* Title: Pure/Tools/debugger.scala 2 Author: Makarius 3 4Interactive debugger for Isabelle/ML. 5*/ 6 7package isabelle 8 9 10import scala.collection.immutable.SortedMap 11 12 13object Debugger 14{ 15 /* thread context */ 16 17 case object Update 18 19 sealed case class Debug_State(pos: Position.T, function: String) 20 type Threads = SortedMap[String, List[Debug_State]] 21 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 35 def debug_index: Option[Int] = 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 41 def debug_position: Option[Position.T] = debug_state.map(_.pos) 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 51 /* debugger state */ 52 53 sealed case class State( 54 active: Int = 0, // active views 55 break: Boolean = false, // break at next possible breakpoint 56 active_breakpoints: Set[Long] = Set.empty, // explicit breakpoint state 57 threads: Threads = SortedMap.empty, // thread name ~> stack of debug states 58 focus: Map[String, Context] = Map.empty, // thread name ~> focus 59 output: Map[String, Command.Results] = Map.empty) // thread name ~> output messages 60 { 61 def set_break(b: Boolean): State = copy(break = b) 62 63 def is_active: Boolean = active > 0 64 def inc_active: State = copy(active = active + 1) 65 def dec_active: State = copy(active = active - 1) 66 67 def toggle_breakpoint(breakpoint: Long): (Boolean, State) = 68 { 69 val active_breakpoints1 = 70 if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint 71 else active_breakpoints + breakpoint 72 (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1)) 73 } 74 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 = 79 { 80 val threads1 = 81 if (debug_states.nonEmpty) threads + (thread_name -> debug_states) 82 else threads - thread_name 83 val focus1 = 84 focus.get(thread_name) match { 85 case Some(c) if debug_states.nonEmpty => 86 focus + (thread_name -> Context(thread_name, debug_states)) 87 case _ => focus - thread_name 88 } 89 copy(threads = threads1, focus = focus1) 90 } 91 92 def set_focus(c: Context): State = copy(focus = focus + (c.thread_name -> c)) 93 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) 102 } 103 104 105 /* protocol handler */ 106 107 class Handler(session: Session) extends Session.Protocol_Handler 108 { 109 val debugger: Debugger = new Debugger(session) 110 111 private def debugger_state(msg: Prover.Protocol_Output): Boolean = 112 { 113 msg.properties match { 114 case Markup.Debugger_State(thread_name) => 115 val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) 116 val debug_states = 117 { 118 import XML.Decode._ 119 list(pair(properties, string))(msg_body).map({ 120 case (pos, function) => Debug_State(pos, function) 121 }) 122 } 123 debugger.update_thread(thread_name, debug_states) 124 true 125 case _ => false 126 } 127 } 128 129 private def debugger_output(msg: Prover.Protocol_Output): Boolean = 130 { 131 msg.properties match { 132 case Markup.Debugger_Output(thread_name) => 133 Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match { 134 case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) => 135 val message = XML.Elem(Markup(Markup.message(name), props), body) 136 debugger.add_output(thread_name, i -> session.xml_cache.elem(message)) 137 true 138 case _ => false 139 } 140 case _ => false 141 } 142 } 143 144 val functions = 145 List( 146 Markup.DEBUGGER_STATE -> debugger_state _, 147 Markup.DEBUGGER_OUTPUT -> debugger_output _) 148 } 149} 150 151class Debugger private(session: Session) 152{ 153 /* debugger state */ 154 155 private val state = Synchronized(Debugger.State()) 156 157 private val delay_update = 158 Standard_Thread.delay_first(session.output_delay) { 159 session.debugger_updates.post(Debugger.Update) 160 } 161 162 163 /* protocol commands */ 164 165 def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State]) 166 { 167 state.change(_.update_thread(thread_name, debug_states)) 168 delay_update.invoke() 169 } 170 171 def add_output(thread_name: String, entry: Command.Results.Entry) 172 { 173 state.change(_.add_output(thread_name, entry)) 174 delay_update.invoke() 175 } 176 177 def is_active(): Boolean = session.is_ready && state.value.is_active 178 179 def ready() 180 { 181 if (is_active()) 182 session.protocol_command("Debugger.init") 183 } 184 185 def init(): Unit = 186 state.change(st => 187 { 188 val st1 = st.inc_active 189 if (session.is_ready && !st.is_active && st1.is_active) 190 session.protocol_command("Debugger.init") 191 st1 192 }) 193 194 def exit(): Unit = 195 state.change(st => 196 { 197 val st1 = st.dec_active 198 if (session.is_ready && st.is_active && !st1.is_active) 199 session.protocol_command("Debugger.exit") 200 st1 201 }) 202 203 def is_break(): Boolean = state.value.break 204 def set_break(b: Boolean) 205 { 206 state.change(st => { 207 val st1 = st.set_break(b) 208 session.protocol_command("Debugger.break", b.toString) 209 st1 210 }) 211 delay_update.invoke() 212 } 213 214 def active_breakpoint_state(breakpoint: Long): Option[Boolean] = 215 { 216 val st = state.value 217 if (st.is_active) Some(st.active_breakpoints(breakpoint)) else None 218 } 219 220 def breakpoint_state(breakpoint: Long): Boolean = 221 state.value.active_breakpoints(breakpoint) 222 223 def toggle_breakpoint(command: Command, breakpoint: Long) 224 { 225 state.change(st => 226 { 227 val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint) 228 session.protocol_command( 229 "Debugger.breakpoint", 230 Symbol.encode(command.node_name.node), 231 Document_ID(command.id), 232 Value.Long(breakpoint), 233 Value.Boolean(breakpoint_state)) 234 st1 235 }) 236 } 237 238 def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) = 239 { 240 val st = state.value 241 val output = 242 focus match { 243 case None => Nil 244 case Some(c) => 245 (for { 246 (thread_name, results) <- st.output 247 if thread_name == c.thread_name 248 (_, tree) <- results.iterator 249 } yield tree).toList 250 } 251 (st.threads, output) 252 } 253 254 def focus(): List[Debugger.Context] = state.value.focus.toList.map(_._2) 255 def set_focus(c: Debugger.Context) 256 { 257 state.change(_.set_focus(c)) 258 delay_update.invoke() 259 } 260 261 def input(thread_name: String, msg: String*): Unit = 262 session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*) 263 264 def continue(thread_name: String): Unit = input(thread_name, "continue") 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") 268 269 def clear_output(thread_name: String) 270 { 271 state.change(_.clear_output(thread_name)) 272 delay_update.invoke() 273 } 274 275 def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String) 276 { 277 state.change(st => { 278 input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString, 279 SML.toString, Symbol.encode(context), Symbol.encode(expression)) 280 st.clear_output(c.thread_name) 281 }) 282 delay_update.invoke() 283 } 284 285 def print_vals(c: Debugger.Context, SML: Boolean, context: String) 286 { 287 require(c.debug_index.isDefined) 288 289 state.change(st => { 290 input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString, 291 SML.toString, Symbol.encode(context)) 292 st.clear_output(c.thread_name) 293 }) 294 delay_update.invoke() 295 } 296} 297