support declarative editor_execution_range, instead of old-style check/cancel buttons;
authorwenzelm
Mon Jul 29 12:50:16 2013 +0200 (2013-07-29)
changeset 52759a20631db9c8a
parent 52753 1165f78c16d8
child 52760 8517172b9626
support declarative editor_execution_range, instead of old-style check/cancel buttons;
etc/options
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/etc/options	Sun Jul 28 20:51:15 2013 +0200
     1.2 +++ b/etc/options	Mon Jul 29 12:50:16 2013 +0200
     1.3 @@ -126,6 +126,9 @@
     1.4  public option editor_execution_priority : int = -2
     1.5    -- "execution priority of main document structure (e.g. 0, -1, -2)"
     1.6  
     1.7 +option editor_execution_range : string = "visible"
     1.8 +  -- "range of continuous document processing: all, none, visible"
     1.9 +
    1.10  
    1.11  section "Miscellaneous Tools"
    1.12  
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Jul 28 20:51:15 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Jul 29 12:50:16 2013 +0200
     2.3 @@ -82,11 +82,17 @@
     2.4    def node_perspective(): Text.Perspective =
     2.5    {
     2.6      Swing_Thread.require()
     2.7 -    Text.Perspective(
     2.8 -      for {
     2.9 -        doc_view <- PIDE.document_views(buffer)
    2.10 -        range <- doc_view.perspective().ranges
    2.11 -      } yield range)
    2.12 +
    2.13 +    PIDE.execution_range() match {
    2.14 +      case PIDE.Execution_Range.ALL => Text.Perspective.full
    2.15 +      case PIDE.Execution_Range.NONE => Text.Perspective.empty
    2.16 +      case PIDE.Execution_Range.VISIBLE =>
    2.17 +        Text.Perspective(
    2.18 +          for {
    2.19 +            doc_view <- PIDE.document_views(buffer)
    2.20 +            range <- doc_view.perspective().ranges
    2.21 +          } yield range)
    2.22 +    }
    2.23    }
    2.24  
    2.25  
    2.26 @@ -126,7 +132,7 @@
    2.27  
    2.28      def snapshot(): List[Text.Edit] = pending.toList
    2.29  
    2.30 -    def flush()
    2.31 +    def flushed_edits(): List[Document.Edit_Text] =
    2.32      {
    2.33        Swing_Thread.require()
    2.34  
    2.35 @@ -135,10 +141,13 @@
    2.36        if (!edits.isEmpty || last_perspective != new_perspective) {
    2.37          pending.clear
    2.38          last_perspective = new_perspective
    2.39 -        session.update(node_edits(new_perspective, edits))
    2.40 +        node_edits(new_perspective, edits)
    2.41        }
    2.42 +      else Nil
    2.43      }
    2.44  
    2.45 +    def flush(): Unit = session.update(flushed_edits())
    2.46 +
    2.47      private val delay_flush =
    2.48        Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    2.49  
    2.50 @@ -149,11 +158,6 @@
    2.51        delay_flush.invoke()
    2.52      }
    2.53  
    2.54 -    def update_perspective()
    2.55 -    {
    2.56 -      delay_flush.invoke()
    2.57 -    }
    2.58 -
    2.59      def init()
    2.60      {
    2.61        flush()
    2.62 @@ -167,17 +171,8 @@
    2.63      }
    2.64    }
    2.65  
    2.66 -  def update_perspective()
    2.67 -  {
    2.68 -    Swing_Thread.require()
    2.69 -    pending_edits.update_perspective()
    2.70 -  }
    2.71 -
    2.72 -  def full_perspective()
    2.73 -  {
    2.74 -    pending_edits.flush()
    2.75 -    session.update(node_edits(Text.Perspective(List(JEdit_Lib.buffer_range(buffer))), Nil))
    2.76 -  }
    2.77 +  def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
    2.78 +  def flush(): Unit = pending_edits.flush()
    2.79  
    2.80  
    2.81    /* snapshot */
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Jul 28 20:51:15 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 29 12:50:16 2013 +0200
     3.3 @@ -100,7 +100,7 @@
     3.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     3.5      {
     3.6        // no robust_body
     3.7 -      model.update_perspective()
     3.8 +      model.flush()
     3.9      }
    3.10    }
    3.11  
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Jul 28 20:51:15 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Jul 29 12:50:16 2013 +0200
     4.3 @@ -117,17 +117,43 @@
     4.4    }
     4.5  
     4.6  
     4.7 -  /* full checking */
     4.8 +  /* execution range */
     4.9 +
    4.10 +  object Execution_Range extends Enumeration {
    4.11 +    val ALL = Value("all")
    4.12 +    val NONE = Value("none")
    4.13 +    val VISIBLE = Value("visible")
    4.14 +  }
    4.15  
    4.16 -  def check_buffer(buffer: Buffer)
    4.17 +  def execution_range(): Execution_Range.Value =
    4.18 +    options.string("editor_execution_range") match {
    4.19 +      case "all" => Execution_Range.ALL
    4.20 +      case "none" => Execution_Range.NONE
    4.21 +      case "visible" => Execution_Range.VISIBLE
    4.22 +      case s => error("Bad value for option \"editor_execution_range\": " + quote(s))
    4.23 +    }
    4.24 +
    4.25 +  def update_execution_range(range: Execution_Range.Value)
    4.26    {
    4.27 -    document_model(buffer) match {
    4.28 -      case Some(model) => model.full_perspective()
    4.29 -      case None =>
    4.30 +    Swing_Thread.require()
    4.31 +
    4.32 +    if (options.string("editor_execution_range") != range.toString) {
    4.33 +      options.string("editor_execution_range") = range.toString
    4.34 +      PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
    4.35 +
    4.36 +      val edits =
    4.37 +        (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    4.38 +          case (edits, buffer) =>
    4.39 +            JEdit_Lib.buffer_lock(buffer) {
    4.40 +              document_model(buffer) match {
    4.41 +                case Some(model) => model.flushed_edits() ::: edits
    4.42 +                case None => edits
    4.43 +              }
    4.44 +            }
    4.45 +          }
    4.46 +      PIDE.session.update(edits)
    4.47      }
    4.48    }
    4.49 -
    4.50 -  def cancel_execution() { PIDE.session.cancel_execution() }
    4.51  }
    4.52  
    4.53  
     5.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Jul 28 20:51:15 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Jul 29 12:50:16 2013 +0200
     5.3 @@ -10,13 +10,14 @@
     5.4  import isabelle._
     5.5  
     5.6  import scala.actors.Actor._
     5.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
     5.8 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component,
     5.9 +  BoxPanel, Orientation, RadioButton, ButtonGroup}
    5.10  import scala.swing.event.{ButtonClicked, MouseClicked}
    5.11  
    5.12  import java.lang.System
    5.13 -import java.awt.{BorderLayout, Graphics2D, Insets}
    5.14 +import java.awt.{BorderLayout, Graphics2D, Insets, Color}
    5.15  import javax.swing.{JList, BorderFactory}
    5.16 -import javax.swing.border.{BevelBorder, SoftBevelBorder}
    5.17 +import javax.swing.border.{BevelBorder, SoftBevelBorder, LineBorder}
    5.18  
    5.19  import org.gjt.sp.jedit.{View, jEdit}
    5.20  
    5.21 @@ -54,20 +55,33 @@
    5.22      Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
    5.23    }
    5.24  
    5.25 -  private val cancel = new Button("Cancel") {
    5.26 -    reactions += { case ButtonClicked(_) => PIDE.cancel_execution() }
    5.27 -  }
    5.28 -  cancel.tooltip = "Cancel current checking process"
    5.29 +  private val execution_range = new BoxPanel(Orientation.Horizontal) {
    5.30 +    private def button(range: PIDE.Execution_Range.Value): RadioButton =
    5.31 +      new RadioButton(range.toString) {
    5.32 +        reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
    5.33 +      }
    5.34 +    private val label = new Label("Range:") { tooltip = "range of continuous document processing" }
    5.35 +    private val b1 = button(PIDE.Execution_Range.ALL)
    5.36 +    private val b2 = button(PIDE.Execution_Range.NONE)
    5.37 +    private val b3 = button(PIDE.Execution_Range.VISIBLE)
    5.38 +    private val group = new ButtonGroup(b1, b2, b3)
    5.39 +    contents ++= List(label, b1, b2, b3)
    5.40 +    border = new LineBorder(Color.GRAY)
    5.41  
    5.42 -  private val check = new Button("Check") {
    5.43 -    reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) }
    5.44 +    def load()
    5.45 +    {
    5.46 +      PIDE.execution_range() match {
    5.47 +        case PIDE.Execution_Range.ALL => group.select(b1)
    5.48 +        case PIDE.Execution_Range.NONE => group.select(b2)
    5.49 +        case PIDE.Execution_Range.VISIBLE => group.select(b3)
    5.50 +      }
    5.51 +    }
    5.52    }
    5.53 -  check.tooltip = "Commence full checking of current buffer"
    5.54  
    5.55    private val logic = Isabelle_Logic.logic_selector(true)
    5.56  
    5.57    private val controls =
    5.58 -    new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
    5.59 +    new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic)
    5.60    add(controls.peer, BorderLayout.NORTH)
    5.61  
    5.62  
    5.63 @@ -156,7 +170,11 @@
    5.64        react {
    5.65          case phase: Session.Phase => handle_phase(phase)
    5.66  
    5.67 -        case _: Session.Global_Options => Swing_Thread.later { logic.load () }
    5.68 +        case _: Session.Global_Options =>
    5.69 +          Swing_Thread.later {
    5.70 +            execution_range.load()
    5.71 +            logic.load ()
    5.72 +          }
    5.73  
    5.74          case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
    5.75