39 private var current_font_info: Font_Info = Font_Info.main() |
39 private var current_font_info: Font_Info = Font_Info.main() |
40 private var current_output: List[XML.Elem] = Nil |
40 private var current_output: List[XML.Elem] = Nil |
41 private var current_base_snapshot = Document.Snapshot.init |
41 private var current_base_snapshot = Document.Snapshot.init |
42 private var current_base_results = Command.Results.empty |
42 private var current_base_results = Command.Results.empty |
43 private var current_rendering: JEdit_Rendering = |
43 private var current_rendering: JEdit_Rendering = |
44 JEdit_Rendering.text(current_base_snapshot, Nil)._2 |
44 JEdit_Rendering(current_base_snapshot, Command.rich_text()) |
45 private var future_refresh: Option[Future[Unit]] = None |
45 private var future_refresh: Option[Future[Unit]] = None |
46 |
46 |
47 private val rich_text_area = |
47 private val rich_text_area = |
48 new Rich_Text_Area(view, pretty_text_area, () => current_rendering, close_action, |
48 new Rich_Text_Area(view, pretty_text_area, () => current_rendering, close_action, |
49 get_search_pattern _, () => (), caret_visible = false, enable_hovering = true) |
49 get_search_pattern _, () => (), caret_visible = false, enable_hovering = true) |
97 |
97 |
98 future_refresh.foreach(_.cancel()) |
98 future_refresh.foreach(_.cancel()) |
99 future_refresh = |
99 future_refresh = |
100 Some(Future.fork { |
100 Some(Future.fork { |
101 val (text, rendering) = |
101 val (text, rendering) = |
102 try { JEdit_Rendering.text(snapshot, formatted, results = results) } |
102 try { |
|
103 val rich_text = Command.rich_text(body = formatted, results = results) |
|
104 (rich_text.source, JEdit_Rendering(snapshot, rich_text)) |
|
105 } |
103 catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn } |
106 catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn } |
104 Exn.Interrupt.expose() |
107 Exn.Interrupt.expose() |
105 |
108 |
106 GUI_Thread.later { |
109 GUI_Thread.later { |
107 current_rendering = rendering |
110 current_rendering = rendering |