# HG changeset patch
# User wenzelm
# Date 1355518221 -3600
# Node ID 3b68e5760a2d840a422192bbfd767a21ab79821c
# Parent  48cb76b785da085b2e3dac74672d8b3584a175be
tuned error dialog;

diff -r 48cb76b785da -r 3b68e5760a2d src/Pure/System/build_dialog.scala
--- a/src/Pure/System/build_dialog.scala	Fri Dec 14 21:26:01 2012 +0100
+++ b/src/Pure/System/build_dialog.scala	Fri Dec 14 21:50:21 2012 +0100
@@ -18,6 +18,7 @@
 {
   def main(args: Array[String]) =
   {
+    Platform.init_laf()
     try {
       args.toList match {
         case
@@ -36,8 +37,6 @@
                 more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0)
             else
               Swing_Thread.later {
-                Platform.init_laf()
-
                 val top = build_dialog(options, system_mode, more_dirs, session)
                 top.pack()
 
diff -r 48cb76b785da -r 3b68e5760a2d src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Dec 14 21:26:01 2012 +0100
+++ b/src/Pure/library.scala	Fri Dec 14 21:50:21 2012 +0100
@@ -128,7 +128,7 @@
 
   /* simple dialogs */
 
-  def scrollable_text(txt: String, width: Int = 80, editable: Boolean = false): ScrollPane =
+  def scrollable_text(txt: String, width: Int = 60, editable: Boolean = false): ScrollPane =
   {
     val text = new TextArea(txt)
     if (width > 0) text.columns = width