1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/System/gui.scala	Thu Apr 04 18:25:47 2013 +0200
     1.3 @@ -0,0 +1,121 @@
     1.4 +/*  Title:      Pure/System/gui.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Elementary GUI tools.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.awt.{Image, Component, Toolkit}
    1.14 +import javax.swing.{ImageIcon, JOptionPane, UIManager}
    1.15 +
    1.16 +import scala.swing.{ComboBox, TextArea, ScrollPane}
    1.17 +import scala.swing.event.SelectionChanged
    1.18 +
    1.19 +
    1.20 +object GUI
    1.21 +{
    1.22 +  /* Swing look-and-feel */
    1.23 +
    1.24 +  def get_laf(): String =
    1.25 +  {
    1.26 +    def laf(name: String): Option[String] =
    1.27 +      UIManager.getInstalledLookAndFeels().find(_.getName == name).map(_.getClassName)
    1.28 +
    1.29 +    if (Platform.is_windows || Platform.is_macos)
    1.30 +      UIManager.getSystemLookAndFeelClassName()
    1.31 +    else
    1.32 +      laf("Nimbus") orElse laf("GTK+") getOrElse
    1.33 +        UIManager.getCrossPlatformLookAndFeelClassName()
    1.34 +  }
    1.35 +
    1.36 +  def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
    1.37 +
    1.38 +
    1.39 +  /* simple dialogs */
    1.40 +
    1.41 +  def scrollable_text(txt: String, width: Int = 60, editable: Boolean = false): ScrollPane =
    1.42 +  {
    1.43 +    val text = new TextArea(txt)
    1.44 +    if (width > 0) text.columns = width
    1.45 +    text.editable = editable
    1.46 +    new ScrollPane(text)
    1.47 +  }
    1.48 +
    1.49 +  private def simple_dialog(kind: Int, default_title: String,
    1.50 +    parent: Component, title: String, message: Seq[Any])
    1.51 +  {
    1.52 +    Swing_Thread.now {
    1.53 +      val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
    1.54 +      JOptionPane.showMessageDialog(parent,
    1.55 +        java_message.toArray.asInstanceOf[Array[AnyRef]],
    1.56 +        if (title == null) default_title else title, kind)
    1.57 +    }
    1.58 +  }
    1.59 +
    1.60 +  def dialog(parent: Component, title: String, message: Any*) =
    1.61 +    simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
    1.62 +
    1.63 +  def warning_dialog(parent: Component, title: String, message: Any*) =
    1.64 +    simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
    1.65 +
    1.66 +  def error_dialog(parent: Component, title: String, message: Any*) =
    1.67 +    simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
    1.68 +
    1.69 +  def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
    1.70 +    Swing_Thread.now {
    1.71 +      val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
    1.72 +      JOptionPane.showConfirmDialog(parent,
    1.73 +        java_message.toArray.asInstanceOf[Array[AnyRef]], title,
    1.74 +          option_type, JOptionPane.QUESTION_MESSAGE)
    1.75 +    }
    1.76 +
    1.77 +
    1.78 +  /* zoom box */
    1.79 +
    1.80 +  class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
    1.81 +    List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
    1.82 +  {
    1.83 +    val Factor = "([0-9]+)%?".r
    1.84 +    def parse(text: String): Int =
    1.85 +      text match {
    1.86 +        case Factor(s) =>
    1.87 +          val i = Integer.parseInt(s)
    1.88 +          if (10 <= i && i <= 1000) i else 100
    1.89 +        case _ => 100
    1.90 +      }
    1.91 +
    1.92 +    def print(i: Int): String = i.toString + "%"
    1.93 +
    1.94 +    def set_item(i: Int) {
    1.95 +      peer.getEditor match {
    1.96 +        case null =>
    1.97 +        case editor => editor.setItem(print(i))
    1.98 +      }
    1.99 +    }
   1.100 +
   1.101 +    makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
   1.102 +    reactions += {
   1.103 +      case SelectionChanged(_) => apply_factor(parse(selection.item))
   1.104 +    }
   1.105 +    listenTo(selection)
   1.106 +    selection.index = 3
   1.107 +    prototypeDisplayValue = Some("00000%")
   1.108 +  }
   1.109 +
   1.110 +
   1.111 +  /* screen resolution */
   1.112 +
   1.113 +  def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
   1.114 +  def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt
   1.115 +
   1.116 +
   1.117 +  /* icon */
   1.118 +
   1.119 +  def isabelle_icon(): ImageIcon =
   1.120 +    new ImageIcon(Isabelle_System.platform_path(Path.explode("~~/lib/logo/isabelle.gif")))
   1.121 +
   1.122 +  def isabelle_image(): Image = isabelle_icon().getImage
   1.123 +}
   1.124 +