--- 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)
}
--- 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])
{
--- 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))
}
--- 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 =>