equal
deleted
inserted
replaced
1 /* Title: Tools/Graphview/src/floating_dialog.scala |
|
2 Author: Markus Kaiser, TU Muenchen |
|
3 |
|
4 PopUp Dialog containing node meta-information. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import scala.swing.{Dialog, BorderPanel, Component, TextArea} |
|
13 import java.awt.{Font, Point, Dimension} |
|
14 |
|
15 |
|
16 class Floating_Dialog(content: XML.Body, _title: String, _location: Point) |
|
17 extends Dialog |
|
18 { |
|
19 location = _location |
|
20 title = _title |
|
21 //No adaptive size because we don't want to resize the Dialog about 1 sec |
|
22 //after it is shown. |
|
23 preferredSize = new Dimension(300, 300) |
|
24 peer.setAlwaysOnTop(true) |
|
25 |
|
26 private val text_font = new Font(Parameters.font_family, Font.PLAIN, Parameters.font_size) |
|
27 private val text = new TextArea |
|
28 text.peer.setFont(text_font) |
|
29 text.editable = false |
|
30 |
|
31 contents = new BorderPanel { add(text, BorderPanel.Position.Center) } |
|
32 text.text = Pretty.string_of(content, 76, Pretty.font_metric(text.peer.getFontMetrics(text_font))) |
|
33 } |
|