equal
deleted
inserted
replaced
26 |
26 |
27 private val readme = new HTML_Panel("SansSerif", 14) |
27 private val readme = new HTML_Panel("SansSerif", 14) |
28 readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html")))) |
28 readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html")))) |
29 |
29 |
30 private val syslog = new TextArea(Isabelle.session.syslog()) |
30 private val syslog = new TextArea(Isabelle.session.syslog()) |
31 syslog.editable = false |
|
32 |
31 |
33 private val tabs = new TabbedPane { |
32 private val tabs = new TabbedPane { |
34 pages += new TabbedPane.Page("README", Component.wrap(readme)) |
33 pages += new TabbedPane.Page("README", Component.wrap(readme)) |
35 pages += new TabbedPane.Page("System log", new ScrollPane(syslog)) |
34 pages += new TabbedPane.Page("System log", new ScrollPane(syslog)) |
36 |
35 |