apply small result immediately, to avoid visible delay of text update after window move;
authorwenzelm
Sat Mar 23 16:46:09 2013 +0100 (2013-03-23 ago)
changeset 514955944b20c41bf
parent 51494 8f3d1a7bee26
child 51496 cb677987b7e3
apply small result immediately, to avoid visible delay of text update after window move;
src/Tools/jEdit/src/pretty_text_area.scala
     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 -      future_rendering.map(_.cancel(true))
    1.38 -      future_rendering = Some(default_thread_pool.submit(() =>
    1.39 -        {
    1.40 -          val (text, rendering) =
    1.41 -            try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
    1.42 -            catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
    1.43 -          Simple_Thread.interrupted_exception()
    1.44 +      def apply_result(result: (String, Rendering))
    1.45 +      {
    1.46 +        val (text, rendering) = result
    1.47 +        current_rendering = rendering
    1.48 +        JEdit_Lib.buffer_edit(getBuffer) {
    1.49 +          rich_text_area.active_reset()
    1.50 +          getBuffer.setReadOnly(false)
    1.51 +          getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
    1.52 +          setText(text)
    1.53 +          setCaretPosition(0)
    1.54 +          getBuffer.setReadOnly(true)
    1.55 +        }
    1.56 +      }
    1.57  
    1.58 -          Swing_Thread.later {
    1.59 -            current_rendering = rendering
    1.60 -            JEdit_Lib.buffer_edit(getBuffer) {
    1.61 -              rich_text_area.active_reset()
    1.62 -              getBuffer.setReadOnly(false)
    1.63 -              getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
    1.64 -              setText(text)
    1.65 -              setCaretPosition(0)
    1.66 -              getBuffer.setReadOnly(true)
    1.67 -            }
    1.68 -          }
    1.69 -        }))
    1.70 +      future_rendering.map(_.cancel(true))
    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