support declarative editor_execution_range, instead of old-style check/cancel buttons;
--- a/etc/options Sun Jul 28 20:51:15 2013 +0200
+++ b/etc/options Mon Jul 29 12:50:16 2013 +0200
@@ -126,6 +126,9 @@
public option editor_execution_priority : int = -2
-- "execution priority of main document structure (e.g. 0, -1, -2)"
+option editor_execution_range : string = "visible"
+ -- "range of continuous document processing: all, none, visible"
+
section "Miscellaneous Tools"
--- a/src/Tools/jEdit/src/document_model.scala Sun Jul 28 20:51:15 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Jul 29 12:50:16 2013 +0200
@@ -82,11 +82,17 @@
def node_perspective(): Text.Perspective =
{
Swing_Thread.require()
- Text.Perspective(
- for {
- doc_view <- PIDE.document_views(buffer)
- range <- doc_view.perspective().ranges
- } yield range)
+
+ PIDE.execution_range() match {
+ case PIDE.Execution_Range.ALL => Text.Perspective.full
+ case PIDE.Execution_Range.NONE => Text.Perspective.empty
+ case PIDE.Execution_Range.VISIBLE =>
+ Text.Perspective(
+ for {
+ doc_view <- PIDE.document_views(buffer)
+ range <- doc_view.perspective().ranges
+ } yield range)
+ }
}
@@ -126,7 +132,7 @@
def snapshot(): List[Text.Edit] = pending.toList
- def flush()
+ def flushed_edits(): List[Document.Edit_Text] =
{
Swing_Thread.require()
@@ -135,10 +141,13 @@
if (!edits.isEmpty || last_perspective != new_perspective) {
pending.clear
last_perspective = new_perspective
- session.update(node_edits(new_perspective, edits))
+ node_edits(new_perspective, edits)
}
+ else Nil
}
+ def flush(): Unit = session.update(flushed_edits())
+
private val delay_flush =
Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
@@ -149,11 +158,6 @@
delay_flush.invoke()
}
- def update_perspective()
- {
- delay_flush.invoke()
- }
-
def init()
{
flush()
@@ -167,17 +171,8 @@
}
}
- def update_perspective()
- {
- Swing_Thread.require()
- pending_edits.update_perspective()
- }
-
- def full_perspective()
- {
- pending_edits.flush()
- session.update(node_edits(Text.Perspective(List(JEdit_Lib.buffer_range(buffer))), Nil))
- }
+ def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
+ def flush(): Unit = pending_edits.flush()
/* snapshot */
--- a/src/Tools/jEdit/src/document_view.scala Sun Jul 28 20:51:15 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Mon Jul 29 12:50:16 2013 +0200
@@ -100,7 +100,7 @@
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
// no robust_body
- model.update_perspective()
+ model.flush()
}
}
--- a/src/Tools/jEdit/src/plugin.scala Sun Jul 28 20:51:15 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Jul 29 12:50:16 2013 +0200
@@ -117,17 +117,43 @@
}
- /* full checking */
+ /* execution range */
+
+ object Execution_Range extends Enumeration {
+ val ALL = Value("all")
+ val NONE = Value("none")
+ val VISIBLE = Value("visible")
+ }
- def check_buffer(buffer: Buffer)
+ def execution_range(): Execution_Range.Value =
+ options.string("editor_execution_range") match {
+ case "all" => Execution_Range.ALL
+ case "none" => Execution_Range.NONE
+ case "visible" => Execution_Range.VISIBLE
+ case s => error("Bad value for option \"editor_execution_range\": " + quote(s))
+ }
+
+ def update_execution_range(range: Execution_Range.Value)
{
- document_model(buffer) match {
- case Some(model) => model.full_perspective()
- case None =>
+ Swing_Thread.require()
+
+ if (options.string("editor_execution_range") != range.toString) {
+ options.string("editor_execution_range") = range.toString
+ PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+
+ val edits =
+ (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
+ case (edits, buffer) =>
+ JEdit_Lib.buffer_lock(buffer) {
+ document_model(buffer) match {
+ case Some(model) => model.flushed_edits() ::: edits
+ case None => edits
+ }
+ }
+ }
+ PIDE.session.update(edits)
}
}
-
- def cancel_execution() { PIDE.session.cancel_execution() }
}
--- a/src/Tools/jEdit/src/theories_dockable.scala Sun Jul 28 20:51:15 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Jul 29 12:50:16 2013 +0200
@@ -10,13 +10,14 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component,
+ BoxPanel, Orientation, RadioButton, ButtonGroup}
import scala.swing.event.{ButtonClicked, MouseClicked}
import java.lang.System
-import java.awt.{BorderLayout, Graphics2D, Insets}
+import java.awt.{BorderLayout, Graphics2D, Insets, Color}
import javax.swing.{JList, BorderFactory}
-import javax.swing.border.{BevelBorder, SoftBevelBorder}
+import javax.swing.border.{BevelBorder, SoftBevelBorder, LineBorder}
import org.gjt.sp.jedit.{View, jEdit}
@@ -54,20 +55,33 @@
Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
}
- private val cancel = new Button("Cancel") {
- reactions += { case ButtonClicked(_) => PIDE.cancel_execution() }
- }
- cancel.tooltip = "Cancel current checking process"
+ private val execution_range = new BoxPanel(Orientation.Horizontal) {
+ private def button(range: PIDE.Execution_Range.Value): RadioButton =
+ new RadioButton(range.toString) {
+ reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
+ }
+ private val label = new Label("Range:") { tooltip = "range of continuous document processing" }
+ private val b1 = button(PIDE.Execution_Range.ALL)
+ private val b2 = button(PIDE.Execution_Range.NONE)
+ private val b3 = button(PIDE.Execution_Range.VISIBLE)
+ private val group = new ButtonGroup(b1, b2, b3)
+ contents ++= List(label, b1, b2, b3)
+ border = new LineBorder(Color.GRAY)
- private val check = new Button("Check") {
- reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) }
+ def load()
+ {
+ PIDE.execution_range() match {
+ case PIDE.Execution_Range.ALL => group.select(b1)
+ case PIDE.Execution_Range.NONE => group.select(b2)
+ case PIDE.Execution_Range.VISIBLE => group.select(b3)
+ }
+ }
}
- check.tooltip = "Commence full checking of current buffer"
private val logic = Isabelle_Logic.logic_selector(true)
private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
+ new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic)
add(controls.peer, BorderLayout.NORTH)
@@ -156,7 +170,11 @@
react {
case phase: Session.Phase => handle_phase(phase)
- case _: Session.Global_Options => Swing_Thread.later { logic.load () }
+ case _: Session.Global_Options =>
+ Swing_Thread.later {
+ execution_range.load()
+ logic.load ()
+ }
case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))