equal
deleted
inserted
replaced
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.dummy |
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 |
68 private var current_rendering: Rendering = |
68 private var current_rendering: Rendering = |
69 Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2 |
69 Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2 |