# HG changeset patch
# User wenzelm
# Date 1364069583 -3600
# Node ID 979592b765f85cedf8e182a56271634b5b52166c
# Parent  7e8968c9a549a8416c77cfe110dbe35027d52fe7
reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;

diff -r 7e8968c9a549 -r 979592b765f8 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 19:54:15 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 21:13:03 2013 +0100
@@ -116,35 +116,26 @@
       val base_results = current_base_results
       val formatted_body = Pretty.formatted(current_body, margin, metric)
 
-      def apply_result(result: (String, Rendering))
-      {
-        val (text, rendering) = result
-        current_rendering = rendering
-        JEdit_Lib.buffer_edit(getBuffer) {
-          rich_text_area.active_reset()
-          getBuffer.setReadOnly(false)
-          getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
-          setText(text)
-          setCaretPosition(0)
-          getBuffer.setReadOnly(true)
-        }
-      }
+      future_rendering.map(_.cancel(true))
+      future_rendering = Some(default_thread_pool.submit(() =>
+        {
+          val (text, rendering) =
+            try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
+            catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
+          Simple_Thread.interrupted_exception()
 
-      future_rendering.map(_.cancel(true))
-      if (XML.text_length(formatted_body) <= 1000) {
-        apply_result(Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body))
-        future_rendering = None
-      }
-      else {
-        future_rendering = Some(default_thread_pool.submit(() =>
-          {
-            val result =
-              try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
-              catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
-            Simple_Thread.interrupted_exception()
-            Swing_Thread.later { apply_result(result) }
-          }))
-      }
+          Swing_Thread.later {
+            current_rendering = rendering
+            JEdit_Lib.buffer_edit(getBuffer) {
+              rich_text_area.active_reset()
+              getBuffer.setReadOnly(false)
+              getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
+              setText(text)
+              setCaretPosition(0)
+              getBuffer.setReadOnly(true)
+            }
+          }
+        }))
     }
   }