set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;

--- a/src/Pure/PIDE/document.ML	Mon Aug 10 19:17:49 2015 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Aug 10 20:22:49 2015 +0200
@@ -21,6 +21,7 @@
   type blob_digest = (string * string option) Exn.result
   val define_command: Document_ID.command -> string -> blob_digest list -> int ->
     ((int * int) * string) list -> state -> state
+  val command_exec: state -> string -> Document_ID.command -> Command.exec option
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
   val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
@@ -406,6 +407,12 @@
 
 val the_command_name = #1 oo the_command;
 
+fun command_exec state node_name command_id =
+  let
+    val State {execution = {version_id, ...}, ...} = state;
+    val node = get_node (nodes_of (the_version state version_id)) node_name;
+  in the_entry node command_id end;
+
 end;
 
 

--- a/src/Pure/Tools/debugger.ML	Mon Aug 10 19:17:49 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 10 20:22:49 2015 +0200
@@ -234,12 +234,29 @@
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.breakpoint"
-    (fn [serial_string, b_string] =>
+    (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
       let
-        val serial = Markup.parse_int serial_string;
-        val b = Markup.parse_bool b_string;
-        (* FIXME *)
-      in () end);
+        val id = Markup.parse_int id0;
+        val breakpoint = Markup.parse_int breakpoint0;
+        val breakpoint_state = Markup.parse_bool breakpoint_state0;
+
+        fun err () = error ("Bad exec for command " ^ Markup.print_int id);
+      in
+        (case Document.command_exec (Document.state ()) node_name id of
+          SOME (eval, _) =>
+            if Command.eval_finished eval then
+              let
+                val st = Command.eval_result_state eval;
+                val ctxt = Toplevel.presentation_context_of st
+                  handle Toplevel.UNDEF => err ();
+              in
+                (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
+                  SOME (b, _) => b := breakpoint_state
+                | NONE => err ())
+              end
+            else err ()
+        | NONE => err ())
+      end);
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.cancel"

--- a/src/Pure/Tools/debugger.scala	Mon Aug 10 19:17:49 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 20:22:49 2015 +0200
@@ -29,12 +29,12 @@
     def inc_active: State = copy(active = active + 1)
     def dec_active: State = copy(active = active - 1)
 
-    def toggle_breakpoint(serial: Long): (Boolean, State) =
+    def toggle_breakpoint(breakpoint: Long): (Boolean, State) =
     {
       val active_breakpoints1 =
-        if (active_breakpoints(serial)) active_breakpoints - serial
-      else active_breakpoints + serial
-      (active_breakpoints1(serial), copy(active_breakpoints = active_breakpoints1))
+        if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint
+      else active_breakpoints + breakpoint
+      (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1))
     }
 
     def set_focus(new_focus: Option[Position.T]): State =
@@ -141,19 +141,23 @@
   def inc_active(): Unit = global_state.change(_.inc_active)
   def dec_active(): Unit = global_state.change(_.dec_active)
 
-  def breakpoint_active(serial: Long): Option[Boolean] =
+  def breakpoint_active(breakpoint: Long): Option[Boolean] =
   {
     val state = current_state()
-    if (state.active > 0) Some(state.active_breakpoints(serial)) else None
+    if (state.active > 0) Some(state.active_breakpoints(breakpoint)) else None
   }
 
-  def toggle_breakpoint(serial: Long)
+  def toggle_breakpoint(command: Command, breakpoint: Long)
   {
     global_state.change(state =>
     {
-      val (b, state1) = state.toggle_breakpoint(serial)
+      val (breakpoint_state, state1) = state.toggle_breakpoint(breakpoint)
       state1.session.protocol_command(
-        "Debugger.breakpoint", Properties.Value.Long(serial), Properties.Value.Boolean(b))
+        "Debugger.breakpoint",
+        Symbol.encode(command.node_name.node),
+        Document_ID(command.id),
+        Properties.Value.Long(breakpoint),
+        Properties.Value.Boolean(breakpoint_state))
       state1
     })
   }

--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 19:17:49 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 20:22:49 2015 +0200
@@ -41,15 +41,15 @@
 
   /* breakpoints */
 
-  def toggle_breakpoint(serial: Long)
+  def toggle_breakpoint(command: Command, breakpoint: Long)
   {
     GUI_Thread.require {}
 
-    Debugger.toggle_breakpoint(serial)
+    Debugger.toggle_breakpoint(command, breakpoint)
     jEdit.propertiesChanged()
   }
 
-  def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[Long] =
+  def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[(Command, Long)] =
   {
     GUI_Thread.require {}
 
@@ -57,7 +57,7 @@
       case Some(doc_view) =>
         val rendering = doc_view.get_rendering()
         val range = JEdit_Lib.point_range(text_area.getBuffer, offset)
-        rendering.breakpoints(range).headOption
+        rendering.breakpoint(range)
       case None => None
     }
   }

--- a/src/Tools/jEdit/src/isabelle.scala	Mon Aug 10 19:17:49 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Aug 10 20:22:49 2015 +0200
@@ -350,8 +350,9 @@
 
   def toggle_breakpoint(text_area: JEditTextArea)
   {
-    for (breakpoint <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition))
-      Debugger_Dockable.toggle_breakpoint(breakpoint)
+    for {
+      (command, serial) <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition)
+    } Debugger_Dockable.toggle_breakpoint(command, serial)
   }
 
 

--- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 19:17:49 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 20:22:49 2015 +0200
@@ -343,13 +343,18 @@
 
   /* breakpoints */
 
-  def breakpoints(range: Text.Range): List[Long] =
-    snapshot.select(range, Rendering.breakpoint_elements, _ =>
-      {
-        case Text.Info(_, XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _)) =>
-          Some(serial)
-        case _ => None
-      }).map(_.info)
+  def breakpoint(range: Text.Range): Option[(Command, Long)] =
+    if (snapshot.is_outdated) None
+    else
+      snapshot.select(range, Rendering.breakpoint_elements, command_states =>
+        {
+          case Text.Info(_, XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _)) =>
+            command_states match {
+              case st :: _ => Some((st.command, serial))
+              case _ => None
+            }
+          case _ => None
+        }).headOption.map(_.info)
 
 
   /* command status overview */