equal
deleted
inserted
replaced
66 window.getRootPane.setBorder(new LineBorder(Color.BLACK)) |
66 window.getRootPane.setBorder(new LineBorder(Color.BLACK)) |
67 |
67 |
68 |
68 |
69 /* pretty text area */ |
69 /* pretty text area */ |
70 |
70 |
71 val pretty_text_area = new Pretty_Text_Area(view) |
71 val pretty_text_area = new Pretty_Text_Area(view, Some(rendering.tooltip_color)) |
72 pretty_text_area.getPainter.setBackground(rendering.tooltip_color) |
|
73 pretty_text_area.resize(Rendering.font_family(), |
72 pretty_text_area.resize(Rendering.font_family(), |
74 Rendering.font_size("jedit_tooltip_font_scale").round) |
73 Rendering.font_size("jedit_tooltip_font_scale").round) |
75 pretty_text_area.update(rendering.snapshot, results, body) |
74 pretty_text_area.update(rendering.snapshot, results, body) |
76 |
75 |
77 pretty_text_area.registerKeyboardAction(action_listener, "close_all", |
76 pretty_text_area.registerKeyboardAction(action_listener, "close_all", |