protocol support for thread debugger state;
authorwenzelm
Wed Aug 05 14:18:07 2015 +0200 (2015-08-05 ago)
changeset 608425510c8444bc4
parent 60841 144523e0678e
child 60843 9980f3bcdea2
protocol support for thread debugger state;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Tools/debugger.ML
src/Pure/Tools/debugger.scala
src/Tools/jEdit/src/debugger_dockable.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Tue Aug 04 23:11:16 2015 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Wed Aug 05 14:18:07 2015 +0200
     1.3 @@ -191,6 +191,7 @@
     1.4    val build_theories_result: string -> Properties.T
     1.5    val print_operationsN: string
     1.6    val print_operations: Properties.T
     1.7 +  val debugger_state: string -> Properties.T
     1.8    val debugger_output: string -> Properties.T
     1.9    val simp_trace_panelN: string
    1.10    val simp_trace_logN: string
    1.11 @@ -614,6 +615,7 @@
    1.12  
    1.13  (* debugger *)
    1.14  
    1.15 +fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)];
    1.16  fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)];
    1.17  
    1.18  
     2.1 --- a/src/Pure/PIDE/markup.scala	Tue Aug 04 23:11:16 2015 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Wed Aug 05 14:18:07 2015 +0200
     2.3 @@ -495,6 +495,16 @@
     2.4  
     2.5    /* debugger output */
     2.6  
     2.7 +  val DEBUGGER_STATE = "debugger_state"
     2.8 +  object Debugger_State
     2.9 +  {
    2.10 +    def unapply(props: Properties.T): Option[String] =
    2.11 +      props match {
    2.12 +        case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
    2.13 +        case _ => None
    2.14 +      }
    2.15 +  }
    2.16 +
    2.17    val DEBUGGER_OUTPUT = "debugger_output"
    2.18    object Debugger_Output
    2.19    {
     3.1 --- a/src/Pure/Tools/debugger.ML	Tue Aug 04 23:11:16 2015 +0200
     3.2 +++ b/src/Pure/Tools/debugger.ML	Wed Aug 05 14:18:07 2015 +0200
     3.3 @@ -40,27 +40,27 @@
     3.4  
     3.5  val global_state = Synchronized.var "Debugger.state" init_state;
     3.6  
     3.7 -fun cancel name =
     3.8 +fun cancel thread_name =
     3.9    Synchronized.change global_state (tap (fn State {threads, ...} =>
    3.10 -    (case Symtab.lookup threads name of
    3.11 +    (case Symtab.lookup threads thread_name of
    3.12        NONE => ()
    3.13      | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
    3.14  
    3.15 -fun input name msg =
    3.16 +fun input thread_name msg =
    3.17    Synchronized.change global_state (map_state (fn (threads, input) =>
    3.18 -    let val input' = Symtab.map_default (name, Queue.empty) (Queue.enqueue msg) input;
    3.19 +    let val input' = Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg) input;
    3.20      in (threads, input') end));
    3.21  
    3.22 -fun get_input name =
    3.23 +fun get_input thread_name =
    3.24    Synchronized.guarded_access global_state (fn State {threads, input} =>
    3.25 -    (case Symtab.lookup input name of
    3.26 +    (case Symtab.lookup input thread_name of
    3.27        NONE => NONE
    3.28      | SOME queue =>
    3.29          let
    3.30            val (msg, queue') = Queue.dequeue queue;
    3.31            val input' =
    3.32 -            if Queue.is_empty queue' then Symtab.delete_safe name input
    3.33 -            else Symtab.update (name, queue') input;
    3.34 +            if Queue.is_empty queue' then Symtab.delete_safe thread_name input
    3.35 +            else Symtab.update (thread_name, queue') input;
    3.36          in SOME (msg, make_state (threads, input')) end));
    3.37  
    3.38  
    3.39 @@ -84,13 +84,23 @@
    3.40  
    3.41  (* main entry point *)
    3.42  
    3.43 -fun debug_loop name =
    3.44 -  (case get_input name of
    3.45 +fun debugger_state thread_name =
    3.46 +  Output.protocol_message (Markup.debugger_state thread_name)
    3.47 +   [get_data ()
    3.48 +    |> map (fn st =>
    3.49 +      (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
    3.50 +       ML_Debugger.debug_function st))
    3.51 +    |> let open XML.Encode in list (pair properties string) end
    3.52 +    |> YXML.string_of_body];
    3.53 +
    3.54 +fun debugger_loop thread_name =
    3.55 +  (debugger_state thread_name;
    3.56 +   case get_input thread_name of
    3.57      ["continue"] => ()
    3.58    | bad =>
    3.59       (Output.system_message
    3.60          ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad);
    3.61 -      debug_loop name));
    3.62 +      debugger_loop thread_name));
    3.63  
    3.64  fun debugger cond =
    3.65    if debugging () orelse not (cond ()) orelse
    3.66 @@ -100,7 +110,7 @@
    3.67      with_debugging (fn () =>
    3.68        (case Simple_Thread.get_name () of
    3.69          NONE => ()
    3.70 -      | SOME name => debug_loop name));
    3.71 +      | SOME thread_name => debugger_loop thread_name));
    3.72  
    3.73  fun init () =
    3.74    ML_Debugger.on_breakpoint
    3.75 @@ -116,10 +126,10 @@
    3.76  
    3.77  val _ =
    3.78    Isabelle_Process.protocol_command "Debugger.cancel"
    3.79 -    (fn [name] => cancel name);
    3.80 +    (fn [thread_name] => cancel thread_name);
    3.81  
    3.82  val _ =
    3.83    Isabelle_Process.protocol_command "Debugger.input"
    3.84 -    (fn name :: msg => input name msg);
    3.85 +    (fn thread_name :: msg => input thread_name msg);
    3.86  
    3.87  end;
     4.1 --- a/src/Pure/Tools/debugger.scala	Tue Aug 04 23:11:16 2015 +0200
     4.2 +++ b/src/Pure/Tools/debugger.scala	Wed Aug 05 14:18:07 2015 +0200
     4.3 @@ -11,12 +11,37 @@
     4.4  {
     4.5    /* global state */
     4.6  
     4.7 +  sealed case class Debug_State(
     4.8 +    pos: Position.T,
     4.9 +    function: String)
    4.10 +
    4.11    sealed case class State(
    4.12      session: Session = new Session(Resources.empty),
    4.13 +    threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
    4.14      output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
    4.15    {
    4.16 -    def add_output(name: String, entry: Command.Results.Entry): State =
    4.17 -      copy(output = output + (name -> (output.getOrElse(name, Command.Results.empty) + entry)))
    4.18 +    def set_session(new_session: Session): State =
    4.19 +      copy(session = new_session)
    4.20 +
    4.21 +    def get_thread(thread_name: String): List[Debug_State] =
    4.22 +      threads.getOrElse(thread_name, Nil)
    4.23 +
    4.24 +    def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
    4.25 +      copy(threads = threads + (thread_name -> debug_states))
    4.26 +
    4.27 +    def get_output(thread_name: String): Command.Results =
    4.28 +      output.getOrElse(thread_name, Command.Results.empty)
    4.29 +
    4.30 +    def add_output(thread_name: String, entry: Command.Results.Entry): State =
    4.31 +      copy(output = output + (thread_name -> (get_output(thread_name) + entry)))
    4.32 +
    4.33 +    def clear_output(thread_name: String): State =
    4.34 +      copy(output = output - thread_name)
    4.35 +
    4.36 +    def purge(thread_name: String): State =
    4.37 +      if (get_thread(thread_name).isEmpty)
    4.38 +        copy(threads = threads - thread_name, output = output - thread_name)
    4.39 +      else this
    4.40    }
    4.41  
    4.42    private val global_state = Synchronized(State())
    4.43 @@ -41,6 +66,25 @@
    4.44        delay_update.invoke()
    4.45      }
    4.46  
    4.47 +    private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    4.48 +    {
    4.49 +      msg.properties match {
    4.50 +        case Markup.Debugger_State(thread_name) =>
    4.51 +          val msg_body = YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes))
    4.52 +          val debug_states =
    4.53 +          {
    4.54 +            import XML.Decode._
    4.55 +            list(pair(properties, Symbol.decode_string))(msg_body).map({
    4.56 +              case (pos, function) => Debug_State(pos, function)
    4.57 +            })
    4.58 +          }
    4.59 +          global_state.change(_.update_thread(thread_name, debug_states))
    4.60 +          update(thread_name)
    4.61 +          true
    4.62 +        case _ => false
    4.63 +      }
    4.64 +    }
    4.65 +
    4.66      private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    4.67      {
    4.68        msg.properties match {
    4.69 @@ -61,15 +105,17 @@
    4.70      }
    4.71  
    4.72      val functions =
    4.73 -      Map(Markup.DEBUGGER_OUTPUT -> debugger_output _)
    4.74 +      Map(
    4.75 +        Markup.DEBUGGER_STATE -> debugger_state _,
    4.76 +        Markup.DEBUGGER_OUTPUT -> debugger_output _)
    4.77    }
    4.78  
    4.79  
    4.80    /* protocol commands */
    4.81  
    4.82 -  def init(new_session: Session)
    4.83 +  def init(session: Session)
    4.84    {
    4.85 -    global_state.change(_.copy(session = new_session))
    4.86 +    global_state.change(_.set_session(session))
    4.87      current_state().session.protocol_command("Debugger.init")
    4.88    }
    4.89  
     5.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 04 23:11:16 2015 +0200
     5.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Wed Aug 05 14:18:07 2015 +0200
     5.3 @@ -94,7 +94,7 @@
     5.4      val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
     5.5      val new_output =  // FIXME select by thread name
     5.6        (for ((_, results) <- Debugger.current_state.output; (_, tree) <- results.iterator)
     5.7 -        yield tree).toList
     5.8 +        yield tree).toList ::: List(XML.Text(Debugger.current_state.threads.toString))
     5.9  
    5.10      if (new_output != current_output)
    5.11        pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))