# HG changeset patch
# User wenzelm
# Date 1439221776 -7200
# Node ID 1f0d2bbcf38b9ab6114e610876e9e9780e944bcf
# Parent 8d00ff5a052e011f67a5fe618992a3dfe48e8378
added action to toggle breakpoints (on editor side);
diff -r 8d00ff5a052e -r 1f0d2bbcf38b src/Pure/Tools/debugger.ML
--- 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);
diff -r 8d00ff5a052e -r 1f0d2bbcf38b src/Pure/Tools/debugger.scala
--- 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)))
diff -r 8d00ff5a052e -r 1f0d2bbcf38b src/Tools/jEdit/etc/options
--- 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"
diff -r 8d00ff5a052e -r 1f0d2bbcf38b src/Tools/jEdit/src/actions.xml
--- 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();
+
+
+ isabelle.jedit.Isabelle.toggle_breakpoint(textArea);
+
+
isabelle.jedit.Isabelle.plugin_options(view);
diff -r 8d00ff5a052e -r 1f0d2bbcf38b src/Tools/jEdit/src/context_menu.scala
--- 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
}
}
-
diff -r 8d00ff5a052e -r 1f0d2bbcf38b src/Tools/jEdit/src/debugger_dockable.scala
--- 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)
diff -r 8d00ff5a052e -r 1f0d2bbcf38b src/Tools/jEdit/src/isabelle.scala
--- 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)
diff -r 8d00ff5a052e -r 1f0d2bbcf38b src/Tools/jEdit/src/jEdit.props
--- 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
diff -r 8d00ff5a052e -r 1f0d2bbcf38b src/Tools/jEdit/src/rendering.scala
--- 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")