1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/GUI/color_value.scala Sun Sep 22 14:30:34 2013 +0200
1.3 @@ -0,0 +1,47 @@
1.4 +/* Title: Pure/GUI/color_value.scala
1.5 + Author: Makarius
1.6 +
1.7 +Cached color values.
1.8 +*/
1.9 +
1.10 +package isabelle
1.11 +
1.12 +
1.13 +import java.awt.Color
1.14 +
1.15 +
1.16 +object Color_Value
1.17 +{
1.18 + private var cache = Map.empty[String, Color]
1.19 +
1.20 + def parse(s: String): Color =
1.21 + {
1.22 + val i = java.lang.Long.parseLong(s, 16)
1.23 + val r = ((i >> 24) & 0xFF).toInt
1.24 + val g = ((i >> 16) & 0xFF).toInt
1.25 + val b = ((i >> 8) & 0xFF).toInt
1.26 + val a = (i & 0xFF).toInt
1.27 + new Color(r, g, b, a)
1.28 + }
1.29 +
1.30 + def print(c: Color): String =
1.31 + {
1.32 + val r = new java.lang.Integer(c.getRed)
1.33 + val g = new java.lang.Integer(c.getGreen)
1.34 + val b = new java.lang.Integer(c.getBlue)
1.35 + val a = new java.lang.Integer(c.getAlpha)
1.36 + String.format("%02x%02x%02x%02x", r, g, b, a).toUpperCase
1.37 + }
1.38 +
1.39 + def apply(s: String): Color =
1.40 + synchronized {
1.41 + cache.get(s) match {
1.42 + case Some(c) => c
1.43 + case None =>
1.44 + val c = parse(s)
1.45 + cache += (s -> c)
1.46 + c
1.47 + }
1.48 + }
1.49 +}
1.50 +
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Pure/GUI/gui.scala Sun Sep 22 14:30:34 2013 +0200
2.3 @@ -0,0 +1,154 @@
2.4 +/* Title: Pure/GUI/gui.scala
2.5 + Author: Makarius
2.6 +
2.7 +Basic GUI tools (for AWT/Swing).
2.8 +*/
2.9 +
2.10 +package isabelle
2.11 +
2.12 +
2.13 +import java.awt.{Image, Component, Container, Toolkit, Window}
2.14 +import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow}
2.15 +
2.16 +import scala.swing.{ComboBox, TextArea, ScrollPane}
2.17 +import scala.swing.event.SelectionChanged
2.18 +
2.19 +
2.20 +object GUI
2.21 +{
2.22 + /* Swing look-and-feel */
2.23 +
2.24 + def get_laf(): String =
2.25 + {
2.26 + def laf(name: String): Option[String] =
2.27 + UIManager.getInstalledLookAndFeels().find(_.getName == name).map(_.getClassName)
2.28 +
2.29 + if (Platform.is_windows || Platform.is_macos)
2.30 + UIManager.getSystemLookAndFeelClassName()
2.31 + else
2.32 + laf("Nimbus") orElse laf("GTK+") getOrElse
2.33 + UIManager.getCrossPlatformLookAndFeelClassName()
2.34 + }
2.35 +
2.36 + def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
2.37 +
2.38 +
2.39 + /* simple dialogs */
2.40 +
2.41 + def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
2.42 + : ScrollPane =
2.43 + {
2.44 + val text = new TextArea(txt)
2.45 + if (width > 0) text.columns = width
2.46 + if (height > 0 && split_lines(txt).length > height) text.rows = height
2.47 + text.editable = editable
2.48 + new ScrollPane(text)
2.49 + }
2.50 +
2.51 + private def simple_dialog(kind: Int, default_title: String,
2.52 + parent: Component, title: String, message: Seq[Any])
2.53 + {
2.54 + Swing_Thread.now {
2.55 + val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
2.56 + JOptionPane.showMessageDialog(parent,
2.57 + java_message.toArray.asInstanceOf[Array[AnyRef]],
2.58 + if (title == null) default_title else title, kind)
2.59 + }
2.60 + }
2.61 +
2.62 + def dialog(parent: Component, title: String, message: Any*) =
2.63 + simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
2.64 +
2.65 + def warning_dialog(parent: Component, title: String, message: Any*) =
2.66 + simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
2.67 +
2.68 + def error_dialog(parent: Component, title: String, message: Any*) =
2.69 + simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
2.70 +
2.71 + def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
2.72 + Swing_Thread.now {
2.73 + val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
2.74 + JOptionPane.showConfirmDialog(parent,
2.75 + java_message.toArray.asInstanceOf[Array[AnyRef]], title,
2.76 + option_type, JOptionPane.QUESTION_MESSAGE)
2.77 + }
2.78 +
2.79 +
2.80 + /* zoom box */
2.81 +
2.82 + class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
2.83 + List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
2.84 + {
2.85 + val Factor = "([0-9]+)%?".r
2.86 + def parse(text: String): Int =
2.87 + text match {
2.88 + case Factor(s) =>
2.89 + val i = Integer.parseInt(s)
2.90 + if (10 <= i && i <= 1000) i else 100
2.91 + case _ => 100
2.92 + }
2.93 +
2.94 + def print(i: Int): String = i.toString + "%"
2.95 +
2.96 + def set_item(i: Int) {
2.97 + peer.getEditor match {
2.98 + case null =>
2.99 + case editor => editor.setItem(print(i))
2.100 + }
2.101 + }
2.102 +
2.103 + makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
2.104 + reactions += {
2.105 + case SelectionChanged(_) => apply_factor(parse(selection.item))
2.106 + }
2.107 + listenTo(selection)
2.108 + selection.index = 3
2.109 + prototypeDisplayValue = Some("00000%")
2.110 + }
2.111 +
2.112 +
2.113 + /* screen resolution */
2.114 +
2.115 + def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
2.116 + def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt
2.117 +
2.118 +
2.119 + /* icon */
2.120 +
2.121 + def isabelle_icon(): ImageIcon =
2.122 + new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif"))
2.123 +
2.124 + def isabelle_image(): Image = isabelle_icon().getImage
2.125 +
2.126 +
2.127 + /* component hierachy */
2.128 +
2.129 + def get_parent(component: Component): Option[Container] =
2.130 + component.getParent match {
2.131 + case null => None
2.132 + case parent => Some(parent)
2.133 + }
2.134 +
2.135 + def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
2.136 + private var next_elem = get_parent(component)
2.137 + def hasNext(): Boolean = next_elem.isDefined
2.138 + def next(): Container =
2.139 + next_elem match {
2.140 + case Some(parent) =>
2.141 + next_elem = get_parent(parent)
2.142 + parent
2.143 + case None => Iterator.empty.next()
2.144 + }
2.145 + }
2.146 +
2.147 + def parent_window(component: Component): Option[Window] =
2.148 + ancestors(component).collectFirst({ case x: Window => x })
2.149 +
2.150 + def layered_pane(component: Component): Option[JLayeredPane] =
2.151 + parent_window(component) match {
2.152 + case Some(window: JWindow) => Some(window.getLayeredPane)
2.153 + case Some(frame: JFrame) => Some(frame.getLayeredPane)
2.154 + case _ => None
2.155 + }
2.156 +}
2.157 +
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Pure/GUI/gui_setup.scala Sun Sep 22 14:30:34 2013 +0200
3.3 @@ -0,0 +1,71 @@
3.4 +/* Title: Pure/GUI/gui_setup.scala
3.5 + Author: Makarius
3.6 +
3.7 +GUI for basic system setup.
3.8 +*/
3.9 +
3.10 +package isabelle
3.11 +
3.12 +import java.lang.System
3.13 +
3.14 +import scala.swing.{ScrollPane, Button, FlowPanel,
3.15 + BorderPanel, MainFrame, TextArea, SwingApplication}
3.16 +import scala.swing.event.ButtonClicked
3.17 +
3.18 +
3.19 +object GUI_Setup extends SwingApplication
3.20 +{
3.21 + def startup(args: Array[String]) =
3.22 + {
3.23 + GUI.init_laf()
3.24 + top.pack()
3.25 + top.visible = true
3.26 + }
3.27 +
3.28 + def top = new MainFrame {
3.29 + iconImage = GUI.isabelle_image()
3.30 +
3.31 + title = "Isabelle setup"
3.32 +
3.33 + // components
3.34 + val text = new TextArea {
3.35 + editable = false
3.36 + columns = 80
3.37 + rows = 20
3.38 + }
3.39 + val ok = new Button { text = "OK" }
3.40 + val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
3.41 +
3.42 + val panel = new BorderPanel
3.43 + panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
3.44 + panel.layout(ok_panel) = BorderPanel.Position.South
3.45 + contents = panel
3.46 +
3.47 + // values
3.48 + text.append("JVM name: " + Platform.jvm_name + "\n")
3.49 + text.append("JVM platform: " + Platform.jvm_platform + "\n")
3.50 + text.append("JVM home: " + java.lang.System.getProperty("java.home", "") + "\n")
3.51 + try {
3.52 + Isabelle_System.init()
3.53 + if (Platform.is_windows)
3.54 + text.append("Cygwin root: " + Isabelle_System.get_cygwin_root() + "\n")
3.55 + text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n")
3.56 + text.append("Isabelle platform: " + Isabelle_System.getenv("ISABELLE_PLATFORM") + "\n")
3.57 + val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
3.58 + if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
3.59 + text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n")
3.60 + val isabelle_home_windows = Isabelle_System.getenv("ISABELLE_HOME_WINDOWS")
3.61 + if (isabelle_home_windows != "")
3.62 + text.append("Isabelle home (Windows): " + isabelle_home_windows + "\n")
3.63 + text.append("Isabelle JDK home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n")
3.64 + }
3.65 + catch { case ERROR(msg) => text.append(msg + "\n") }
3.66 +
3.67 + // reactions
3.68 + listenTo(ok)
3.69 + reactions += {
3.70 + case ButtonClicked(`ok`) => sys.exit(0)
3.71 + }
3.72 + }
3.73 +}
3.74 +
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/GUI/html5_panel.scala Sun Sep 22 14:30:34 2013 +0200
4.3 @@ -0,0 +1,78 @@
4.4 +/* Title: Pure/GUI/html5_panel.scala
4.5 + Author: Makarius
4.6 +
4.7 +HTML5 panel based on Java FX WebView.
4.8 +*/
4.9 +
4.10 +package isabelle
4.11 +
4.12 +
4.13 +import javafx.scene.Scene
4.14 +import javafx.scene.web.{WebView, WebEngine}
4.15 +import javafx.scene.input.KeyEvent
4.16 +import javafx.scene.text.FontSmoothingType
4.17 +import javafx.scene.layout.{HBox, VBox, Priority}
4.18 +import javafx.geometry.{HPos, VPos, Insets}
4.19 +import javafx.event.EventHandler
4.20 +
4.21 +
4.22 +// see http://netbeans.org/bugzilla/show_bug.cgi?id=210414
4.23 +// and http://hg.netbeans.org/jet-main/rev/a88434cec458
4.24 +private class Web_View_Workaround extends javafx.scene.layout.Pane
4.25 +{
4.26 + VBox.setVgrow(this, Priority.ALWAYS)
4.27 + HBox.setHgrow(this, Priority.ALWAYS)
4.28 +
4.29 + setMaxWidth(java.lang.Double.MAX_VALUE)
4.30 + setMaxHeight(java.lang.Double.MAX_VALUE)
4.31 +
4.32 + val web_view = new WebView
4.33 + web_view.setMinSize(500, 400)
4.34 + web_view.setPrefSize(500, 400)
4.35 +
4.36 + getChildren().add(web_view)
4.37 +
4.38 + override protected def layoutChildren()
4.39 + {
4.40 + val managed = getManagedChildren()
4.41 + val width = getWidth()
4.42 + val height = getHeight()
4.43 + val top = getInsets().getTop()
4.44 + val right = getInsets().getRight()
4.45 + val left = getInsets().getLeft()
4.46 + val bottom = getInsets().getBottom()
4.47 +
4.48 + for (i <- 0 until managed.size)
4.49 + layoutInArea(managed.get(i), left, top,
4.50 + width - left - right, height - top - bottom,
4.51 + 0, Insets.EMPTY, true, true, HPos.CENTER, VPos.CENTER)
4.52 + }
4.53 +}
4.54 +
4.55 +
4.56 +class HTML5_Panel extends javafx.embed.swing.JFXPanel
4.57 +{
4.58 + private val future =
4.59 + JFX_Thread.future {
4.60 + val pane = new Web_View_Workaround
4.61 +
4.62 + val web_view = pane.web_view
4.63 + web_view.setFontSmoothingType(FontSmoothingType.GRAY)
4.64 + web_view.setOnKeyTyped(new EventHandler[KeyEvent] {
4.65 + def handle(e: KeyEvent) {
4.66 + if (e.isControlDown && e.getCharacter == "0")
4.67 + web_view.setFontScale(1.0)
4.68 + if (e.isControlDown && e.getCharacter == "+")
4.69 + web_view.setFontScale(web_view.getFontScale * 1.1)
4.70 + else if (e.isControlDown && e.getCharacter == "-")
4.71 + web_view.setFontScale(web_view.getFontScale / 1.1)
4.72 + }
4.73 + })
4.74 +
4.75 + setScene(new Scene(pane))
4.76 + pane
4.77 + }
4.78 +
4.79 + def web_view: WebView = future.join.web_view
4.80 + def web_engine: WebEngine = web_view.getEngine
4.81 +}
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Pure/GUI/jfx_thread.scala Sun Sep 22 14:30:34 2013 +0200
5.3 @@ -0,0 +1,37 @@
5.4 +/* Title: Pure/GUI/jfx_thread.scala
5.5 + Author: Makarius
5.6 +
5.7 +Evaluation within the Java FX application thread.
5.8 +*/
5.9 +
5.10 +package isabelle
5.11 +
5.12 +import javafx.application.{Platform => JFX_Platform}
5.13 +
5.14 +
5.15 +object JFX_Thread
5.16 +{
5.17 + /* checks */
5.18 +
5.19 + def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
5.20 + def require() = Predef.require(JFX_Platform.isFxApplicationThread())
5.21 +
5.22 +
5.23 + /* asynchronous context switch */
5.24 +
5.25 + def later(body: => Unit)
5.26 + {
5.27 + if (JFX_Platform.isFxApplicationThread()) body
5.28 + else JFX_Platform.runLater(new Runnable { def run = body })
5.29 + }
5.30 +
5.31 + def future[A](body: => A): Future[A] =
5.32 + {
5.33 + if (JFX_Platform.isFxApplicationThread()) Future.value(body)
5.34 + else {
5.35 + val promise = Future.promise[A]
5.36 + later { promise.fulfill_result(Exn.capture(body)) }
5.37 + promise
5.38 + }
5.39 + }
5.40 +}
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Pure/GUI/popup.scala Sun Sep 22 14:30:34 2013 +0200
6.3 @@ -0,0 +1,38 @@
6.4 +/* Title: Pure/GUI/popup.scala
6.5 + Author: Makarius
6.6 +
6.7 +Popup within layered pane.
6.8 +*/
6.9 +
6.10 +package isabelle
6.11 +
6.12 +
6.13 +import java.awt.{Point, Dimension}
6.14 +import javax.swing.{JLayeredPane, JComponent}
6.15 +
6.16 +
6.17 +class Popup(
6.18 + layered: JLayeredPane,
6.19 + component: JComponent,
6.20 + location: Point,
6.21 + size: Dimension)
6.22 +{
6.23 + def show
6.24 + {
6.25 + component.setLocation(location)
6.26 + component.setSize(size)
6.27 + component.setPreferredSize(size)
6.28 + component.setOpaque(true)
6.29 + layered.add(component, JLayeredPane.POPUP_LAYER)
6.30 + layered.moveToFront(component)
6.31 + layered.repaint(component.getBounds())
6.32 + }
6.33 +
6.34 + def hide
6.35 + {
6.36 + val bounds = component.getBounds()
6.37 + layered.remove(component)
6.38 + layered.repaint(bounds)
6.39 + }
6.40 +}
6.41 +
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Pure/GUI/swing_thread.scala Sun Sep 22 14:30:34 2013 +0200
7.3 @@ -0,0 +1,104 @@
7.4 +/* Title: Pure/GUI/swing_thread.scala
7.5 + Author: Makarius
7.6 +
7.7 +Evaluation within the AWT/Swing thread.
7.8 +*/
7.9 +
7.10 +package isabelle
7.11 +
7.12 +import javax.swing.{SwingUtilities, Timer}
7.13 +import java.awt.event.{ActionListener, ActionEvent}
7.14 +
7.15 +
7.16 +object Swing_Thread
7.17 +{
7.18 + /* checks */
7.19 +
7.20 + def assert[A](body: => A) =
7.21 + {
7.22 + Predef.assert(SwingUtilities.isEventDispatchThread())
7.23 + body
7.24 + }
7.25 +
7.26 + def require[A](body: => A) =
7.27 + {
7.28 + Predef.require(SwingUtilities.isEventDispatchThread())
7.29 + body
7.30 + }
7.31 +
7.32 +
7.33 + /* main dispatch queue */
7.34 +
7.35 + def now[A](body: => A): A =
7.36 + {
7.37 + if (SwingUtilities.isEventDispatchThread()) body
7.38 + else {
7.39 + lazy val result = { assert(); Exn.capture(body) }
7.40 + SwingUtilities.invokeAndWait(new Runnable { def run = result })
7.41 + Exn.release(result)
7.42 + }
7.43 + }
7.44 +
7.45 + def future[A](body: => A): Future[A] =
7.46 + {
7.47 + if (SwingUtilities.isEventDispatchThread()) Future.value(body)
7.48 + else Future.fork { now(body) }
7.49 + }
7.50 +
7.51 + def later(body: => Unit)
7.52 + {
7.53 + if (SwingUtilities.isEventDispatchThread()) body
7.54 + else SwingUtilities.invokeLater(new Runnable { def run = body })
7.55 + }
7.56 +
7.57 +
7.58 + /* delayed actions */
7.59 +
7.60 + abstract class Delay extends
7.61 + {
7.62 + def invoke(): Unit
7.63 + def revoke(): Unit
7.64 + def postpone(time: Time): Unit
7.65 + }
7.66 +
7.67 + private def delayed_action(first: Boolean)(time: => Time)(action: => Unit): Delay =
7.68 + new Delay {
7.69 + private val timer = new Timer(time.ms.toInt, null)
7.70 + timer.setRepeats(false)
7.71 + timer.addActionListener(new ActionListener {
7.72 + override def actionPerformed(e: ActionEvent) {
7.73 + assert()
7.74 + timer.setInitialDelay(time.ms.toInt)
7.75 + action
7.76 + }
7.77 + })
7.78 +
7.79 + def invoke()
7.80 + {
7.81 + require()
7.82 + if (first) timer.start() else timer.restart()
7.83 + }
7.84 +
7.85 + def revoke()
7.86 + {
7.87 + require()
7.88 + timer.stop()
7.89 + timer.setInitialDelay(time.ms.toInt)
7.90 + }
7.91 +
7.92 + def postpone(alt_time: Time)
7.93 + {
7.94 + require()
7.95 + if (timer.isRunning) {
7.96 + timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
7.97 + timer.restart()
7.98 + }
7.99 + }
7.100 + }
7.101 +
7.102 + // delayed action after first invocation
7.103 + def delay_first = delayed_action(true) _
7.104 +
7.105 + // delayed action after last invocation
7.106 + def delay_last = delayed_action(false) _
7.107 +}
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Pure/GUI/system_dialog.scala Sun Sep 22 14:30:34 2013 +0200
8.3 @@ -0,0 +1,212 @@
8.4 +/* Title: Pure/GUI/system_dialog.scala
8.5 + Author: Makarius
8.6 +
8.7 +Dialog for system processes, with optional output window.
8.8 +*/
8.9 +
8.10 +package isabelle
8.11 +
8.12 +
8.13 +import java.awt.{GraphicsEnvironment, Point, Font}
8.14 +import javax.swing.WindowConstants
8.15 +import java.io.{File => JFile, BufferedReader, InputStreamReader}
8.16 +
8.17 +import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
8.18 + BorderPanel, Frame, TextArea, Component, Label}
8.19 +import scala.swing.event.ButtonClicked
8.20 +
8.21 +
8.22 +class System_Dialog extends Build.Progress
8.23 +{
8.24 + /* GUI state -- owned by Swing thread */
8.25 +
8.26 + private var _title = "Isabelle"
8.27 + private var _window: Option[Window] = None
8.28 + private var _return_code: Option[Int] = None
8.29 +
8.30 + private def check_window(): Window =
8.31 + {
8.32 + Swing_Thread.require()
8.33 +
8.34 + _window match {
8.35 + case Some(window) => window
8.36 + case None =>
8.37 + val window = new Window
8.38 + _window = Some(window)
8.39 +
8.40 + window.pack()
8.41 + val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
8.42 + window.location =
8.43 + new Point(point.x - window.size.width / 2, point.y - window.size.height / 2)
8.44 + window.visible = true
8.45 +
8.46 + window
8.47 + }
8.48 + }
8.49 +
8.50 + private val result = Future.promise[Int]
8.51 +
8.52 + private def conclude()
8.53 + {
8.54 + Swing_Thread.require()
8.55 + require(_return_code.isDefined)
8.56 +
8.57 + _window match {
8.58 + case None =>
8.59 + case Some(window) =>
8.60 + window.visible = false
8.61 + window.dispose
8.62 + _window = None
8.63 + }
8.64 +
8.65 + try { result.fulfill(_return_code.get) }
8.66 + catch { case ERROR(_) => }
8.67 + }
8.68 +
8.69 + def join(): Int = result.join
8.70 + def join_exit(): Nothing = sys.exit(join)
8.71 +
8.72 +
8.73 + /* window */
8.74 +
8.75 + private class Window extends Frame
8.76 + {
8.77 + title = _title
8.78 + iconImage = GUI.isabelle_image()
8.79 +
8.80 +
8.81 + /* text */
8.82 +
8.83 + val text = new TextArea {
8.84 + font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
8.85 + editable = false
8.86 + columns = 50
8.87 + rows = 20
8.88 + }
8.89 +
8.90 + val scroll_text = new ScrollPane(text)
8.91 +
8.92 +
8.93 + /* layout panel with dynamic actions */
8.94 +
8.95 + val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
8.96 + val layout_panel = new BorderPanel
8.97 + layout_panel.layout(scroll_text) = BorderPanel.Position.Center
8.98 + layout_panel.layout(action_panel) = BorderPanel.Position.South
8.99 +
8.100 + contents = layout_panel
8.101 +
8.102 + def set_actions(cs: Component*)
8.103 + {
8.104 + action_panel.contents.clear
8.105 + action_panel.contents ++= cs
8.106 + layout_panel.revalidate
8.107 + layout_panel.repaint
8.108 + }
8.109 +
8.110 +
8.111 + /* close */
8.112 +
8.113 + peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
8.114 +
8.115 + override def closeOperation {
8.116 + if (_return_code.isDefined) conclude()
8.117 + else stopping()
8.118 + }
8.119 +
8.120 + def stopping()
8.121 + {
8.122 + is_stopped = true
8.123 + set_actions(new Label("Stopping ..."))
8.124 + }
8.125 +
8.126 + val stop_button = new Button("Stop") {
8.127 + reactions += { case ButtonClicked(_) => stopping() }
8.128 + }
8.129 +
8.130 + var do_auto_close = true
8.131 + def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
8.132 +
8.133 + val auto_close = new CheckBox("Auto close") {
8.134 + reactions += {
8.135 + case ButtonClicked(_) => do_auto_close = this.selected
8.136 + if (can_auto_close) conclude()
8.137 + }
8.138 + }
8.139 + auto_close.selected = do_auto_close
8.140 + auto_close.tooltip = "Automatically close dialog when finished"
8.141 +
8.142 + set_actions(stop_button, auto_close)
8.143 +
8.144 +
8.145 + /* exit */
8.146 +
8.147 + val delay_exit =
8.148 + Swing_Thread.delay_first(Time.seconds(1.0))
8.149 + {
8.150 + if (can_auto_close) conclude()
8.151 + else {
8.152 + val button =
8.153 + new Button(if (_return_code == Some(0)) "OK" else "Exit") {
8.154 + reactions += { case ButtonClicked(_) => conclude() }
8.155 + }
8.156 + set_actions(button)
8.157 + button.peer.getRootPane.setDefaultButton(button.peer)
8.158 + }
8.159 + }
8.160 + }
8.161 +
8.162 +
8.163 + /* progress operations */
8.164 +
8.165 + def title(txt: String): Unit =
8.166 + Swing_Thread.later {
8.167 + _title = txt
8.168 + _window.foreach(window => window.title = txt)
8.169 + }
8.170 +
8.171 + def return_code(rc: Int): Unit =
8.172 + Swing_Thread.later {
8.173 + _return_code = Some(rc)
8.174 + _window match {
8.175 + case None => conclude()
8.176 + case Some(window) => window.delay_exit.invoke
8.177 + }
8.178 + }
8.179 +
8.180 + override def echo(txt: String): Unit =
8.181 + Swing_Thread.later {
8.182 + val window = check_window()
8.183 + window.text.append(txt + "\n")
8.184 + val vertical = window.scroll_text.peer.getVerticalScrollBar
8.185 + vertical.setValue(vertical.getMaximum)
8.186 + }
8.187 +
8.188 + override def theory(session: String, theory: String): Unit =
8.189 + echo(session + ": theory " + theory)
8.190 +
8.191 + @volatile private var is_stopped = false
8.192 + override def stopped: Boolean = is_stopped
8.193 +
8.194 +
8.195 + /* system operations */
8.196 +
8.197 + def execute(cwd: JFile, env: Map[String, String], args: String*): Int =
8.198 + {
8.199 + val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
8.200 + proc.getOutputStream.close
8.201 +
8.202 + val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
8.203 + try {
8.204 + var line = stdout.readLine
8.205 + while (line != null) {
8.206 + echo(line)
8.207 + line = stdout.readLine
8.208 + }
8.209 + }
8.210 + finally { stdout.close }
8.211 +
8.212 + proc.waitFor
8.213 + }
8.214 +}
8.215 +
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Pure/GUI/wrap_panel.scala Sun Sep 22 14:30:34 2013 +0200
9.3 @@ -0,0 +1,123 @@
9.4 +/* Title: Pure/GUI/wrap_panel.scala
9.5 + Author: Makarius
9.6 +
9.7 +Panel with improved FlowLayout for wrapping of components over
9.8 +multiple lines, see also
9.9 +http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
9.10 +scala.swing.FlowPanel.
9.11 +*/
9.12 +
9.13 +package isabelle
9.14 +
9.15 +
9.16 +import java.awt.{FlowLayout, Container, Dimension}
9.17 +import javax.swing.{JComponent, JPanel, JScrollPane}
9.18 +
9.19 +import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane}
9.20 +
9.21 +
9.22 +object Wrap_Panel
9.23 +{
9.24 + val Alignment = FlowPanel.Alignment
9.25 +
9.26 + class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
9.27 + extends FlowLayout(align: Int, hgap: Int, vgap: Int)
9.28 + {
9.29 + override def preferredLayoutSize(target: Container): Dimension =
9.30 + layout_size(target, true)
9.31 +
9.32 + override def minimumLayoutSize(target: Container): Dimension =
9.33 + {
9.34 + val minimum = layout_size(target, false)
9.35 + minimum.width -= (getHgap + 1)
9.36 + minimum
9.37 + }
9.38 +
9.39 + private def layout_size(target: Container, preferred: Boolean): Dimension =
9.40 + {
9.41 + target.getTreeLock.synchronized
9.42 + {
9.43 + val target_width =
9.44 + if (target.getSize.width == 0) Integer.MAX_VALUE
9.45 + else target.getSize.width
9.46 +
9.47 + val hgap = getHgap
9.48 + val vgap = getVgap
9.49 + val insets = target.getInsets
9.50 + val horizontal_insets_and_gap = insets.left + insets.right + (hgap * 2)
9.51 + val max_width = target_width - horizontal_insets_and_gap
9.52 +
9.53 +
9.54 + /* fit components into rows */
9.55 +
9.56 + val dim = new Dimension(0, 0)
9.57 + var row_width = 0
9.58 + var row_height = 0
9.59 + def add_row()
9.60 + {
9.61 + dim.width = dim.width max row_width
9.62 + if (dim.height > 0) dim.height += vgap
9.63 + dim.height += row_height
9.64 + }
9.65 +
9.66 + for {
9.67 + i <- 0 until target.getComponentCount
9.68 + m = target.getComponent(i)
9.69 + if m.isVisible
9.70 + d = if (preferred) m.getPreferredSize else m.getMinimumSize()
9.71 + }
9.72 + {
9.73 + if (row_width + d.width > max_width) {
9.74 + add_row()
9.75 + row_width = 0
9.76 + row_height = 0
9.77 + }
9.78 +
9.79 + if (row_width != 0) row_width += hgap
9.80 +
9.81 + row_width += d.width
9.82 + row_height = row_height max d.height
9.83 + }
9.84 + add_row()
9.85 +
9.86 + dim.width += horizontal_insets_and_gap
9.87 + dim.height += insets.top + insets.bottom + vgap * 2
9.88 +
9.89 +
9.90 + /* special treatment for ScrollPane */
9.91 +
9.92 + val scroll_pane =
9.93 + GUI.ancestors(target).exists(
9.94 + {
9.95 + case _: JScrollPane => true
9.96 + case c: JComponent if Component.wrap(c).isInstanceOf[ScrollPane] => true
9.97 + case _ => false
9.98 + })
9.99 + if (scroll_pane && target.isValid)
9.100 + dim.width -= (hgap + 1)
9.101 +
9.102 + dim
9.103 + }
9.104 + }
9.105 + }
9.106 +}
9.107 +
9.108 +
9.109 +class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*)
9.110 + extends Panel with SequentialContainer.Wrapper
9.111 +{
9.112 + override lazy val peer: JPanel =
9.113 + new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
9.114 +
9.115 + def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*)
9.116 + def this() = this(Wrap_Panel.Alignment.Center)()
9.117 +
9.118 + contents ++= contents0
9.119 +
9.120 + private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
9.121 +
9.122 + def vGap: Int = layoutManager.getVgap
9.123 + def vGap_=(n: Int) { layoutManager.setVgap(n) }
9.124 + def hGap: Int = layoutManager.getHgap
9.125 + def hGap_=(n: Int) { layoutManager.setHgap(n) }
9.126 +}
10.1 --- a/src/Pure/System/color_value.scala Sat Sep 21 22:48:52 2013 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,48 +0,0 @@
10.4 -/* Title: Pure/System/color_value.scala
10.5 - Module: PIDE
10.6 - Author: Makarius
10.7 -
10.8 -Cached color values.
10.9 -*/
10.10 -
10.11 -package isabelle
10.12 -
10.13 -
10.14 -import java.awt.Color
10.15 -
10.16 -
10.17 -object Color_Value
10.18 -{
10.19 - private var cache = Map.empty[String, Color]
10.20 -
10.21 - def parse(s: String): Color =
10.22 - {
10.23 - val i = java.lang.Long.parseLong(s, 16)
10.24 - val r = ((i >> 24) & 0xFF).toInt
10.25 - val g = ((i >> 16) & 0xFF).toInt
10.26 - val b = ((i >> 8) & 0xFF).toInt
10.27 - val a = (i & 0xFF).toInt
10.28 - new Color(r, g, b, a)
10.29 - }
10.30 -
10.31 - def print(c: Color): String =
10.32 - {
10.33 - val r = new java.lang.Integer(c.getRed)
10.34 - val g = new java.lang.Integer(c.getGreen)
10.35 - val b = new java.lang.Integer(c.getBlue)
10.36 - val a = new java.lang.Integer(c.getAlpha)
10.37 - String.format("%02x%02x%02x%02x", r, g, b, a).toUpperCase
10.38 - }
10.39 -
10.40 - def apply(s: String): Color =
10.41 - synchronized {
10.42 - cache.get(s) match {
10.43 - case Some(c) => c
10.44 - case None =>
10.45 - val c = parse(s)
10.46 - cache += (s -> c)
10.47 - c
10.48 - }
10.49 - }
10.50 -}
10.51 -
11.1 --- a/src/Pure/System/gui.scala Sat Sep 21 22:48:52 2013 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,154 +0,0 @@
11.4 -/* Title: Pure/System/gui.scala
11.5 - Author: Makarius
11.6 -
11.7 -Basic GUI tools (for AWT/Swing).
11.8 -*/
11.9 -
11.10 -package isabelle
11.11 -
11.12 -
11.13 -import java.awt.{Image, Component, Container, Toolkit, Window}
11.14 -import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow}
11.15 -
11.16 -import scala.swing.{ComboBox, TextArea, ScrollPane}
11.17 -import scala.swing.event.SelectionChanged
11.18 -
11.19 -
11.20 -object GUI
11.21 -{
11.22 - /* Swing look-and-feel */
11.23 -
11.24 - def get_laf(): String =
11.25 - {
11.26 - def laf(name: String): Option[String] =
11.27 - UIManager.getInstalledLookAndFeels().find(_.getName == name).map(_.getClassName)
11.28 -
11.29 - if (Platform.is_windows || Platform.is_macos)
11.30 - UIManager.getSystemLookAndFeelClassName()
11.31 - else
11.32 - laf("Nimbus") orElse laf("GTK+") getOrElse
11.33 - UIManager.getCrossPlatformLookAndFeelClassName()
11.34 - }
11.35 -
11.36 - def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
11.37 -
11.38 -
11.39 - /* simple dialogs */
11.40 -
11.41 - def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
11.42 - : ScrollPane =
11.43 - {
11.44 - val text = new TextArea(txt)
11.45 - if (width > 0) text.columns = width
11.46 - if (height > 0 && split_lines(txt).length > height) text.rows = height
11.47 - text.editable = editable
11.48 - new ScrollPane(text)
11.49 - }
11.50 -
11.51 - private def simple_dialog(kind: Int, default_title: String,
11.52 - parent: Component, title: String, message: Seq[Any])
11.53 - {
11.54 - Swing_Thread.now {
11.55 - val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
11.56 - JOptionPane.showMessageDialog(parent,
11.57 - java_message.toArray.asInstanceOf[Array[AnyRef]],
11.58 - if (title == null) default_title else title, kind)
11.59 - }
11.60 - }
11.61 -
11.62 - def dialog(parent: Component, title: String, message: Any*) =
11.63 - simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
11.64 -
11.65 - def warning_dialog(parent: Component, title: String, message: Any*) =
11.66 - simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
11.67 -
11.68 - def error_dialog(parent: Component, title: String, message: Any*) =
11.69 - simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
11.70 -
11.71 - def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
11.72 - Swing_Thread.now {
11.73 - val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
11.74 - JOptionPane.showConfirmDialog(parent,
11.75 - java_message.toArray.asInstanceOf[Array[AnyRef]], title,
11.76 - option_type, JOptionPane.QUESTION_MESSAGE)
11.77 - }
11.78 -
11.79 -
11.80 - /* zoom box */
11.81 -
11.82 - class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
11.83 - List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
11.84 - {
11.85 - val Factor = "([0-9]+)%?".r
11.86 - def parse(text: String): Int =
11.87 - text match {
11.88 - case Factor(s) =>
11.89 - val i = Integer.parseInt(s)
11.90 - if (10 <= i && i <= 1000) i else 100
11.91 - case _ => 100
11.92 - }
11.93 -
11.94 - def print(i: Int): String = i.toString + "%"
11.95 -
11.96 - def set_item(i: Int) {
11.97 - peer.getEditor match {
11.98 - case null =>
11.99 - case editor => editor.setItem(print(i))
11.100 - }
11.101 - }
11.102 -
11.103 - makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
11.104 - reactions += {
11.105 - case SelectionChanged(_) => apply_factor(parse(selection.item))
11.106 - }
11.107 - listenTo(selection)
11.108 - selection.index = 3
11.109 - prototypeDisplayValue = Some("00000%")
11.110 - }
11.111 -
11.112 -
11.113 - /* screen resolution */
11.114 -
11.115 - def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
11.116 - def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt
11.117 -
11.118 -
11.119 - /* icon */
11.120 -
11.121 - def isabelle_icon(): ImageIcon =
11.122 - new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif"))
11.123 -
11.124 - def isabelle_image(): Image = isabelle_icon().getImage
11.125 -
11.126 -
11.127 - /* component hierachy */
11.128 -
11.129 - def get_parent(component: Component): Option[Container] =
11.130 - component.getParent match {
11.131 - case null => None
11.132 - case parent => Some(parent)
11.133 - }
11.134 -
11.135 - def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
11.136 - private var next_elem = get_parent(component)
11.137 - def hasNext(): Boolean = next_elem.isDefined
11.138 - def next(): Container =
11.139 - next_elem match {
11.140 - case Some(parent) =>
11.141 - next_elem = get_parent(parent)
11.142 - parent
11.143 - case None => Iterator.empty.next()
11.144 - }
11.145 - }
11.146 -
11.147 - def parent_window(component: Component): Option[Window] =
11.148 - ancestors(component).collectFirst({ case x: Window => x })
11.149 -
11.150 - def layered_pane(component: Component): Option[JLayeredPane] =
11.151 - parent_window(component) match {
11.152 - case Some(window: JWindow) => Some(window.getLayeredPane)
11.153 - case Some(frame: JFrame) => Some(frame.getLayeredPane)
11.154 - case _ => None
11.155 - }
11.156 -}
11.157 -
12.1 --- a/src/Pure/System/gui_setup.scala Sat Sep 21 22:48:52 2013 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,71 +0,0 @@
12.4 -/* Title: Pure/System/gui_setup.scala
12.5 - Author: Makarius
12.6 -
12.7 -GUI for basic system setup.
12.8 -*/
12.9 -
12.10 -package isabelle
12.11 -
12.12 -import java.lang.System
12.13 -
12.14 -import scala.swing.{ScrollPane, Button, FlowPanel,
12.15 - BorderPanel, MainFrame, TextArea, SwingApplication}
12.16 -import scala.swing.event.ButtonClicked
12.17 -
12.18 -
12.19 -object GUI_Setup extends SwingApplication
12.20 -{
12.21 - def startup(args: Array[String]) =
12.22 - {
12.23 - GUI.init_laf()
12.24 - top.pack()
12.25 - top.visible = true
12.26 - }
12.27 -
12.28 - def top = new MainFrame {
12.29 - iconImage = GUI.isabelle_image()
12.30 -
12.31 - title = "Isabelle setup"
12.32 -
12.33 - // components
12.34 - val text = new TextArea {
12.35 - editable = false
12.36 - columns = 80
12.37 - rows = 20
12.38 - }
12.39 - val ok = new Button { text = "OK" }
12.40 - val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
12.41 -
12.42 - val panel = new BorderPanel
12.43 - panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
12.44 - panel.layout(ok_panel) = BorderPanel.Position.South
12.45 - contents = panel
12.46 -
12.47 - // values
12.48 - text.append("JVM name: " + Platform.jvm_name + "\n")
12.49 - text.append("JVM platform: " + Platform.jvm_platform + "\n")
12.50 - text.append("JVM home: " + java.lang.System.getProperty("java.home", "") + "\n")
12.51 - try {
12.52 - Isabelle_System.init()
12.53 - if (Platform.is_windows)
12.54 - text.append("Cygwin root: " + Isabelle_System.get_cygwin_root() + "\n")
12.55 - text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n")
12.56 - text.append("Isabelle platform: " + Isabelle_System.getenv("ISABELLE_PLATFORM") + "\n")
12.57 - val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
12.58 - if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
12.59 - text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n")
12.60 - val isabelle_home_windows = Isabelle_System.getenv("ISABELLE_HOME_WINDOWS")
12.61 - if (isabelle_home_windows != "")
12.62 - text.append("Isabelle home (Windows): " + isabelle_home_windows + "\n")
12.63 - text.append("Isabelle JDK home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n")
12.64 - }
12.65 - catch { case ERROR(msg) => text.append(msg + "\n") }
12.66 -
12.67 - // reactions
12.68 - listenTo(ok)
12.69 - reactions += {
12.70 - case ButtonClicked(`ok`) => sys.exit(0)
12.71 - }
12.72 - }
12.73 -}
12.74 -
13.1 --- a/src/Pure/System/html5_panel.scala Sat Sep 21 22:48:52 2013 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,78 +0,0 @@
13.4 -/* Title: Pure/System/html5_panel.scala
13.5 - Author: Makarius
13.6 -
13.7 -HTML5 panel based on Java FX WebView.
13.8 -*/
13.9 -
13.10 -package isabelle
13.11 -
13.12 -
13.13 -import javafx.scene.Scene
13.14 -import javafx.scene.web.{WebView, WebEngine}
13.15 -import javafx.scene.input.KeyEvent
13.16 -import javafx.scene.text.FontSmoothingType
13.17 -import javafx.scene.layout.{HBox, VBox, Priority}
13.18 -import javafx.geometry.{HPos, VPos, Insets}
13.19 -import javafx.event.EventHandler
13.20 -
13.21 -
13.22 -// see http://netbeans.org/bugzilla/show_bug.cgi?id=210414
13.23 -// and http://hg.netbeans.org/jet-main/rev/a88434cec458
13.24 -private class Web_View_Workaround extends javafx.scene.layout.Pane
13.25 -{
13.26 - VBox.setVgrow(this, Priority.ALWAYS)
13.27 - HBox.setHgrow(this, Priority.ALWAYS)
13.28 -
13.29 - setMaxWidth(java.lang.Double.MAX_VALUE)
13.30 - setMaxHeight(java.lang.Double.MAX_VALUE)
13.31 -
13.32 - val web_view = new WebView
13.33 - web_view.setMinSize(500, 400)
13.34 - web_view.setPrefSize(500, 400)
13.35 -
13.36 - getChildren().add(web_view)
13.37 -
13.38 - override protected def layoutChildren()
13.39 - {
13.40 - val managed = getManagedChildren()
13.41 - val width = getWidth()
13.42 - val height = getHeight()
13.43 - val top = getInsets().getTop()
13.44 - val right = getInsets().getRight()
13.45 - val left = getInsets().getLeft()
13.46 - val bottom = getInsets().getBottom()
13.47 -
13.48 - for (i <- 0 until managed.size)
13.49 - layoutInArea(managed.get(i), left, top,
13.50 - width - left - right, height - top - bottom,
13.51 - 0, Insets.EMPTY, true, true, HPos.CENTER, VPos.CENTER)
13.52 - }
13.53 -}
13.54 -
13.55 -
13.56 -class HTML5_Panel extends javafx.embed.swing.JFXPanel
13.57 -{
13.58 - private val future =
13.59 - JFX_Thread.future {
13.60 - val pane = new Web_View_Workaround
13.61 -
13.62 - val web_view = pane.web_view
13.63 - web_view.setFontSmoothingType(FontSmoothingType.GRAY)
13.64 - web_view.setOnKeyTyped(new EventHandler[KeyEvent] {
13.65 - def handle(e: KeyEvent) {
13.66 - if (e.isControlDown && e.getCharacter == "0")
13.67 - web_view.setFontScale(1.0)
13.68 - if (e.isControlDown && e.getCharacter == "+")
13.69 - web_view.setFontScale(web_view.getFontScale * 1.1)
13.70 - else if (e.isControlDown && e.getCharacter == "-")
13.71 - web_view.setFontScale(web_view.getFontScale / 1.1)
13.72 - }
13.73 - })
13.74 -
13.75 - setScene(new Scene(pane))
13.76 - pane
13.77 - }
13.78 -
13.79 - def web_view: WebView = future.join.web_view
13.80 - def web_engine: WebEngine = web_view.getEngine
13.81 -}
14.1 --- a/src/Pure/System/jfx_thread.scala Sat Sep 21 22:48:52 2013 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,38 +0,0 @@
14.4 -/* Title: Pure/System/jfx_thread.scala
14.5 - Module: PIDE
14.6 - Author: Makarius
14.7 -
14.8 -Evaluation within the Java FX application thread.
14.9 -*/
14.10 -
14.11 -package isabelle
14.12 -
14.13 -import javafx.application.{Platform => JFX_Platform}
14.14 -
14.15 -
14.16 -object JFX_Thread
14.17 -{
14.18 - /* checks */
14.19 -
14.20 - def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
14.21 - def require() = Predef.require(JFX_Platform.isFxApplicationThread())
14.22 -
14.23 -
14.24 - /* asynchronous context switch */
14.25 -
14.26 - def later(body: => Unit)
14.27 - {
14.28 - if (JFX_Platform.isFxApplicationThread()) body
14.29 - else JFX_Platform.runLater(new Runnable { def run = body })
14.30 - }
14.31 -
14.32 - def future[A](body: => A): Future[A] =
14.33 - {
14.34 - if (JFX_Platform.isFxApplicationThread()) Future.value(body)
14.35 - else {
14.36 - val promise = Future.promise[A]
14.37 - later { promise.fulfill_result(Exn.capture(body)) }
14.38 - promise
14.39 - }
14.40 - }
14.41 -}
15.1 --- a/src/Pure/System/swing_thread.scala Sat Sep 21 22:48:52 2013 +0200
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,106 +0,0 @@
15.4 -/* Title: Pure/System/swing_thread.scala
15.5 - Module: PIDE
15.6 - Author: Makarius
15.7 - Author: Fabian Immler, TU Munich
15.8 -
15.9 -Evaluation within the AWT/Swing thread.
15.10 -*/
15.11 -
15.12 -package isabelle
15.13 -
15.14 -import javax.swing.{SwingUtilities, Timer}
15.15 -import java.awt.event.{ActionListener, ActionEvent}
15.16 -
15.17 -
15.18 -object Swing_Thread
15.19 -{
15.20 - /* checks */
15.21 -
15.22 - def assert[A](body: => A) =
15.23 - {
15.24 - Predef.assert(SwingUtilities.isEventDispatchThread())
15.25 - body
15.26 - }
15.27 -
15.28 - def require[A](body: => A) =
15.29 - {
15.30 - Predef.require(SwingUtilities.isEventDispatchThread())
15.31 - body
15.32 - }
15.33 -
15.34 -
15.35 - /* main dispatch queue */
15.36 -
15.37 - def now[A](body: => A): A =
15.38 - {
15.39 - if (SwingUtilities.isEventDispatchThread()) body
15.40 - else {
15.41 - lazy val result = { assert(); Exn.capture(body) }
15.42 - SwingUtilities.invokeAndWait(new Runnable { def run = result })
15.43 - Exn.release(result)
15.44 - }
15.45 - }
15.46 -
15.47 - def future[A](body: => A): Future[A] =
15.48 - {
15.49 - if (SwingUtilities.isEventDispatchThread()) Future.value(body)
15.50 - else Future.fork { now(body) }
15.51 - }
15.52 -
15.53 - def later(body: => Unit)
15.54 - {
15.55 - if (SwingUtilities.isEventDispatchThread()) body
15.56 - else SwingUtilities.invokeLater(new Runnable { def run = body })
15.57 - }
15.58 -
15.59 -
15.60 - /* delayed actions */
15.61 -
15.62 - abstract class Delay extends
15.63 - {
15.64 - def invoke(): Unit
15.65 - def revoke(): Unit
15.66 - def postpone(time: Time): Unit
15.67 - }
15.68 -
15.69 - private def delayed_action(first: Boolean)(time: => Time)(action: => Unit): Delay =
15.70 - new Delay {
15.71 - private val timer = new Timer(time.ms.toInt, null)
15.72 - timer.setRepeats(false)
15.73 - timer.addActionListener(new ActionListener {
15.74 - override def actionPerformed(e: ActionEvent) {
15.75 - assert()
15.76 - timer.setInitialDelay(time.ms.toInt)
15.77 - action
15.78 - }
15.79 - })
15.80 -
15.81 - def invoke()
15.82 - {
15.83 - require()
15.84 - if (first) timer.start() else timer.restart()
15.85 - }
15.86 -
15.87 - def revoke()
15.88 - {
15.89 - require()
15.90 - timer.stop()
15.91 - timer.setInitialDelay(time.ms.toInt)
15.92 - }
15.93 -
15.94 - def postpone(alt_time: Time)
15.95 - {
15.96 - require()
15.97 - if (timer.isRunning) {
15.98 - timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
15.99 - timer.restart()
15.100 - }
15.101 - }
15.102 - }
15.103 -
15.104 - // delayed action after first invocation
15.105 - def delay_first = delayed_action(true) _
15.106 -
15.107 - // delayed action after last invocation
15.108 - def delay_last = delayed_action(false) _
15.109 -}
16.1 --- a/src/Pure/System/system_dialog.scala Sat Sep 21 22:48:52 2013 +0200
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,212 +0,0 @@
16.4 -/* Title: Pure/Tools/system_dialog.scala
16.5 - Author: Makarius
16.6 -
16.7 -Dialog for system processes, with optional output window.
16.8 -*/
16.9 -
16.10 -package isabelle
16.11 -
16.12 -
16.13 -import java.awt.{GraphicsEnvironment, Point, Font}
16.14 -import javax.swing.WindowConstants
16.15 -import java.io.{File => JFile, BufferedReader, InputStreamReader}
16.16 -
16.17 -import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
16.18 - BorderPanel, Frame, TextArea, Component, Label}
16.19 -import scala.swing.event.ButtonClicked
16.20 -
16.21 -
16.22 -class System_Dialog extends Build.Progress
16.23 -{
16.24 - /* GUI state -- owned by Swing thread */
16.25 -
16.26 - private var _title = "Isabelle"
16.27 - private var _window: Option[Window] = None
16.28 - private var _return_code: Option[Int] = None
16.29 -
16.30 - private def check_window(): Window =
16.31 - {
16.32 - Swing_Thread.require()
16.33 -
16.34 - _window match {
16.35 - case Some(window) => window
16.36 - case None =>
16.37 - val window = new Window
16.38 - _window = Some(window)
16.39 -
16.40 - window.pack()
16.41 - val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
16.42 - window.location =
16.43 - new Point(point.x - window.size.width / 2, point.y - window.size.height / 2)
16.44 - window.visible = true
16.45 -
16.46 - window
16.47 - }
16.48 - }
16.49 -
16.50 - private val result = Future.promise[Int]
16.51 -
16.52 - private def conclude()
16.53 - {
16.54 - Swing_Thread.require()
16.55 - require(_return_code.isDefined)
16.56 -
16.57 - _window match {
16.58 - case None =>
16.59 - case Some(window) =>
16.60 - window.visible = false
16.61 - window.dispose
16.62 - _window = None
16.63 - }
16.64 -
16.65 - try { result.fulfill(_return_code.get) }
16.66 - catch { case ERROR(_) => }
16.67 - }
16.68 -
16.69 - def join(): Int = result.join
16.70 - def join_exit(): Nothing = sys.exit(join)
16.71 -
16.72 -
16.73 - /* window */
16.74 -
16.75 - private class Window extends Frame
16.76 - {
16.77 - title = _title
16.78 - iconImage = GUI.isabelle_image()
16.79 -
16.80 -
16.81 - /* text */
16.82 -
16.83 - val text = new TextArea {
16.84 - font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
16.85 - editable = false
16.86 - columns = 50
16.87 - rows = 20
16.88 - }
16.89 -
16.90 - val scroll_text = new ScrollPane(text)
16.91 -
16.92 -
16.93 - /* layout panel with dynamic actions */
16.94 -
16.95 - val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
16.96 - val layout_panel = new BorderPanel
16.97 - layout_panel.layout(scroll_text) = BorderPanel.Position.Center
16.98 - layout_panel.layout(action_panel) = BorderPanel.Position.South
16.99 -
16.100 - contents = layout_panel
16.101 -
16.102 - def set_actions(cs: Component*)
16.103 - {
16.104 - action_panel.contents.clear
16.105 - action_panel.contents ++= cs
16.106 - layout_panel.revalidate
16.107 - layout_panel.repaint
16.108 - }
16.109 -
16.110 -
16.111 - /* close */
16.112 -
16.113 - peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
16.114 -
16.115 - override def closeOperation {
16.116 - if (_return_code.isDefined) conclude()
16.117 - else stopping()
16.118 - }
16.119 -
16.120 - def stopping()
16.121 - {
16.122 - is_stopped = true
16.123 - set_actions(new Label("Stopping ..."))
16.124 - }
16.125 -
16.126 - val stop_button = new Button("Stop") {
16.127 - reactions += { case ButtonClicked(_) => stopping() }
16.128 - }
16.129 -
16.130 - var do_auto_close = true
16.131 - def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
16.132 -
16.133 - val auto_close = new CheckBox("Auto close") {
16.134 - reactions += {
16.135 - case ButtonClicked(_) => do_auto_close = this.selected
16.136 - if (can_auto_close) conclude()
16.137 - }
16.138 - }
16.139 - auto_close.selected = do_auto_close
16.140 - auto_close.tooltip = "Automatically close dialog when finished"
16.141 -
16.142 - set_actions(stop_button, auto_close)
16.143 -
16.144 -
16.145 - /* exit */
16.146 -
16.147 - val delay_exit =
16.148 - Swing_Thread.delay_first(Time.seconds(1.0))
16.149 - {
16.150 - if (can_auto_close) conclude()
16.151 - else {
16.152 - val button =
16.153 - new Button(if (_return_code == Some(0)) "OK" else "Exit") {
16.154 - reactions += { case ButtonClicked(_) => conclude() }
16.155 - }
16.156 - set_actions(button)
16.157 - button.peer.getRootPane.setDefaultButton(button.peer)
16.158 - }
16.159 - }
16.160 - }
16.161 -
16.162 -
16.163 - /* progress operations */
16.164 -
16.165 - def title(txt: String): Unit =
16.166 - Swing_Thread.later {
16.167 - _title = txt
16.168 - _window.foreach(window => window.title = txt)
16.169 - }
16.170 -
16.171 - def return_code(rc: Int): Unit =
16.172 - Swing_Thread.later {
16.173 - _return_code = Some(rc)
16.174 - _window match {
16.175 - case None => conclude()
16.176 - case Some(window) => window.delay_exit.invoke
16.177 - }
16.178 - }
16.179 -
16.180 - override def echo(txt: String): Unit =
16.181 - Swing_Thread.later {
16.182 - val window = check_window()
16.183 - window.text.append(txt + "\n")
16.184 - val vertical = window.scroll_text.peer.getVerticalScrollBar
16.185 - vertical.setValue(vertical.getMaximum)
16.186 - }
16.187 -
16.188 - override def theory(session: String, theory: String): Unit =
16.189 - echo(session + ": theory " + theory)
16.190 -
16.191 - @volatile private var is_stopped = false
16.192 - override def stopped: Boolean = is_stopped
16.193 -
16.194 -
16.195 - /* system operations */
16.196 -
16.197 - def execute(cwd: JFile, env: Map[String, String], args: String*): Int =
16.198 - {
16.199 - val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
16.200 - proc.getOutputStream.close
16.201 -
16.202 - val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
16.203 - try {
16.204 - var line = stdout.readLine
16.205 - while (line != null) {
16.206 - echo(line)
16.207 - line = stdout.readLine
16.208 - }
16.209 - }
16.210 - finally { stdout.close }
16.211 -
16.212 - proc.waitFor
16.213 - }
16.214 -}
16.215 -
17.1 --- a/src/Pure/System/wrap_panel.scala Sat Sep 21 22:48:52 2013 +0200
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,123 +0,0 @@
17.4 -/* Title: Pure/System/wrap_panel.scala
17.5 - Author: Makarius
17.6 -
17.7 -Panel with improved FlowLayout for wrapping of components over
17.8 -multiple lines, see also
17.9 -http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
17.10 -scala.swing.FlowPanel.
17.11 -*/
17.12 -
17.13 -package isabelle
17.14 -
17.15 -
17.16 -import java.awt.{FlowLayout, Container, Dimension}
17.17 -import javax.swing.{JComponent, JPanel, JScrollPane}
17.18 -
17.19 -import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane}
17.20 -
17.21 -
17.22 -object Wrap_Panel
17.23 -{
17.24 - val Alignment = FlowPanel.Alignment
17.25 -
17.26 - class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
17.27 - extends FlowLayout(align: Int, hgap: Int, vgap: Int)
17.28 - {
17.29 - override def preferredLayoutSize(target: Container): Dimension =
17.30 - layout_size(target, true)
17.31 -
17.32 - override def minimumLayoutSize(target: Container): Dimension =
17.33 - {
17.34 - val minimum = layout_size(target, false)
17.35 - minimum.width -= (getHgap + 1)
17.36 - minimum
17.37 - }
17.38 -
17.39 - private def layout_size(target: Container, preferred: Boolean): Dimension =
17.40 - {
17.41 - target.getTreeLock.synchronized
17.42 - {
17.43 - val target_width =
17.44 - if (target.getSize.width == 0) Integer.MAX_VALUE
17.45 - else target.getSize.width
17.46 -
17.47 - val hgap = getHgap
17.48 - val vgap = getVgap
17.49 - val insets = target.getInsets
17.50 - val horizontal_insets_and_gap = insets.left + insets.right + (hgap * 2)
17.51 - val max_width = target_width - horizontal_insets_and_gap
17.52 -
17.53 -
17.54 - /* fit components into rows */
17.55 -
17.56 - val dim = new Dimension(0, 0)
17.57 - var row_width = 0
17.58 - var row_height = 0
17.59 - def add_row()
17.60 - {
17.61 - dim.width = dim.width max row_width
17.62 - if (dim.height > 0) dim.height += vgap
17.63 - dim.height += row_height
17.64 - }
17.65 -
17.66 - for {
17.67 - i <- 0 until target.getComponentCount
17.68 - m = target.getComponent(i)
17.69 - if m.isVisible
17.70 - d = if (preferred) m.getPreferredSize else m.getMinimumSize()
17.71 - }
17.72 - {
17.73 - if (row_width + d.width > max_width) {
17.74 - add_row()
17.75 - row_width = 0
17.76 - row_height = 0
17.77 - }
17.78 -
17.79 - if (row_width != 0) row_width += hgap
17.80 -
17.81 - row_width += d.width
17.82 - row_height = row_height max d.height
17.83 - }
17.84 - add_row()
17.85 -
17.86 - dim.width += horizontal_insets_and_gap
17.87 - dim.height += insets.top + insets.bottom + vgap * 2
17.88 -
17.89 -
17.90 - /* special treatment for ScrollPane */
17.91 -
17.92 - val scroll_pane =
17.93 - GUI.ancestors(target).exists(
17.94 - {
17.95 - case _: JScrollPane => true
17.96 - case c: JComponent if Component.wrap(c).isInstanceOf[ScrollPane] => true
17.97 - case _ => false
17.98 - })
17.99 - if (scroll_pane && target.isValid)
17.100 - dim.width -= (hgap + 1)
17.101 -
17.102 - dim
17.103 - }
17.104 - }
17.105 - }
17.106 -}
17.107 -
17.108 -
17.109 -class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*)
17.110 - extends Panel with SequentialContainer.Wrapper
17.111 -{
17.112 - override lazy val peer: JPanel =
17.113 - new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
17.114 -
17.115 - def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*)
17.116 - def this() = this(Wrap_Panel.Alignment.Center)()
17.117 -
17.118 - contents ++= contents0
17.119 -
17.120 - private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
17.121 -
17.122 - def vGap: Int = layoutManager.getVgap
17.123 - def vGap_=(n: Int) { layoutManager.setVgap(n) }
17.124 - def hGap: Int = layoutManager.getHgap
17.125 - def hGap_=(n: Int) { layoutManager.setHgap(n) }
17.126 -}
18.1 --- a/src/Pure/build-jars Sat Sep 21 22:48:52 2013 +0200
18.2 +++ b/src/Pure/build-jars Sun Sep 22 14:30:34 2013 +0200
18.3 @@ -29,6 +29,15 @@
18.4 General/time.scala
18.5 General/timing.scala
18.6 General/xz_file.scala
18.7 + GUI/color_value.scala
18.8 + GUI/gui.scala
18.9 + GUI/gui_setup.scala
18.10 + GUI/html5_panel.scala
18.11 + GUI/jfx_thread.scala
18.12 + GUI/popup.scala
18.13 + GUI/swing_thread.scala
18.14 + GUI/system_dialog.scala
18.15 + GUI/wrap_panel.scala
18.16 Isar/completion.scala
18.17 Isar/keyword.scala
18.18 Isar/outer_syntax.scala
18.19 @@ -45,27 +54,19 @@
18.20 PIDE/text.scala
18.21 PIDE/xml.scala
18.22 PIDE/yxml.scala
18.23 - System/color_value.scala
18.24 System/command_line.scala
18.25 System/event_bus.scala
18.26 - System/gui.scala
18.27 - System/gui_setup.scala
18.28 - System/html5_panel.scala
18.29 System/interrupt.scala
18.30 System/invoke_scala.scala
18.31 System/isabelle_charset.scala
18.32 System/isabelle_font.scala
18.33 System/isabelle_process.scala
18.34 System/isabelle_system.scala
18.35 - System/jfx_thread.scala
18.36 System/options.scala
18.37 System/platform.scala
18.38 System/session.scala
18.39 - System/swing_thread.scala
18.40 System/system_channel.scala
18.41 - System/system_dialog.scala
18.42 System/utf8.scala
18.43 - System/wrap_panel.scala
18.44 Thy/html.scala
18.45 Thy/present.scala
18.46 Thy/thy_header.scala
19.1 --- a/src/Tools/jEdit/lib/Tools/jedit Sat Sep 21 22:48:52 2013 +0200
19.2 +++ b/src/Tools/jEdit/lib/Tools/jedit Sun Sep 22 14:30:34 2013 +0200
19.3 @@ -31,7 +31,6 @@
19.4 "src/osx_adapter.scala"
19.5 "src/output_dockable.scala"
19.6 "src/plugin.scala"
19.7 - "src/popup.scala"
19.8 "src/pretty_text_area.scala"
19.9 "src/pretty_tooltip.scala"
19.10 "src/process_indicator.scala"
20.1 --- a/src/Tools/jEdit/src/popup.scala Sat Sep 21 22:48:52 2013 +0200
20.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
20.3 @@ -1,40 +0,0 @@
20.4 -/* Title: Tools/jEdit/src/popup.scala
20.5 - Author: Makarius
20.6 -
20.7 -Popup within layered pane.
20.8 -*/
20.9 -
20.10 -package isabelle.jedit
20.11 -
20.12 -
20.13 -import isabelle._
20.14 -
20.15 -import java.awt.{Point, Dimension}
20.16 -import javax.swing.{JLayeredPane, JComponent}
20.17 -
20.18 -
20.19 -class Popup(
20.20 - layered: JLayeredPane,
20.21 - component: JComponent,
20.22 - location: Point,
20.23 - size: Dimension)
20.24 -{
20.25 - def show
20.26 - {
20.27 - component.setLocation(location)
20.28 - component.setSize(size)
20.29 - component.setPreferredSize(size)
20.30 - component.setOpaque(true)
20.31 - layered.add(component, JLayeredPane.POPUP_LAYER)
20.32 - layered.moveToFront(component)
20.33 - layered.repaint(component.getBounds())
20.34 - }
20.35 -
20.36 - def hide
20.37 - {
20.38 - val bounds = component.getBounds()
20.39 - layered.remove(component)
20.40 - layered.repaint(bounds)
20.41 - }
20.42 -}
20.43 -