# HG changeset patch # User wenzelm # Date 1365091127 -7200 # Node ID 949e2cf02a3df7c0be902d4cd48bc8cbb78b34f6 # Parent 072a7249e1ac10f23244b54d329f7968ad01bfe4 tuned signature -- concentrate GUI tools; diff -r 072a7249e1ac -r 949e2cf02a3d src/Pure/Tools/build_dialog.scala --- 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 diff -r 072a7249e1ac -r 949e2cf02a3d src/Pure/Tools/main.scala --- 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) } diff -r 072a7249e1ac -r 949e2cf02a3d src/Pure/library.scala --- 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] diff -r 072a7249e1ac -r 949e2cf02a3d src/Tools/Graphview/src/graph_panel.scala --- 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) { diff -r 072a7249e1ac -r 949e2cf02a3d src/Tools/jEdit/src/info_dockable.scala --- 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) diff -r 072a7249e1ac -r 949e2cf02a3d src/Tools/jEdit/src/jedit_options.scala --- 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 { diff -r 072a7249e1ac -r 949e2cf02a3d src/Tools/jEdit/src/output_dockable.scala --- 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") { diff -r 072a7249e1ac -r 949e2cf02a3d src/Tools/jEdit/src/plugin.scala --- 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 _ =>