# HG changeset patch
# User wenzelm
# Date 1442684409 -7200
# Node ID dde5ecbd5e10f6ed920eef8d2ea296b198593916
# Parent  98eba31c51f880d9f68e04e05521215b8cf6c7d7
tuned;

diff -r 98eba31c51f8 -r dde5ecbd5e10 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Sep 19 19:34:51 2015 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Sep 19 19:40:09 2015 +0200
@@ -10,13 +10,12 @@
 
 import isabelle._
 
+import java.util.concurrent.{Future => JFuture}
 import java.awt.{Color, Font, Toolkit, Window}
 import java.awt.event.KeyEvent
 import javax.swing.JTextField
 import javax.swing.event.{DocumentListener, DocumentEvent}
 
-import java.util.concurrent.{Future => JFuture}
-
 import scala.swing.{Label, Component}
 import scala.util.matching.Regex
 
@@ -76,7 +75,7 @@
   private var current_base_results = Command.Results.empty
   private var current_rendering: Rendering =
     Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
-  private var future_rendering: Option[JFuture[Unit]] = None
+  private var future_refresh: Option[JFuture[Unit]] = None
 
   private val rich_text_area =
     new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
@@ -129,8 +128,8 @@
       val base_results = current_base_results
       val formatted_body = Pretty.formatted(current_body, margin, metric)
 
-      future_rendering.map(_.cancel(true))
-      future_rendering =
+      future_refresh.map(_.cancel(true))
+      future_refresh =
         Some(Simple_Thread.submit_task {
           val (text, rendering) =
             try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }