1.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 16:10:46 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 16:46:09 2013 +0100
     1.3 @@ -21,14 +21,6 @@
     1.4  
     1.5  object Pretty_Text_Area
     1.6  {
     1.7 -  private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
     1.8 -    formatted_body: XML.Body): (String, Rendering) =
     1.9 -  {
    1.10 -    val (text, state) = Pretty_Text_Area.document_state(base_snapshot, base_results, formatted_body)
    1.11 -    val rendering = Rendering(state.snapshot(), PIDE.options.value)
    1.12 -    (text, rendering)
    1.13 -  }
    1.14 -
    1.15    private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
    1.16      formatted_body: XML.Body): (String, Document.State) =
    1.17    {
    1.18 @@ -50,6 +42,14 @@
    1.19  
    1.20      (command.source, state1)
    1.21    }
    1.22 +
    1.23 +  private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
    1.24 +    formatted_body: XML.Body): (String, Rendering) =
    1.25 +  {
    1.26 +    val (text, state) = document_state(base_snapshot, base_results, formatted_body)
    1.27 +    val rendering = Rendering(state.snapshot(), PIDE.options.value)
    1.28 +    (text, rendering)
    1.29 +  }
    1.30  }
    1.31  
    1.32  class Pretty_Text_Area(
    1.33 @@ -115,26 +115,35 @@
    1.34        val base_results = current_base_results
    1.35        val formatted_body = Pretty.formatted(current_body, margin, metric)
    1.36  
    1.37 +      def apply_result(result: (String, Rendering))
    1.38 +      {
    1.39 +        val (text, rendering) = result
    1.40 +        current_rendering = rendering
    1.41 +        JEdit_Lib.buffer_edit(getBuffer) {
    1.42 +          rich_text_area.active_reset()
    1.43 +          getBuffer.setReadOnly(false)
    1.44 +          getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
    1.45 +          setText(text)
    1.46 +          setCaretPosition(0)
    1.47 +          getBuffer.setReadOnly(true)
    1.48 +        }
    1.49 +      }
    1.50 +
    1.51        future_rendering.map(_.cancel(true))
    1.52 -      future_rendering = Some(default_thread_pool.submit(() =>
    1.53 -        {
    1.54 -          val (text, rendering) =
    1.55 -            try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
    1.56 -            catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
    1.57 -          Simple_Thread.interrupted_exception()
    1.58 -
    1.59 -          Swing_Thread.later {
    1.60 -            current_rendering = rendering
    1.61 -            JEdit_Lib.buffer_edit(getBuffer) {
    1.62 -              rich_text_area.active_reset()
    1.63 -              getBuffer.setReadOnly(false)
    1.64 -              getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
    1.65 -              setText(text)
    1.66 -              setCaretPosition(0)
    1.67 -              getBuffer.setReadOnly(true)
    1.68 -            }
    1.69 -          }
    1.70 -        }))
    1.71 +      if (XML.text_length(formatted_body) <= 1000) {
    1.72 +        apply_result(Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body))
    1.73 +        future_rendering = None
    1.74 +      }
    1.75 +      else {
    1.76 +        future_rendering = Some(default_thread_pool.submit(() =>
    1.77 +          {
    1.78 +            val result =
    1.79 +              try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
    1.80 +              catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
    1.81 +            Simple_Thread.interrupted_exception()
    1.82 +            Swing_Thread.later { apply_result(result) }
    1.83 +          }))
    1.84 +      }
    1.85      }
    1.86    }
    1.87