# HG changeset patch
# User wenzelm
# Date 1336139907 -7200
# Node ID dd9cbe708e6b306c05c8ce8dd9b19b11eedb4264
# Parent  2cc26ddd82983a57518484948e16c0d15f7a070e
some attempts to make critical errors fit on screen;

diff -r 2cc26ddd8298 -r dd9cbe708e6b src/Pure/System/main.scala
--- a/src/Pure/System/main.scala	Thu May 03 22:07:29 2012 +0200
+++ b/src/Pure/System/main.scala	Fri May 04 15:58:27 2012 +0200
@@ -21,11 +21,9 @@
       }
       catch { case exn: Throwable => (Exn.message(exn), 2) }
 
-    if (rc != 0) {
-      val text = new TextArea(out + "\nReturn code: " + rc)
-      text.editable = false
-      Library.dialog(null, "Isabelle", "Isabelle output", text)
-    }
+    if (rc != 0)
+      Library.dialog(null, "Isabelle", "Isabelle output",
+        Library.scrollable_text(out + "\nReturn code: " + rc))
 
     System.exit(rc)
   }
diff -r 2cc26ddd8298 -r dd9cbe708e6b src/Pure/library.scala
--- a/src/Pure/library.scala	Thu May 03 22:07:29 2012 +0200
+++ b/src/Pure/library.scala	Fri May 04 15:58:27 2012 +0200
@@ -12,7 +12,7 @@
 import java.awt.Component
 import javax.swing.JOptionPane
 
-import scala.swing.ComboBox
+import scala.swing.{ComboBox, TextArea, ScrollPane}
 import scala.swing.event.SelectionChanged
 import scala.collection.mutable
 
@@ -130,6 +130,14 @@
 
   /* simple dialogs */
 
+  def scrollable_text(txt: String, width: Int = 76, editable: Boolean = false): ScrollPane =
+  {
+    val text = new TextArea(txt)
+    if (width > 0) text.columns = width
+    text.editable = editable
+    new ScrollPane(text)
+  }
+
   private def simple_dialog(kind: Int, default_title: String,
     parent: Component, title: String, message: Seq[Any])
   {
diff -r 2cc26ddd8298 -r dd9cbe708e6b src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu May 03 22:07:29 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Fri May 04 15:58:27 2012 +0200
@@ -40,7 +40,8 @@
   override def click(view: View) = {
     Isabelle_System.source_file(Path.explode(def_file)) match {
       case None =>
-        Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
+        Library.error_dialog(view, "File not found",
+          Library.scrollable_text("Could not find source file " + def_file))
       case Some(file) =>
         jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
     }
diff -r 2cc26ddd8298 -r dd9cbe708e6b src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu May 03 22:07:29 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri May 04 15:58:27 2012 +0200
@@ -388,9 +388,9 @@
           phase match {
             case Session.Failed =>
               Swing_Thread.later {
-                val text = new scala.swing.TextArea(Isabelle.session.current_syslog())
-                text.editable = false
-                Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
+                Library.error_dialog(jEdit.getActiveView,
+                  "Failed to start Isabelle process",
+                    Library.scrollable_text(Isabelle.session.current_syslog()))
               }
 
             case Session.Ready =>