--- 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 */
--- 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
--- 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)