--- a/src/Pure/Tools/build_dialog.scala Thu Apr 04 17:47:28 2013 +0200
+++ b/src/Pure/Tools/build_dialog.scala Thu Apr 04 17:58:47 2013 +0200
@@ -51,8 +51,7 @@
}
catch {
case exn: Throwable =>
- Library.error_dialog(null, "Isabelle build failure",
- Library.scrollable_text(Exn.message(exn)))
+ GUI.error_dialog(null, "Isabelle build failure", GUI.scrollable_text(Exn.message(exn)))
sys.exit(2)
}
}
@@ -78,7 +77,7 @@
/* text */
val text = new TextArea {
- font = new Font("SansSerif", Font.PLAIN, Library.resolution_scale(10) max 14)
+ font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
editable = false
columns = 50
rows = 20
--- a/src/Pure/Tools/main.scala Thu Apr 04 17:47:28 2013 +0200
+++ b/src/Pure/Tools/main.scala Thu Apr 04 17:58:47 2013 +0200
@@ -22,8 +22,8 @@
catch { case exn: Throwable => (Exn.message(exn), 2) }
if (rc != 0)
- Library.dialog(null, "Isabelle", "Isabelle output",
- Library.scrollable_text(out + "\nReturn code: " + rc))
+ GUI.dialog(null, "Isabelle", "Isabelle output",
+ GUI.scrollable_text(out + "\nReturn code: " + rc))
sys.exit(rc)
}
--- a/src/Pure/library.scala Thu Apr 04 17:47:28 2013 +0200
+++ b/src/Pure/library.scala Thu Apr 04 17:58:47 2013 +0200
@@ -8,15 +8,8 @@
package isabelle
-import java.lang.System
import java.util.Locale
import java.util.concurrent.{Future => JFuture, TimeUnit}
-import java.awt.{Component, Toolkit}
-import javax.swing.JOptionPane
-
-import scala.swing.{ComboBox, TextArea, ScrollPane}
-import scala.swing.event.SelectionChanged
-import scala.collection.mutable
object Library
@@ -128,84 +121,6 @@
}
- /* simple dialogs */
-
- def scrollable_text(txt: String, width: Int = 60, 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])
- {
- Swing_Thread.now {
- val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
- JOptionPane.showMessageDialog(parent,
- java_message.toArray.asInstanceOf[Array[AnyRef]],
- if (title == null) default_title else title, kind)
- }
- }
-
- def dialog(parent: Component, title: String, message: Any*) =
- simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
-
- def warning_dialog(parent: Component, title: String, message: Any*) =
- simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
-
- def error_dialog(parent: Component, title: String, message: Any*) =
- simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
-
- def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
- Swing_Thread.now {
- val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
- JOptionPane.showConfirmDialog(parent,
- java_message.toArray.asInstanceOf[Array[AnyRef]], title,
- option_type, JOptionPane.QUESTION_MESSAGE)
- }
-
-
- /* zoom box */
-
- class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
- List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
- {
- val Factor = "([0-9]+)%?".r
- def parse(text: String): Int =
- text match {
- case Factor(s) =>
- val i = Integer.parseInt(s)
- if (10 <= i && i <= 1000) i else 100
- case _ => 100
- }
-
- def print(i: Int): String = i.toString + "%"
-
- def set_item(i: Int) {
- peer.getEditor match {
- case null =>
- case editor => editor.setItem(print(i))
- }
- }
-
- makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
- reactions += {
- case SelectionChanged(_) => apply_factor(parse(selection.item))
- }
- listenTo(selection)
- selection.index = 3
- prototypeDisplayValue = Some("00000%")
- }
-
-
- /* screen resolution */
-
- def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
- def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt
-
-
/* Java futures */
def future_value[A](x: A) = new JFuture[A]
--- a/src/Tools/Graphview/src/graph_panel.scala Thu Apr 04 17:47:28 2013 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala Thu Apr 04 17:58:47 2013 +0200
@@ -62,8 +62,7 @@
refresh()
}
- val zoom_box: Library.Zoom_Box =
- new Library.Zoom_Box(percent => rescale(0.01 * percent))
+ val zoom_box: GUI.Zoom_Box = new GUI.Zoom_Box(percent => rescale(0.01 * percent))
def rescale(s: Double)
{
--- a/src/Tools/jEdit/src/info_dockable.scala Thu Apr 04 17:47:28 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Thu Apr 04 17:58:47 2013 +0200
@@ -94,7 +94,7 @@
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
})
- private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
+ private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
zoom.tooltip = "Zoom factor for basic font size"
private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
--- a/src/Tools/jEdit/src/jedit_options.scala Thu Apr 04 17:47:28 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Thu Apr 04 17:58:47 2013 +0200
@@ -75,8 +75,8 @@
try { update(value + (opt_name, text)) }
catch {
case ERROR(msg) =>
- Library.error_dialog(this.peer, "Failed to update options",
- Library.scrollable_text(msg))
+ GUI.error_dialog(this.peer, "Failed to update options",
+ GUI.scrollable_text(msg))
}
}
text_area.peer.setInputVerifier(new InputVerifier {
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Apr 04 17:47:28 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Apr 04 17:58:47 2013 +0200
@@ -135,7 +135,7 @@
/* controls */
- private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
+ private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
zoom.tooltip = "Zoom factor for basic font size"
private val auto_update = new CheckBox("Auto update") {
--- a/src/Tools/jEdit/src/plugin.scala Thu Apr 04 17:47:28 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Thu Apr 04 17:58:47 2013 +0200
@@ -166,7 +166,7 @@
files_list.selection.indices += i
val answer =
- Library.confirm_dialog(view,
+ GUI.confirm_dialog(view,
"Auto loading of required files",
JOptionPane.YES_NO_OPTION,
"The following files are required to resolve theory imports.",
@@ -191,8 +191,8 @@
phase match {
case Session.Inactive | Session.Failed =>
Swing_Thread.later {
- Library.error_dialog(jEdit.getActiveView, "Prover process terminated",
- "Isabelle Syslog", Library.scrollable_text(PIDE.session.current_syslog()))
+ GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
+ "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
}
case Session.Ready =>
@@ -230,8 +230,8 @@
if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
message match {
case msg: EditorStarted =>
- Library.error_dialog(null, "Isabelle plugin startup failure",
- Library.scrollable_text(Exn.message(PIDE.startup_failure.get)),
+ GUI.error_dialog(null, "Isabelle plugin startup failure",
+ GUI.scrollable_text(Exn.message(PIDE.startup_failure.get)),
"Prover IDE inactive!")
PIDE.startup_notified = true
case _ =>