--- 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)];
--- 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
{
--- 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;
--- 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")
}
--- 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))