added "check" button: adhoc change to full buffer perspective;
authorwenzelm
Wed Sep 07 11:17:19 2011 +0200 (2011-09-07)
changeset 4477647e8c8daccae
parent 44775 27930cf6f0f7
child 44777 1afb48f872ae
added "check" button: adhoc change to full buffer perspective;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Sep 07 11:00:39 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Sep 07 11:17:19 2011 +0200
     1.3 @@ -69,6 +69,8 @@
     1.4  
     1.5    /* perspective */
     1.6  
     1.7 +  def buffer_range(): Text.Range = Text.Range(0, (buffer.getLength - 1) max 0)
     1.8 +
     1.9    def perspective(): Text.Perspective =
    1.10    {
    1.11      Swing_Thread.require()
    1.12 @@ -136,6 +138,12 @@
    1.13      pending_edits.update_perspective()
    1.14    }
    1.15  
    1.16 +  def full_perspective()
    1.17 +  {
    1.18 +    pending_edits.flush()
    1.19 +    session.edit_node(name, node_header(), Text.Perspective(List(buffer_range())), Nil)
    1.20 +  }
    1.21 +
    1.22  
    1.23    /* snapshot */
    1.24  
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Sep 07 11:00:39 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Sep 07 11:17:19 2011 +0200
     2.3 @@ -118,7 +118,7 @@
     2.4    def perspective(): Text.Perspective =
     2.5    {
     2.6      Swing_Thread.require()
     2.7 -    val buffer_range = Text.Range(0, (model.buffer.getLength - 1) max 0)
     2.8 +    val buffer_range = model.buffer_range()
     2.9      Text.Perspective(
    2.10        for {
    2.11          i <- 0 until text_area.getVisibleLines
     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Wed Sep 07 11:00:39 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Sep 07 11:17:19 2011 +0200
     3.3 @@ -66,6 +66,18 @@
     3.4    }
     3.5    cancel.tooltip = "Cancel current proof checking process"
     3.6  
     3.7 +  private val check = new Button("Check") {
     3.8 +    reactions +=
     3.9 +    {
    3.10 +      case ButtonClicked(_) =>
    3.11 +        Isabelle.document_model(view.getBuffer) match {
    3.12 +          case None =>
    3.13 +          case Some(model) => model.full_perspective()
    3.14 +        }
    3.15 +    }
    3.16 +  }
    3.17 +  check.tooltip = "Commence full proof checking of current buffer"
    3.18 +
    3.19    private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
    3.20    logic.listenTo(logic.selection)
    3.21    logic.reactions += {
    3.22 @@ -73,7 +85,7 @@
    3.23    }
    3.24  
    3.25    private val controls =
    3.26 -    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, cancel, logic)
    3.27 +    new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
    3.28    add(controls.peer, BorderLayout.NORTH)
    3.29  
    3.30