added action to toggle breakpoints (on editor side);

--- a/src/Pure/Tools/debugger.ML	Mon Aug 10 16:14:50 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 10 17:49:36 2015 +0200
@@ -233,6 +233,15 @@
     (fn [] => init ());
 
 val _ =
+  Isabelle_Process.protocol_command "Debugger.breakpoint"
+    (fn [serial_string, b_string] =>
+      let
+        val serial = Markup.parse_int serial_string;
+        val b = Markup.parse_bool b_string;
+        (* FIXME *)
+      in () end);
+
+val _ =
   Isabelle_Process.protocol_command "Debugger.cancel"
     (fn [thread_name] => cancel thread_name);
 

--- a/src/Pure/Tools/debugger.scala	Mon Aug 10 16:14:50 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 17:49:36 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): State =
+    def toggle_breakpoint(serial: Long): (Boolean, State) =
     {
       val active_breakpoints1 =
         if (active_breakpoints(serial)) active_breakpoints - serial
       else active_breakpoints + serial
-      copy(active_breakpoints = active_breakpoints1)
+      (active_breakpoints1(serial), copy(active_breakpoints = active_breakpoints1))
     }
 
     def set_focus(new_focus: Option[Position.T]): State =
@@ -147,8 +147,16 @@
     if (state.active > 0) Some(state.active_breakpoints(serial)) else None
   }
 
-  def toggle_breakpoint(serial: Long): Unit =
-    global_state.change(_.toggle_breakpoint(serial))
+  def toggle_breakpoint(serial: Long)
+  {
+    global_state.change(state =>
+    {
+      val (b, state1) = state.toggle_breakpoint(serial)
+      state1.session.protocol_command(
+        "Debugger.breakpoint", Properties.Value.Long(serial), Properties.Value.Boolean(b))
+      state1
+    })
+  }
 
   def focus(new_focus: Option[Position.T]): Boolean =
     global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus)))

--- a/src/Tools/jEdit/etc/options	Mon Aug 10 16:14:50 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Aug 10 17:49:36 2015 +0200
@@ -100,8 +100,8 @@
 option spell_checker_color : string = "0000FFFF"
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
-option breakpoint_color : string = "00CC0032"
-option breakpoint_active_color : string = "00CC0064"
+option breakpoint_color : string = "00CC0019"
+option breakpoint_active_color : string = "00CC0050"
 option quoted_color : string = "8B8B8B19"
 option antiquoted_color : string = "FFC83219"
 option antiquote_color : string = "6600CCFF"

--- a/src/Tools/jEdit/src/actions.xml	Mon Aug 10 16:14:50 2015 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Mon Aug 10 17:49:36 2015 +0200
@@ -122,6 +122,11 @@
 	    isabelle.jedit.Isabelle.reset_dictionary();
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.toggle-breakpoint">
+	  <CODE>
+	    isabelle.jedit.Isabelle.toggle_breakpoint(textArea);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.options">
 	  <CODE>
 	    isabelle.jedit.Isabelle.plugin_options(view);

--- a/src/Tools/jEdit/src/context_menu.scala	Mon Aug 10 16:14:50 2015 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala	Mon Aug 10 17:49:36 2015 +0200
@@ -27,7 +27,9 @@
     val items1 =
       if (evt != null && evt.getSource == text_area.getPainter) {
         val offset = text_area.xyToOffset(evt.getX, evt.getY)
-        if (offset >= 0) Spell_Checker.context_menu(text_area, offset)
+        if (offset >= 0)
+          Spell_Checker.context_menu(text_area, offset) :::
+          Debugger_Dockable.context_menu(text_area, offset)
         else Nil
       }
       else Nil
@@ -38,4 +40,3 @@
     if (items.isEmpty) null else items.toArray
   }
 }
-

--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 16:14:50 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 17:49:36 2015 +0200
@@ -12,7 +12,7 @@
 import java.awt.{BorderLayout, Dimension}
 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter,
   FocusAdapter, FocusEvent}
-import javax.swing.{JTree, JScrollPane}
+import javax.swing.{JTree, JScrollPane, JMenuItem}
 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
 
@@ -20,10 +20,14 @@
 import scala.swing.event.ButtonClicked
 
 import org.gjt.sp.jedit.{jEdit, View}
+import org.gjt.sp.jedit.menu.EnhancedMenuItem
+import org.gjt.sp.jedit.textarea.JEditTextArea
 
 
 object Debugger_Dockable
 {
+  /* state entries */
+
   sealed case class Thread_Entry(thread_name: String, debug_states: List[Debugger.Debug_State])
   {
     override def toString: String = thread_name
@@ -33,6 +37,41 @@
   {
     override def toString: String = debug_state.function
   }
+
+
+  /* breakpoints */
+
+  def toggle_breakpoint(serial: Long)
+  {
+    GUI_Thread.require {}
+
+    Debugger.toggle_breakpoint(serial)
+    jEdit.propertiesChanged()
+  }
+
+  def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[Long] =
+  {
+    GUI_Thread.require {}
+
+    PIDE.document_view(text_area) match {
+      case Some(doc_view) =>
+        val rendering = doc_view.get_rendering()
+        val range = JEdit_Lib.point_range(text_area.getBuffer, offset)
+        rendering.breakpoints(range).headOption
+      case None => None
+    }
+  }
+
+
+  /* context menu */
+
+  def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
+    if (get_breakpoint(text_area, offset).isDefined) {
+      val context = jEdit.getActionContext()
+      val name = "isabelle.toggle-breakpoint"
+      List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context))
+    }
+    else Nil
 }
 
 class Debugger_Dockable(view: View, position: String) extends Dockable(view, position)

--- a/src/Tools/jEdit/src/isabelle.scala	Mon Aug 10 16:14:50 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Aug 10 17:49:36 2015 +0200
@@ -346,6 +346,15 @@
   }
 
 
+  /* debugger */
+
+  def toggle_breakpoint(text_area: JEditTextArea)
+  {
+    for (breakpoint <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition))
+      Debugger_Dockable.toggle_breakpoint(breakpoint)
+  }
+
+
   /* plugin options */
 
   def plugin_options(frame: Frame)

--- a/src/Tools/jEdit/src/jEdit.props	Mon Aug 10 16:14:50 2015 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Aug 10 17:49:36 2015 +0200
@@ -226,6 +226,7 @@
 isabelle.reset-words.label=Reset non-permanent words
 isabelle.set-continuous-checking.label=Set continuous checking
 isabelle.set-node-required.label=Set node required
+isabelle.toggle-breakpoint.label=Toggle Breakpoint
 isabelle.toggle-continuous-checking.label=Toggle continuous checking
 isabelle.toggle-continuous-checking.shortcut=C+e ENTER
 isabelle.toggle-node-required.label=Toggle node required

--- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 16:14:50 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 17:49:36 2015 +0200
@@ -149,6 +149,8 @@
 
   private val citation_elements = Markup.Elements(Markup.CITATION)
 
+  private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
+
   private val highlight_elements =
     Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
@@ -339,6 +341,17 @@
       }).headOption.map(_.info)
 
 
+  /* 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)
+
+
   /* command status overview */
 
   def overview_limit: Int = options.int("jedit_text_overview_limit")