1.1 --- a/src/Pure/System/main.scala	Thu May 03 22:07:29 2012 +0200
     1.2 +++ b/src/Pure/System/main.scala	Fri May 04 15:58:27 2012 +0200
     1.3 @@ -21,11 +21,9 @@
     1.4        }
     1.5        catch { case exn: Throwable => (Exn.message(exn), 2) }
     1.6  
     1.7 -    if (rc != 0) {
     1.8 -      val text = new TextArea(out + "\nReturn code: " + rc)
     1.9 -      text.editable = false
    1.10 -      Library.dialog(null, "Isabelle", "Isabelle output", text)
    1.11 -    }
    1.12 +    if (rc != 0)
    1.13 +      Library.dialog(null, "Isabelle", "Isabelle output",
    1.14 +        Library.scrollable_text(out + "\nReturn code: " + rc))
    1.15  
    1.16      System.exit(rc)
    1.17    }

     2.1 --- a/src/Pure/library.scala	Thu May 03 22:07:29 2012 +0200
     2.2 +++ b/src/Pure/library.scala	Fri May 04 15:58:27 2012 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  import java.awt.Component
     2.5  import javax.swing.JOptionPane
     2.6  
     2.7 -import scala.swing.ComboBox
     2.8 +import scala.swing.{ComboBox, TextArea, ScrollPane}
     2.9  import scala.swing.event.SelectionChanged
    2.10  import scala.collection.mutable
    2.11  
    2.12 @@ -130,6 +130,14 @@
    2.13  
    2.14    /* simple dialogs */
    2.15  
    2.16 +  def scrollable_text(txt: String, width: Int = 76, editable: Boolean = false): ScrollPane =
    2.17 +  {
    2.18 +    val text = new TextArea(txt)
    2.19 +    if (width > 0) text.columns = width
    2.20 +    text.editable = editable
    2.21 +    new ScrollPane(text)
    2.22 +  }
    2.23 +
    2.24    private def simple_dialog(kind: Int, default_title: String,
    2.25      parent: Component, title: String, message: Seq[Any])
    2.26    {

     3.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu May 03 22:07:29 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Fri May 04 15:58:27 2012 +0200
     3.3 @@ -40,7 +40,8 @@
     3.4    override def click(view: View) = {
     3.5      Isabelle_System.source_file(Path.explode(def_file)) match {
     3.6        case None =>
     3.7 -        Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
     3.8 +        Library.error_dialog(view, "File not found",
     3.9 +          Library.scrollable_text("Could not find source file " + def_file))
    3.10        case Some(file) =>
    3.11          jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
    3.12      }

     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu May 03 22:07:29 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri May 04 15:58:27 2012 +0200
     4.3 @@ -388,9 +388,9 @@
     4.4            phase match {
     4.5              case Session.Failed =>
     4.6                Swing_Thread.later {
     4.7 -                val text = new scala.swing.TextArea(Isabelle.session.current_syslog())
     4.8 -                text.editable = false
     4.9 -                Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
    4.10 +                Library.error_dialog(jEdit.getActiveView,
    4.11 +                  "Failed to start Isabelle process",
    4.12 +                    Library.scrollable_text(Isabelle.session.current_syslog()))
    4.13                }
    4.14  
    4.15              case Session.Ready =>