# HG changeset patch
# User wenzelm
# Date 1448133232 -3600
# Node ID 5f5ff1eab407c874057d1eb86791b347662530b9
# Parent  6f1a84d78865dd2e350c1884e765c17b60497e46
double flush to ensure persistent "state" output is reset;
tuned GUI;

diff -r 6f1a84d78865 -r 5f5ff1eab407 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Sat Nov 21 20:12:36 2015 +0100
+++ b/src/Pure/PIDE/editor.scala	Sat Nov 21 20:13:52 2015 +0100
@@ -10,7 +10,7 @@
 abstract class Editor[Context]
 {
   def session: Session
-  def flush(): Unit
+  def flush(hidden: Boolean = true): Unit
   def invoke(): Unit
   def current_context: Context
   def current_node(context: Context): Option[Document.Node.Name]
diff -r 6f1a84d78865 -r 5f5ff1eab407 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Nov 21 20:12:36 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Nov 21 20:13:52 2015 +0100
@@ -113,7 +113,7 @@
     }
   }
 
-  def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
+  def node_perspective(hidden: Boolean, doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
   {
     GUI_Thread.require {}
 
@@ -140,7 +140,7 @@
 
       (reparse,
         Document.Node.Perspective(node_required,
-          Text.Perspective(document_view_ranges ::: load_ranges),
+          Text.Perspective(if (hidden) Nil else document_view_ranges ::: load_ranges),
           PIDE.editor.node_overlays(node_name)))
     }
     else (false, Document.Node.no_perspective_text)
@@ -232,21 +232,21 @@
     def is_pending(): Boolean = synchronized { pending_clear || pending.nonEmpty }
     def snapshot(): List[Text.Edit] = synchronized { pending.toList }
 
-    def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] = synchronized
-    {
-      GUI_Thread.require {}
+    def flushed_edits(hidden: Boolean, doc_blobs: Document.Blobs): List[Document.Edit_Text] =
+      synchronized {
+        GUI_Thread.require {}
 
-      val clear = pending_clear
-      val edits = snapshot()
-      val (reparse, perspective) = node_perspective(doc_blobs)
-      if (clear || reparse || edits.nonEmpty || last_perspective != perspective) {
-        pending_clear = false
-        pending.clear
-        last_perspective = perspective
-        node_edits(clear, edits, perspective)
+        val clear = pending_clear
+        val edits = snapshot()
+        val (reparse, perspective) = node_perspective(hidden, doc_blobs)
+        if (clear || reparse || edits.nonEmpty || last_perspective != perspective) {
+          pending_clear = false
+          pending.clear
+          last_perspective = perspective
+          node_edits(clear, edits, perspective)
+        }
+        else Nil
       }
-      else Nil
-    }
 
     def edit(clear: Boolean, e: Text.Edit): Unit = synchronized
     {
@@ -272,8 +272,8 @@
   def snapshot(): Document.Snapshot =
     session.snapshot(node_name, pending_edits.snapshot())
 
-  def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
-    pending_edits.flushed_edits(doc_blobs)
+  def flushed_edits(hidden: Boolean, doc_blobs: Document.Blobs): List[Document.Edit_Text] =
+    pending_edits.flushed_edits(hidden, doc_blobs)
 
 
   /* buffer listener */
diff -r 6f1a84d78865 -r 5f5ff1eab407 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Nov 21 20:12:36 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Nov 21 20:13:52 2015 +0100
@@ -28,7 +28,7 @@
   def remove_node(name: Document.Node.Name): Unit =
     GUI_Thread.require { removed_nodes += name }
 
-  override def flush()
+  override def flush(hidden: Boolean = false)
   {
     GUI_Thread.require {}
 
@@ -40,7 +40,7 @@
       (removed -- models.iterator.map(_.node_name)).toList.map(
         name => (name, Document.Node.no_perspective_text))
 
-    val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
+    val edits = models.flatMap(_.flushed_edits(hidden, doc_blobs)) ::: removed_perspective
     session.update(doc_blobs, edits)
   }
 
diff -r 6f1a84d78865 -r 5f5ff1eab407 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Nov 21 20:12:36 2015 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Nov 21 20:13:52 2015 +0100
@@ -91,12 +91,14 @@
     if (output_state != b) {
       PIDE.options.bool("editor_output_state") = b
       PIDE.session.update_options(PIDE.options.value)
+      PIDE.editor.flush(hidden = true)
+      PIDE.editor.flush()
     }
   }
 
-  private val output_state_button = new CheckBox("Output state")
+  private val output_state_button = new CheckBox("Proof state")
   {
-    tooltip = "Implicit output of proof state"
+    tooltip = "Output of proof state (normally shown on State panel)"
     reactions += { case ButtonClicked(_) => output_state = selected }
     selected = output_state
   }