# HG changeset patch # User wenzelm # Date 1375095016 -7200 # Node ID a20631db9c8a884da3217c2f54204b63ac61b0ca # Parent 1165f78c16d8f07a4a7995155ea9d6ef2ddc75a2 support declarative editor_execution_range, instead of old-style check/cancel buttons; diff -r 1165f78c16d8 -r a20631db9c8a etc/options --- 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" diff -r 1165f78c16d8 -r a20631db9c8a src/Tools/jEdit/src/document_model.scala --- 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 */ diff -r 1165f78c16d8 -r a20631db9c8a src/Tools/jEdit/src/document_view.scala --- 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() } } diff -r 1165f78c16d8 -r a20631db9c8a src/Tools/jEdit/src/plugin.scala --- 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() } } diff -r 1165f78c16d8 -r a20631db9c8a src/Tools/jEdit/src/theories_dockable.scala --- 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))