# HG changeset patch
# User wenzelm
# Date 1347961763 -7200
# Node ID 8c9925d31617c7f81bd49a824a42daa6da31d905
# Parent  4cac648e0f8533d5eff6173f80fb761b2b60e157
more static rendering state;

diff -r 4cac648e0f85 -r 8c9925d31617 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Sep 18 11:43:05 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Sep 18 11:49:23 2012 +0200
@@ -56,16 +56,19 @@
   private var current_font_size: Int = 12
   private var current_margin: Int = 0
   private var current_body: XML.Body = Nil
+  private var current_rendering: Isabelle_Rendering = make_rendering()
 
-  def get_rendering(): Isabelle_Rendering =
+  private def make_rendering(): Isabelle_Rendering =
   {
+    Swing_Thread.require()
+
     val body =
       Pretty.formatted(current_body, current_margin, Pretty.font_metric(current_font_metrics))
     Isabelle_Rendering(Pretty_Text_Area.document_state(body).snapshot(), Isabelle.options.value)
   }
 
   val text_area = new JEditEmbeddedTextArea
-  val rich_text_area = new Rich_Text_Area(view, text_area, get_rendering _)
+  val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering)
 
   def refresh()
   {