src/Tools/jEdit/src/pretty_text_area.scala
changeset 56662 f373fb77e0a4
parent 56360 1d122af2b11a
child 56711 ef3d00153e3b
equal deleted inserted replaced
56661:ef623f6f036b 56662:f373fb77e0a4
    57   close_action: () => Unit = () => (),
    57   close_action: () => Unit = () => (),
    58   propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
    58   propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
    59 {
    59 {
    60   text_area =>
    60   text_area =>
    61 
    61 
    62   Swing_Thread.require()
    62   Swing_Thread.require {}
    63 
    63 
    64   private var current_font_info: Font_Info = Font_Info.main()
    64   private var current_font_info: Font_Info = Font_Info.main()
    65   private var current_body: XML.Body = Nil
    65   private var current_body: XML.Body = Nil
    66   private var current_base_snapshot = Document.Snapshot.init
    66   private var current_base_snapshot = Document.Snapshot.init
    67   private var current_base_results = Command.Results.empty
    67   private var current_base_results = Command.Results.empty
    75 
    75 
    76   def get_background(): Option[Color] = None
    76   def get_background(): Option[Color] = None
    77 
    77 
    78   def refresh()
    78   def refresh()
    79   {
    79   {
    80     Swing_Thread.require()
    80     Swing_Thread.require {}
    81 
    81 
    82     val font = current_font_info.font
    82     val font = current_font_info.font
    83     getPainter.setFont(font)
    83     getPainter.setFont(font)
    84     getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
    84     getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
    85     getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
    85     getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
   140     }
   140     }
   141   }
   141   }
   142 
   142 
   143   def resize(font_info: Font_Info)
   143   def resize(font_info: Font_Info)
   144   {
   144   {
   145     Swing_Thread.require()
   145     Swing_Thread.require {}
   146 
   146 
   147     current_font_info = font_info
   147     current_font_info = font_info
   148     refresh()
   148     refresh()
   149   }
   149   }
   150 
   150 
   151   def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
   151   def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
   152   {
   152   {
   153     Swing_Thread.require()
   153     Swing_Thread.require {}
   154     require(!base_snapshot.is_outdated)
   154     require(!base_snapshot.is_outdated)
   155 
   155 
   156     current_base_snapshot = base_snapshot
   156     current_base_snapshot = base_snapshot
   157     current_base_results = base_results
   157     current_base_results = base_results
   158     current_body = body
   158     current_body = body