# HG changeset patch
# User wenzelm
# Date 1442689657 -7200
# Node ID b9d69001824e1cfb35165da50f41b7fcb54a549d
# Parent  67c20ce71d22516ea90b2960154af7abefed1134
straight-forward refresh, without special preconditions;
eliminated somewhat expensive eq_content;

diff -r 67c20ce71d22 -r b9d69001824e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Sep 19 20:47:11 2015 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Sep 19 21:07:37 2015 +0200
@@ -150,12 +150,6 @@
       else Some(new State(other_command, Nil, Results.empty, markups1))
     }
 
-    def eq_content(other: State): Boolean =
-      command.source == other.command.source &&
-      status == other.status &&
-      results == other.results &&
-      markups == other.markups
-
     private def add_status(st: Markup): State =
       copy(status = st :: status)
 
diff -r 67c20ce71d22 -r b9d69001824e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Sep 19 20:47:11 2015 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Sep 19 21:07:37 2015 +0200
@@ -452,7 +452,6 @@
     val node: Node
     val load_commands: List[Command]
     def is_loaded: Boolean
-    def eq_content(other: Snapshot): Boolean
 
     def cumulate[A](
       range: Text.Range,
@@ -794,23 +793,6 @@
 
         val is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
 
-        def eq_content(other: Snapshot): Boolean =
-        {
-          def eq_commands(commands: (Command, Command)): Boolean =
-          {
-            val states1 = state.command_states(version, commands._1)
-            val states2 = other.state.command_states(other.version, commands._2)
-            states1.length == states2.length &&
-            (states1 zip states2).forall({ case (st1, st2) => st1 eq_content st2 })
-          }
-
-          !is_outdated && !other.is_outdated &&
-          node.commands.size == other.node.commands.size &&
-          (node.commands.iterator zip other.node.commands.iterator).forall(eq_commands) &&
-          load_commands.length == other.load_commands.length &&
-          (load_commands zip other.load_commands).forall(eq_commands)
-        }
-
 
         /* cumulate markup */
 
diff -r 67c20ce71d22 -r b9d69001824e src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Sat Sep 19 20:47:11 2015 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Sat Sep 19 21:07:37 2015 +0200
@@ -70,8 +70,6 @@
 
   /* synchronous painting */
 
-  private var current_snapshot = Document.Snapshot.init
-  private var current_options = PIDE.options.value
   private var current_overview = Overview()
   private var current_colors: List[(Color, Int, Int)] = Nil
 
@@ -83,11 +81,9 @@
     doc_view.rich_text_area.robust_body(()) {
       JEdit_Lib.buffer_lock(buffer) {
         val rendering = doc_view.get_rendering()
-        val snapshot = rendering.snapshot
-        val options = rendering.options
         val overview = get_overview()
 
-        if (!snapshot.is_outdated && overview == current_overview) {
+        if (!rendering.snapshot.is_outdated && overview == current_overview) {
           gfx.setColor(getBackground)
           gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
           for ((color, h, h1) <- current_colors) {
@@ -118,15 +114,9 @@
       doc_view.rich_text_area.robust_body(()) {
         JEdit_Lib.buffer_lock(buffer) {
           val rendering = doc_view.get_rendering()
-          val snapshot = rendering.snapshot
-          val options = rendering.options
           val overview = get_overview()
 
-          if (!snapshot.is_outdated &&
-              (overview != current_overview ||
-               !(snapshot eq_content current_snapshot) ||
-               !(options eq current_options)))
-          {
+          if (!rendering.snapshot.is_outdated) {
             cancel()
 
             val line_offsets =
@@ -175,8 +165,6 @@
                 val new_colors = loop(0, 0, 0, 0, Nil)
 
                 GUI_Thread.later {
-                  current_snapshot = snapshot
-                  current_options = options
                   current_overview = overview
                   current_colors = new_colors
                   repaint()