equal
deleted
inserted
replaced
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 import java.awt.{GraphicsEnvironment, Point, Font} |
10 import java.awt.{GraphicsEnvironment, Point} |
11 import javax.swing.WindowConstants |
11 import javax.swing.WindowConstants |
12 import java.io.{File => JFile, BufferedReader, InputStreamReader} |
12 import java.io.{File => JFile, BufferedReader, InputStreamReader} |
13 |
13 |
14 import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel, |
14 import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel, |
15 BorderPanel, Frame, TextArea, Component, Label} |
15 BorderPanel, Frame, TextArea, Component, Label} |
80 val text = new TextArea { |
80 val text = new TextArea { |
81 editable = false |
81 editable = false |
82 columns = 65 |
82 columns = 65 |
83 rows = 24 |
83 rows = 24 |
84 } |
84 } |
|
85 if (GUI.is_windows_laf) text.font = (new Label).font |
85 |
86 |
86 val scroll_text = new ScrollPane(text) |
87 val scroll_text = new ScrollPane(text) |
87 |
88 |
88 |
89 |
89 /* layout panel with dynamic actions */ |
90 /* layout panel with dynamic actions */ |