# HG changeset patch
# User wenzelm
# Date 1315387039 -7200
# Node ID 47e8c8daccae7a94a07515ec5b30cc4336aa8415
# Parent  27930cf6f0f70e7fef0950ad013b7d85c7957a27
added "check" button: adhoc change to full buffer perspective;

diff -r 27930cf6f0f7 -r 47e8c8daccae src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Sep 07 11:00:39 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Sep 07 11:17:19 2011 +0200
@@ -69,6 +69,8 @@
 
   /* perspective */
 
+  def buffer_range(): Text.Range = Text.Range(0, (buffer.getLength - 1) max 0)
+
   def perspective(): Text.Perspective =
   {
     Swing_Thread.require()
@@ -136,6 +138,12 @@
     pending_edits.update_perspective()
   }
 
+  def full_perspective()
+  {
+    pending_edits.flush()
+    session.edit_node(name, node_header(), Text.Perspective(List(buffer_range())), Nil)
+  }
+
 
   /* snapshot */
 
diff -r 27930cf6f0f7 -r 47e8c8daccae src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Sep 07 11:00:39 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Sep 07 11:17:19 2011 +0200
@@ -118,7 +118,7 @@
   def perspective(): Text.Perspective =
   {
     Swing_Thread.require()
-    val buffer_range = Text.Range(0, (model.buffer.getLength - 1) max 0)
+    val buffer_range = model.buffer_range()
     Text.Perspective(
       for {
         i <- 0 until text_area.getVisibleLines
diff -r 27930cf6f0f7 -r 47e8c8daccae src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Wed Sep 07 11:00:39 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Sep 07 11:17:19 2011 +0200
@@ -66,6 +66,18 @@
   }
   cancel.tooltip = "Cancel current proof checking process"
 
+  private val check = new Button("Check") {
+    reactions +=
+    {
+      case ButtonClicked(_) =>
+        Isabelle.document_model(view.getBuffer) match {
+          case None =>
+          case Some(model) => model.full_perspective()
+        }
+    }
+  }
+  check.tooltip = "Commence full proof checking of current buffer"
+
   private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
   logic.listenTo(logic.selection)
   logic.reactions += {
@@ -73,7 +85,7 @@
   }
 
   private val controls =
-    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, cancel, logic)
+    new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
   add(controls.peer, BorderLayout.NORTH)