# HG changeset patch # User wenzelm # Date 1438777087 -7200 # Node ID 5510c8444bc41692f31881aa2c99761c5599de9f # Parent 144523e0678e7eb836afc26212844b0880d49d1e protocol support for thread debugger state; diff -r 144523e0678e -r 5510c8444bc4 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue Aug 04 23:11:16 2015 +0200 +++ b/src/Pure/PIDE/markup.ML Wed Aug 05 14:18:07 2015 +0200 @@ -191,6 +191,7 @@ val build_theories_result: string -> Properties.T val print_operationsN: string val print_operations: Properties.T + val debugger_state: string -> Properties.T val debugger_output: string -> Properties.T val simp_trace_panelN: string val simp_trace_logN: string @@ -614,6 +615,7 @@ (* debugger *) +fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)]; fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)]; diff -r 144523e0678e -r 5510c8444bc4 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Aug 04 23:11:16 2015 +0200 +++ b/src/Pure/PIDE/markup.scala Wed Aug 05 14:18:07 2015 +0200 @@ -495,6 +495,16 @@ /* debugger output */ + val DEBUGGER_STATE = "debugger_state" + object Debugger_State + { + def unapply(props: Properties.T): Option[String] = + props match { + case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name) + case _ => None + } + } + val DEBUGGER_OUTPUT = "debugger_output" object Debugger_Output { diff -r 144523e0678e -r 5510c8444bc4 src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML Tue Aug 04 23:11:16 2015 +0200 +++ b/src/Pure/Tools/debugger.ML Wed Aug 05 14:18:07 2015 +0200 @@ -40,27 +40,27 @@ val global_state = Synchronized.var "Debugger.state" init_state; -fun cancel name = +fun cancel thread_name = Synchronized.change global_state (tap (fn State {threads, ...} => - (case Symtab.lookup threads name of + (case Symtab.lookup threads thread_name of NONE => () | SOME thread => Simple_Thread.interrupt_unsynchronized thread))); -fun input name msg = +fun input thread_name msg = Synchronized.change global_state (map_state (fn (threads, input) => - let val input' = Symtab.map_default (name, Queue.empty) (Queue.enqueue msg) input; + let val input' = Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg) input; in (threads, input') end)); -fun get_input name = +fun get_input thread_name = Synchronized.guarded_access global_state (fn State {threads, input} => - (case Symtab.lookup input name of + (case Symtab.lookup input thread_name of NONE => NONE | SOME queue => let val (msg, queue') = Queue.dequeue queue; val input' = - if Queue.is_empty queue' then Symtab.delete_safe name input - else Symtab.update (name, queue') input; + if Queue.is_empty queue' then Symtab.delete_safe thread_name input + else Symtab.update (thread_name, queue') input; in SOME (msg, make_state (threads, input')) end)); @@ -84,13 +84,23 @@ (* main entry point *) -fun debug_loop name = - (case get_input name of +fun debugger_state thread_name = + Output.protocol_message (Markup.debugger_state thread_name) + [get_data () + |> map (fn st => + (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)), + ML_Debugger.debug_function st)) + |> let open XML.Encode in list (pair properties string) end + |> YXML.string_of_body]; + +fun debugger_loop thread_name = + (debugger_state thread_name; + case get_input thread_name of ["continue"] => () | bad => (Output.system_message ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); - debug_loop name)); + debugger_loop thread_name)); fun debugger cond = if debugging () orelse not (cond ()) orelse @@ -100,7 +110,7 @@ with_debugging (fn () => (case Simple_Thread.get_name () of NONE => () - | SOME name => debug_loop name)); + | SOME thread_name => debugger_loop thread_name)); fun init () = ML_Debugger.on_breakpoint @@ -116,10 +126,10 @@ val _ = Isabelle_Process.protocol_command "Debugger.cancel" - (fn [name] => cancel name); + (fn [thread_name] => cancel thread_name); val _ = Isabelle_Process.protocol_command "Debugger.input" - (fn name :: msg => input name msg); + (fn thread_name :: msg => input thread_name msg); end; diff -r 144523e0678e -r 5510c8444bc4 src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Tue Aug 04 23:11:16 2015 +0200 +++ b/src/Pure/Tools/debugger.scala Wed Aug 05 14:18:07 2015 +0200 @@ -11,12 +11,37 @@ { /* global state */ + sealed case class Debug_State( + pos: Position.T, + function: String) + sealed case class State( session: Session = new Session(Resources.empty), + threads: Map[String, List[Debug_State]] = Map.empty, // thread name ~> stack of debug states output: Map[String, Command.Results] = Map.empty) // thread name ~> output messages { - def add_output(name: String, entry: Command.Results.Entry): State = - copy(output = output + (name -> (output.getOrElse(name, Command.Results.empty) + entry))) + def set_session(new_session: Session): State = + copy(session = new_session) + + def get_thread(thread_name: String): List[Debug_State] = + threads.getOrElse(thread_name, Nil) + + def update_thread(thread_name: String, debug_states: List[Debug_State]): State = + copy(threads = threads + (thread_name -> debug_states)) + + def get_output(thread_name: String): Command.Results = + output.getOrElse(thread_name, Command.Results.empty) + + def add_output(thread_name: String, entry: Command.Results.Entry): State = + copy(output = output + (thread_name -> (get_output(thread_name) + entry))) + + def clear_output(thread_name: String): State = + copy(output = output - thread_name) + + def purge(thread_name: String): State = + if (get_thread(thread_name).isEmpty) + copy(threads = threads - thread_name, output = output - thread_name) + else this } private val global_state = Synchronized(State()) @@ -41,6 +66,25 @@ delay_update.invoke() } + private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean = + { + msg.properties match { + case Markup.Debugger_State(thread_name) => + val msg_body = YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes)) + val debug_states = + { + import XML.Decode._ + list(pair(properties, Symbol.decode_string))(msg_body).map({ + case (pos, function) => Debug_State(pos, function) + }) + } + global_state.change(_.update_thread(thread_name, debug_states)) + update(thread_name) + true + case _ => false + } + } + private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean = { msg.properties match { @@ -61,15 +105,17 @@ } val functions = - Map(Markup.DEBUGGER_OUTPUT -> debugger_output _) + Map( + Markup.DEBUGGER_STATE -> debugger_state _, + Markup.DEBUGGER_OUTPUT -> debugger_output _) } /* protocol commands */ - def init(new_session: Session) + def init(session: Session) { - global_state.change(_.copy(session = new_session)) + global_state.change(_.set_session(session)) current_state().session.protocol_command("Debugger.init") } diff -r 144523e0678e -r 5510c8444bc4 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Aug 04 23:11:16 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Wed Aug 05 14:18:07 2015 +0200 @@ -94,7 +94,7 @@ val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) val new_output = // FIXME select by thread name (for ((_, results) <- Debugger.current_state.output; (_, tree) <- results.iterator) - yield tree).toList + yield tree).toList ::: List(XML.Text(Debugger.current_state.threads.toString)) if (new_output != current_output) pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))