src/Tools/jEdit/src/pretty_text_area.scala
changeset 50166 2585c81d840a
parent 50160 a29be9d067d2
child 50168 4a575ef46466
equal deleted inserted replaced
50165:24d47733975f 50166:2585c81d840a
    70 
    70 
    71   def refresh()
    71   def refresh()
    72   {
    72   {
    73     Swing_Thread.require()
    73     Swing_Thread.require()
    74 
    74 
    75     val font = new Font(current_font_family, Font.PLAIN, current_font_size)
    75     if (getWidth > 0) {
    76     getPainter.setFont(font)
    76       val font = new Font(current_font_family, Font.PLAIN, current_font_size)
    77     getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
    77       getPainter.setFont(font)
    78     getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
    78       getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
       
    79       getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
    79 
    80 
    80     val font_metrics = getPainter.getFontMetrics(font)
    81       val font_metrics = getPainter.getFontMetrics(font)
    81     val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
    82       val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
    82 
    83 
    83     val base_snapshot = current_base_snapshot
    84       val base_snapshot = current_base_snapshot
    84     val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
    85       val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
    85 
    86 
    86     future_rendering.map(_.cancel(true))
    87       future_rendering.map(_.cancel(true))
    87     future_rendering = Some(default_thread_pool.submit(() =>
    88       future_rendering = Some(default_thread_pool.submit(() =>
    88       {
    89         {
    89         val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
    90           val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
    90         Simple_Thread.interrupted_exception()
    91           Simple_Thread.interrupted_exception()
    91 
    92 
    92         Swing_Thread.later {
    93           Swing_Thread.later {
    93           current_rendering = rendering
    94             current_rendering = rendering
    94 
    95 
    95           try {
    96             try {
    96             getBuffer.beginCompoundEdit
    97               getBuffer.beginCompoundEdit
    97             getBuffer.setReadOnly(false)
    98               getBuffer.setReadOnly(false)
    98             setText(text)
    99               setText(text)
    99             setCaretPosition(0)
   100               setCaretPosition(0)
   100             getBuffer.setReadOnly(true)
   101               getBuffer.setReadOnly(true)
       
   102             }
       
   103             finally {
       
   104               getBuffer.endCompoundEdit
       
   105             }
   101           }
   106           }
   102           finally {
   107         }))
   103             getBuffer.endCompoundEdit
   108     }
   104           }
       
   105         }
       
   106       }))
       
   107   }
   109   }
   108 
   110 
   109   def resize(font_family: String, font_size: Int)
   111   def resize(font_family: String, font_size: Int)
   110   {
   112   {
   111     Swing_Thread.require()
   113     Swing_Thread.require()