--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/color_value.scala Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,47 @@
+/* Title: Pure/GUI/color_value.scala
+ Author: Makarius
+
+Cached color values.
+*/
+
+package isabelle
+
+
+import java.awt.Color
+
+
+object Color_Value
+{
+ private var cache = Map.empty[String, Color]
+
+ def parse(s: String): Color =
+ {
+ val i = java.lang.Long.parseLong(s, 16)
+ val r = ((i >> 24) & 0xFF).toInt
+ val g = ((i >> 16) & 0xFF).toInt
+ val b = ((i >> 8) & 0xFF).toInt
+ val a = (i & 0xFF).toInt
+ new Color(r, g, b, a)
+ }
+
+ def print(c: Color): String =
+ {
+ val r = new java.lang.Integer(c.getRed)
+ val g = new java.lang.Integer(c.getGreen)
+ val b = new java.lang.Integer(c.getBlue)
+ val a = new java.lang.Integer(c.getAlpha)
+ String.format("%02x%02x%02x%02x", r, g, b, a).toUpperCase
+ }
+
+ def apply(s: String): Color =
+ synchronized {
+ cache.get(s) match {
+ case Some(c) => c
+ case None =>
+ val c = parse(s)
+ cache += (s -> c)
+ c
+ }
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/gui.scala Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,154 @@
+/* Title: Pure/GUI/gui.scala
+ Author: Makarius
+
+Basic GUI tools (for AWT/Swing).
+*/
+
+package isabelle
+
+
+import java.awt.{Image, Component, Container, Toolkit, Window}
+import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow}
+
+import scala.swing.{ComboBox, TextArea, ScrollPane}
+import scala.swing.event.SelectionChanged
+
+
+object GUI
+{
+ /* Swing look-and-feel */
+
+ def get_laf(): String =
+ {
+ def laf(name: String): Option[String] =
+ UIManager.getInstalledLookAndFeels().find(_.getName == name).map(_.getClassName)
+
+ if (Platform.is_windows || Platform.is_macos)
+ UIManager.getSystemLookAndFeelClassName()
+ else
+ laf("Nimbus") orElse laf("GTK+") getOrElse
+ UIManager.getCrossPlatformLookAndFeelClassName()
+ }
+
+ def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
+
+
+ /* simple dialogs */
+
+ def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
+ : ScrollPane =
+ {
+ val text = new TextArea(txt)
+ if (width > 0) text.columns = width
+ if (height > 0 && split_lines(txt).length > height) text.rows = height
+ 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
+
+
+ /* icon */
+
+ def isabelle_icon(): ImageIcon =
+ new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif"))
+
+ def isabelle_image(): Image = isabelle_icon().getImage
+
+
+ /* component hierachy */
+
+ def get_parent(component: Component): Option[Container] =
+ component.getParent match {
+ case null => None
+ case parent => Some(parent)
+ }
+
+ def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
+ private var next_elem = get_parent(component)
+ def hasNext(): Boolean = next_elem.isDefined
+ def next(): Container =
+ next_elem match {
+ case Some(parent) =>
+ next_elem = get_parent(parent)
+ parent
+ case None => Iterator.empty.next()
+ }
+ }
+
+ def parent_window(component: Component): Option[Window] =
+ ancestors(component).collectFirst({ case x: Window => x })
+
+ def layered_pane(component: Component): Option[JLayeredPane] =
+ parent_window(component) match {
+ case Some(window: JWindow) => Some(window.getLayeredPane)
+ case Some(frame: JFrame) => Some(frame.getLayeredPane)
+ case _ => None
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/gui_setup.scala Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,71 @@
+/* Title: Pure/GUI/gui_setup.scala
+ Author: Makarius
+
+GUI for basic system setup.
+*/
+
+package isabelle
+
+import java.lang.System
+
+import scala.swing.{ScrollPane, Button, FlowPanel,
+ BorderPanel, MainFrame, TextArea, SwingApplication}
+import scala.swing.event.ButtonClicked
+
+
+object GUI_Setup extends SwingApplication
+{
+ def startup(args: Array[String]) =
+ {
+ GUI.init_laf()
+ top.pack()
+ top.visible = true
+ }
+
+ def top = new MainFrame {
+ iconImage = GUI.isabelle_image()
+
+ title = "Isabelle setup"
+
+ // components
+ val text = new TextArea {
+ editable = false
+ columns = 80
+ rows = 20
+ }
+ val ok = new Button { text = "OK" }
+ val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
+
+ val panel = new BorderPanel
+ panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
+ panel.layout(ok_panel) = BorderPanel.Position.South
+ contents = panel
+
+ // values
+ text.append("JVM name: " + Platform.jvm_name + "\n")
+ text.append("JVM platform: " + Platform.jvm_platform + "\n")
+ text.append("JVM home: " + java.lang.System.getProperty("java.home", "") + "\n")
+ try {
+ Isabelle_System.init()
+ if (Platform.is_windows)
+ text.append("Cygwin root: " + Isabelle_System.get_cygwin_root() + "\n")
+ text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n")
+ text.append("Isabelle platform: " + Isabelle_System.getenv("ISABELLE_PLATFORM") + "\n")
+ val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
+ if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
+ text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n")
+ val isabelle_home_windows = Isabelle_System.getenv("ISABELLE_HOME_WINDOWS")
+ if (isabelle_home_windows != "")
+ text.append("Isabelle home (Windows): " + isabelle_home_windows + "\n")
+ text.append("Isabelle JDK home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n")
+ }
+ catch { case ERROR(msg) => text.append(msg + "\n") }
+
+ // reactions
+ listenTo(ok)
+ reactions += {
+ case ButtonClicked(`ok`) => sys.exit(0)
+ }
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/html5_panel.scala Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,78 @@
+/* Title: Pure/GUI/html5_panel.scala
+ Author: Makarius
+
+HTML5 panel based on Java FX WebView.
+*/
+
+package isabelle
+
+
+import javafx.scene.Scene
+import javafx.scene.web.{WebView, WebEngine}
+import javafx.scene.input.KeyEvent
+import javafx.scene.text.FontSmoothingType
+import javafx.scene.layout.{HBox, VBox, Priority}
+import javafx.geometry.{HPos, VPos, Insets}
+import javafx.event.EventHandler
+
+
+// see http://netbeans.org/bugzilla/show_bug.cgi?id=210414
+// and http://hg.netbeans.org/jet-main/rev/a88434cec458
+private class Web_View_Workaround extends javafx.scene.layout.Pane
+{
+ VBox.setVgrow(this, Priority.ALWAYS)
+ HBox.setHgrow(this, Priority.ALWAYS)
+
+ setMaxWidth(java.lang.Double.MAX_VALUE)
+ setMaxHeight(java.lang.Double.MAX_VALUE)
+
+ val web_view = new WebView
+ web_view.setMinSize(500, 400)
+ web_view.setPrefSize(500, 400)
+
+ getChildren().add(web_view)
+
+ override protected def layoutChildren()
+ {
+ val managed = getManagedChildren()
+ val width = getWidth()
+ val height = getHeight()
+ val top = getInsets().getTop()
+ val right = getInsets().getRight()
+ val left = getInsets().getLeft()
+ val bottom = getInsets().getBottom()
+
+ for (i <- 0 until managed.size)
+ layoutInArea(managed.get(i), left, top,
+ width - left - right, height - top - bottom,
+ 0, Insets.EMPTY, true, true, HPos.CENTER, VPos.CENTER)
+ }
+}
+
+
+class HTML5_Panel extends javafx.embed.swing.JFXPanel
+{
+ private val future =
+ JFX_Thread.future {
+ val pane = new Web_View_Workaround
+
+ val web_view = pane.web_view
+ web_view.setFontSmoothingType(FontSmoothingType.GRAY)
+ web_view.setOnKeyTyped(new EventHandler[KeyEvent] {
+ def handle(e: KeyEvent) {
+ if (e.isControlDown && e.getCharacter == "0")
+ web_view.setFontScale(1.0)
+ if (e.isControlDown && e.getCharacter == "+")
+ web_view.setFontScale(web_view.getFontScale * 1.1)
+ else if (e.isControlDown && e.getCharacter == "-")
+ web_view.setFontScale(web_view.getFontScale / 1.1)
+ }
+ })
+
+ setScene(new Scene(pane))
+ pane
+ }
+
+ def web_view: WebView = future.join.web_view
+ def web_engine: WebEngine = web_view.getEngine
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/jfx_thread.scala Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,37 @@
+/* Title: Pure/GUI/jfx_thread.scala
+ Author: Makarius
+
+Evaluation within the Java FX application thread.
+*/
+
+package isabelle
+
+import javafx.application.{Platform => JFX_Platform}
+
+
+object JFX_Thread
+{
+ /* checks */
+
+ def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
+ def require() = Predef.require(JFX_Platform.isFxApplicationThread())
+
+
+ /* asynchronous context switch */
+
+ def later(body: => Unit)
+ {
+ if (JFX_Platform.isFxApplicationThread()) body
+ else JFX_Platform.runLater(new Runnable { def run = body })
+ }
+
+ def future[A](body: => A): Future[A] =
+ {
+ if (JFX_Platform.isFxApplicationThread()) Future.value(body)
+ else {
+ val promise = Future.promise[A]
+ later { promise.fulfill_result(Exn.capture(body)) }
+ promise
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/popup.scala Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,38 @@
+/* Title: Pure/GUI/popup.scala
+ Author: Makarius
+
+Popup within layered pane.
+*/
+
+package isabelle
+
+
+import java.awt.{Point, Dimension}
+import javax.swing.{JLayeredPane, JComponent}
+
+
+class Popup(
+ layered: JLayeredPane,
+ component: JComponent,
+ location: Point,
+ size: Dimension)
+{
+ def show
+ {
+ component.setLocation(location)
+ component.setSize(size)
+ component.setPreferredSize(size)
+ component.setOpaque(true)
+ layered.add(component, JLayeredPane.POPUP_LAYER)
+ layered.moveToFront(component)
+ layered.repaint(component.getBounds())
+ }
+
+ def hide
+ {
+ val bounds = component.getBounds()
+ layered.remove(component)
+ layered.repaint(bounds)
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/swing_thread.scala Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,104 @@
+/* Title: Pure/GUI/swing_thread.scala
+ Author: Makarius
+
+Evaluation within the AWT/Swing thread.
+*/
+
+package isabelle
+
+import javax.swing.{SwingUtilities, Timer}
+import java.awt.event.{ActionListener, ActionEvent}
+
+
+object Swing_Thread
+{
+ /* checks */
+
+ def assert[A](body: => A) =
+ {
+ Predef.assert(SwingUtilities.isEventDispatchThread())
+ body
+ }
+
+ def require[A](body: => A) =
+ {
+ Predef.require(SwingUtilities.isEventDispatchThread())
+ body
+ }
+
+
+ /* main dispatch queue */
+
+ def now[A](body: => A): A =
+ {
+ if (SwingUtilities.isEventDispatchThread()) body
+ else {
+ lazy val result = { assert(); Exn.capture(body) }
+ SwingUtilities.invokeAndWait(new Runnable { def run = result })
+ Exn.release(result)
+ }
+ }
+
+ def future[A](body: => A): Future[A] =
+ {
+ if (SwingUtilities.isEventDispatchThread()) Future.value(body)
+ else Future.fork { now(body) }
+ }
+
+ def later(body: => Unit)
+ {
+ if (SwingUtilities.isEventDispatchThread()) body
+ else SwingUtilities.invokeLater(new Runnable { def run = body })
+ }
+
+
+ /* delayed actions */
+
+ abstract class Delay extends
+ {
+ def invoke(): Unit
+ def revoke(): Unit
+ def postpone(time: Time): Unit
+ }
+
+ private def delayed_action(first: Boolean)(time: => Time)(action: => Unit): Delay =
+ new Delay {
+ private val timer = new Timer(time.ms.toInt, null)
+ timer.setRepeats(false)
+ timer.addActionListener(new ActionListener {
+ override def actionPerformed(e: ActionEvent) {
+ assert()
+ timer.setInitialDelay(time.ms.toInt)
+ action
+ }
+ })
+
+ def invoke()
+ {
+ require()
+ if (first) timer.start() else timer.restart()
+ }
+
+ def revoke()
+ {
+ require()
+ timer.stop()
+ timer.setInitialDelay(time.ms.toInt)
+ }
+
+ def postpone(alt_time: Time)
+ {
+ require()
+ if (timer.isRunning) {
+ timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
+ timer.restart()
+ }
+ }
+ }
+
+ // delayed action after first invocation
+ def delay_first = delayed_action(true) _
+
+ // delayed action after last invocation
+ def delay_last = delayed_action(false) _
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/system_dialog.scala Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,212 @@
+/* Title: Pure/GUI/system_dialog.scala
+ Author: Makarius
+
+Dialog for system processes, with optional output window.
+*/
+
+package isabelle
+
+
+import java.awt.{GraphicsEnvironment, Point, Font}
+import javax.swing.WindowConstants
+import java.io.{File => JFile, BufferedReader, InputStreamReader}
+
+import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
+ BorderPanel, Frame, TextArea, Component, Label}
+import scala.swing.event.ButtonClicked
+
+
+class System_Dialog extends Build.Progress
+{
+ /* GUI state -- owned by Swing thread */
+
+ private var _title = "Isabelle"
+ private var _window: Option[Window] = None
+ private var _return_code: Option[Int] = None
+
+ private def check_window(): Window =
+ {
+ Swing_Thread.require()
+
+ _window match {
+ case Some(window) => window
+ case None =>
+ val window = new Window
+ _window = Some(window)
+
+ window.pack()
+ val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
+ window.location =
+ new Point(point.x - window.size.width / 2, point.y - window.size.height / 2)
+ window.visible = true
+
+ window
+ }
+ }
+
+ private val result = Future.promise[Int]
+
+ private def conclude()
+ {
+ Swing_Thread.require()
+ require(_return_code.isDefined)
+
+ _window match {
+ case None =>
+ case Some(window) =>
+ window.visible = false
+ window.dispose
+ _window = None
+ }
+
+ try { result.fulfill(_return_code.get) }
+ catch { case ERROR(_) => }
+ }
+
+ def join(): Int = result.join
+ def join_exit(): Nothing = sys.exit(join)
+
+
+ /* window */
+
+ private class Window extends Frame
+ {
+ title = _title
+ iconImage = GUI.isabelle_image()
+
+
+ /* text */
+
+ val text = new TextArea {
+ font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
+ editable = false
+ columns = 50
+ rows = 20
+ }
+
+ val scroll_text = new ScrollPane(text)
+
+
+ /* layout panel with dynamic actions */
+
+ val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
+ val layout_panel = new BorderPanel
+ layout_panel.layout(scroll_text) = BorderPanel.Position.Center
+ layout_panel.layout(action_panel) = BorderPanel.Position.South
+
+ contents = layout_panel
+
+ def set_actions(cs: Component*)
+ {
+ action_panel.contents.clear
+ action_panel.contents ++= cs
+ layout_panel.revalidate
+ layout_panel.repaint
+ }
+
+
+ /* close */
+
+ peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
+
+ override def closeOperation {
+ if (_return_code.isDefined) conclude()
+ else stopping()
+ }
+
+ def stopping()
+ {
+ is_stopped = true
+ set_actions(new Label("Stopping ..."))
+ }
+
+ val stop_button = new Button("Stop") {
+ reactions += { case ButtonClicked(_) => stopping() }
+ }
+
+ var do_auto_close = true
+ def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
+
+ val auto_close = new CheckBox("Auto close") {
+ reactions += {
+ case ButtonClicked(_) => do_auto_close = this.selected
+ if (can_auto_close) conclude()
+ }
+ }
+ auto_close.selected = do_auto_close
+ auto_close.tooltip = "Automatically close dialog when finished"
+
+ set_actions(stop_button, auto_close)
+
+
+ /* exit */
+
+ val delay_exit =
+ Swing_Thread.delay_first(Time.seconds(1.0))
+ {
+ if (can_auto_close) conclude()
+ else {
+ val button =
+ new Button(if (_return_code == Some(0)) "OK" else "Exit") {
+ reactions += { case ButtonClicked(_) => conclude() }
+ }
+ set_actions(button)
+ button.peer.getRootPane.setDefaultButton(button.peer)
+ }
+ }
+ }
+
+
+ /* progress operations */
+
+ def title(txt: String): Unit =
+ Swing_Thread.later {
+ _title = txt
+ _window.foreach(window => window.title = txt)
+ }
+
+ def return_code(rc: Int): Unit =
+ Swing_Thread.later {
+ _return_code = Some(rc)
+ _window match {
+ case None => conclude()
+ case Some(window) => window.delay_exit.invoke
+ }
+ }
+
+ override def echo(txt: String): Unit =
+ Swing_Thread.later {
+ val window = check_window()
+ window.text.append(txt + "\n")
+ val vertical = window.scroll_text.peer.getVerticalScrollBar
+ vertical.setValue(vertical.getMaximum)
+ }
+
+ override def theory(session: String, theory: String): Unit =
+ echo(session + ": theory " + theory)
+
+ @volatile private var is_stopped = false
+ override def stopped: Boolean = is_stopped
+
+
+ /* system operations */
+
+ def execute(cwd: JFile, env: Map[String, String], args: String*): Int =
+ {
+ val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
+ proc.getOutputStream.close
+
+ val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
+ try {
+ var line = stdout.readLine
+ while (line != null) {
+ echo(line)
+ line = stdout.readLine
+ }
+ }
+ finally { stdout.close }
+
+ proc.waitFor
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/wrap_panel.scala Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,123 @@
+/* Title: Pure/GUI/wrap_panel.scala
+ Author: Makarius
+
+Panel with improved FlowLayout for wrapping of components over
+multiple lines, see also
+http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
+scala.swing.FlowPanel.
+*/
+
+package isabelle
+
+
+import java.awt.{FlowLayout, Container, Dimension}
+import javax.swing.{JComponent, JPanel, JScrollPane}
+
+import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane}
+
+
+object Wrap_Panel
+{
+ val Alignment = FlowPanel.Alignment
+
+ class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
+ extends FlowLayout(align: Int, hgap: Int, vgap: Int)
+ {
+ override def preferredLayoutSize(target: Container): Dimension =
+ layout_size(target, true)
+
+ override def minimumLayoutSize(target: Container): Dimension =
+ {
+ val minimum = layout_size(target, false)
+ minimum.width -= (getHgap + 1)
+ minimum
+ }
+
+ private def layout_size(target: Container, preferred: Boolean): Dimension =
+ {
+ target.getTreeLock.synchronized
+ {
+ val target_width =
+ if (target.getSize.width == 0) Integer.MAX_VALUE
+ else target.getSize.width
+
+ val hgap = getHgap
+ val vgap = getVgap
+ val insets = target.getInsets
+ val horizontal_insets_and_gap = insets.left + insets.right + (hgap * 2)
+ val max_width = target_width - horizontal_insets_and_gap
+
+
+ /* fit components into rows */
+
+ val dim = new Dimension(0, 0)
+ var row_width = 0
+ var row_height = 0
+ def add_row()
+ {
+ dim.width = dim.width max row_width
+ if (dim.height > 0) dim.height += vgap
+ dim.height += row_height
+ }
+
+ for {
+ i <- 0 until target.getComponentCount
+ m = target.getComponent(i)
+ if m.isVisible
+ d = if (preferred) m.getPreferredSize else m.getMinimumSize()
+ }
+ {
+ if (row_width + d.width > max_width) {
+ add_row()
+ row_width = 0
+ row_height = 0
+ }
+
+ if (row_width != 0) row_width += hgap
+
+ row_width += d.width
+ row_height = row_height max d.height
+ }
+ add_row()
+
+ dim.width += horizontal_insets_and_gap
+ dim.height += insets.top + insets.bottom + vgap * 2
+
+
+ /* special treatment for ScrollPane */
+
+ val scroll_pane =
+ GUI.ancestors(target).exists(
+ {
+ case _: JScrollPane => true
+ case c: JComponent if Component.wrap(c).isInstanceOf[ScrollPane] => true
+ case _ => false
+ })
+ if (scroll_pane && target.isValid)
+ dim.width -= (hgap + 1)
+
+ dim
+ }
+ }
+ }
+}
+
+
+class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*)
+ extends Panel with SequentialContainer.Wrapper
+{
+ override lazy val peer: JPanel =
+ new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
+
+ def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*)
+ def this() = this(Wrap_Panel.Alignment.Center)()
+
+ contents ++= contents0
+
+ private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
+
+ def vGap: Int = layoutManager.getVgap
+ def vGap_=(n: Int) { layoutManager.setVgap(n) }
+ def hGap: Int = layoutManager.getHgap
+ def hGap_=(n: Int) { layoutManager.setHgap(n) }
+}
--- a/src/Pure/System/color_value.scala Sat Sep 21 22:48:52 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-/* Title: Pure/System/color_value.scala
- Module: PIDE
- Author: Makarius
-
-Cached color values.
-*/
-
-package isabelle
-
-
-import java.awt.Color
-
-
-object Color_Value
-{
- private var cache = Map.empty[String, Color]
-
- def parse(s: String): Color =
- {
- val i = java.lang.Long.parseLong(s, 16)
- val r = ((i >> 24) & 0xFF).toInt
- val g = ((i >> 16) & 0xFF).toInt
- val b = ((i >> 8) & 0xFF).toInt
- val a = (i & 0xFF).toInt
- new Color(r, g, b, a)
- }
-
- def print(c: Color): String =
- {
- val r = new java.lang.Integer(c.getRed)
- val g = new java.lang.Integer(c.getGreen)
- val b = new java.lang.Integer(c.getBlue)
- val a = new java.lang.Integer(c.getAlpha)
- String.format("%02x%02x%02x%02x", r, g, b, a).toUpperCase
- }
-
- def apply(s: String): Color =
- synchronized {
- cache.get(s) match {
- case Some(c) => c
- case None =>
- val c = parse(s)
- cache += (s -> c)
- c
- }
- }
-}
-
--- a/src/Pure/System/gui.scala Sat Sep 21 22:48:52 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,154 +0,0 @@
-/* Title: Pure/System/gui.scala
- Author: Makarius
-
-Basic GUI tools (for AWT/Swing).
-*/
-
-package isabelle
-
-
-import java.awt.{Image, Component, Container, Toolkit, Window}
-import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow}
-
-import scala.swing.{ComboBox, TextArea, ScrollPane}
-import scala.swing.event.SelectionChanged
-
-
-object GUI
-{
- /* Swing look-and-feel */
-
- def get_laf(): String =
- {
- def laf(name: String): Option[String] =
- UIManager.getInstalledLookAndFeels().find(_.getName == name).map(_.getClassName)
-
- if (Platform.is_windows || Platform.is_macos)
- UIManager.getSystemLookAndFeelClassName()
- else
- laf("Nimbus") orElse laf("GTK+") getOrElse
- UIManager.getCrossPlatformLookAndFeelClassName()
- }
-
- def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
-
-
- /* simple dialogs */
-
- def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
- : ScrollPane =
- {
- val text = new TextArea(txt)
- if (width > 0) text.columns = width
- if (height > 0 && split_lines(txt).length > height) text.rows = height
- 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
-
-
- /* icon */
-
- def isabelle_icon(): ImageIcon =
- new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif"))
-
- def isabelle_image(): Image = isabelle_icon().getImage
-
-
- /* component hierachy */
-
- def get_parent(component: Component): Option[Container] =
- component.getParent match {
- case null => None
- case parent => Some(parent)
- }
-
- def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
- private var next_elem = get_parent(component)
- def hasNext(): Boolean = next_elem.isDefined
- def next(): Container =
- next_elem match {
- case Some(parent) =>
- next_elem = get_parent(parent)
- parent
- case None => Iterator.empty.next()
- }
- }
-
- def parent_window(component: Component): Option[Window] =
- ancestors(component).collectFirst({ case x: Window => x })
-
- def layered_pane(component: Component): Option[JLayeredPane] =
- parent_window(component) match {
- case Some(window: JWindow) => Some(window.getLayeredPane)
- case Some(frame: JFrame) => Some(frame.getLayeredPane)
- case _ => None
- }
-}
-
--- a/src/Pure/System/gui_setup.scala Sat Sep 21 22:48:52 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
-/* Title: Pure/System/gui_setup.scala
- Author: Makarius
-
-GUI for basic system setup.
-*/
-
-package isabelle
-
-import java.lang.System
-
-import scala.swing.{ScrollPane, Button, FlowPanel,
- BorderPanel, MainFrame, TextArea, SwingApplication}
-import scala.swing.event.ButtonClicked
-
-
-object GUI_Setup extends SwingApplication
-{
- def startup(args: Array[String]) =
- {
- GUI.init_laf()
- top.pack()
- top.visible = true
- }
-
- def top = new MainFrame {
- iconImage = GUI.isabelle_image()
-
- title = "Isabelle setup"
-
- // components
- val text = new TextArea {
- editable = false
- columns = 80
- rows = 20
- }
- val ok = new Button { text = "OK" }
- val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
-
- val panel = new BorderPanel
- panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
- panel.layout(ok_panel) = BorderPanel.Position.South
- contents = panel
-
- // values
- text.append("JVM name: " + Platform.jvm_name + "\n")
- text.append("JVM platform: " + Platform.jvm_platform + "\n")
- text.append("JVM home: " + java.lang.System.getProperty("java.home", "") + "\n")
- try {
- Isabelle_System.init()
- if (Platform.is_windows)
- text.append("Cygwin root: " + Isabelle_System.get_cygwin_root() + "\n")
- text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n")
- text.append("Isabelle platform: " + Isabelle_System.getenv("ISABELLE_PLATFORM") + "\n")
- val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
- if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
- text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n")
- val isabelle_home_windows = Isabelle_System.getenv("ISABELLE_HOME_WINDOWS")
- if (isabelle_home_windows != "")
- text.append("Isabelle home (Windows): " + isabelle_home_windows + "\n")
- text.append("Isabelle JDK home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n")
- }
- catch { case ERROR(msg) => text.append(msg + "\n") }
-
- // reactions
- listenTo(ok)
- reactions += {
- case ButtonClicked(`ok`) => sys.exit(0)
- }
- }
-}
-
--- a/src/Pure/System/html5_panel.scala Sat Sep 21 22:48:52 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-/* Title: Pure/System/html5_panel.scala
- Author: Makarius
-
-HTML5 panel based on Java FX WebView.
-*/
-
-package isabelle
-
-
-import javafx.scene.Scene
-import javafx.scene.web.{WebView, WebEngine}
-import javafx.scene.input.KeyEvent
-import javafx.scene.text.FontSmoothingType
-import javafx.scene.layout.{HBox, VBox, Priority}
-import javafx.geometry.{HPos, VPos, Insets}
-import javafx.event.EventHandler
-
-
-// see http://netbeans.org/bugzilla/show_bug.cgi?id=210414
-// and http://hg.netbeans.org/jet-main/rev/a88434cec458
-private class Web_View_Workaround extends javafx.scene.layout.Pane
-{
- VBox.setVgrow(this, Priority.ALWAYS)
- HBox.setHgrow(this, Priority.ALWAYS)
-
- setMaxWidth(java.lang.Double.MAX_VALUE)
- setMaxHeight(java.lang.Double.MAX_VALUE)
-
- val web_view = new WebView
- web_view.setMinSize(500, 400)
- web_view.setPrefSize(500, 400)
-
- getChildren().add(web_view)
-
- override protected def layoutChildren()
- {
- val managed = getManagedChildren()
- val width = getWidth()
- val height = getHeight()
- val top = getInsets().getTop()
- val right = getInsets().getRight()
- val left = getInsets().getLeft()
- val bottom = getInsets().getBottom()
-
- for (i <- 0 until managed.size)
- layoutInArea(managed.get(i), left, top,
- width - left - right, height - top - bottom,
- 0, Insets.EMPTY, true, true, HPos.CENTER, VPos.CENTER)
- }
-}
-
-
-class HTML5_Panel extends javafx.embed.swing.JFXPanel
-{
- private val future =
- JFX_Thread.future {
- val pane = new Web_View_Workaround
-
- val web_view = pane.web_view
- web_view.setFontSmoothingType(FontSmoothingType.GRAY)
- web_view.setOnKeyTyped(new EventHandler[KeyEvent] {
- def handle(e: KeyEvent) {
- if (e.isControlDown && e.getCharacter == "0")
- web_view.setFontScale(1.0)
- if (e.isControlDown && e.getCharacter == "+")
- web_view.setFontScale(web_view.getFontScale * 1.1)
- else if (e.isControlDown && e.getCharacter == "-")
- web_view.setFontScale(web_view.getFontScale / 1.1)
- }
- })
-
- setScene(new Scene(pane))
- pane
- }
-
- def web_view: WebView = future.join.web_view
- def web_engine: WebEngine = web_view.getEngine
-}
--- a/src/Pure/System/jfx_thread.scala Sat Sep 21 22:48:52 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-/* Title: Pure/System/jfx_thread.scala
- Module: PIDE
- Author: Makarius
-
-Evaluation within the Java FX application thread.
-*/
-
-package isabelle
-
-import javafx.application.{Platform => JFX_Platform}
-
-
-object JFX_Thread
-{
- /* checks */
-
- def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
- def require() = Predef.require(JFX_Platform.isFxApplicationThread())
-
-
- /* asynchronous context switch */
-
- def later(body: => Unit)
- {
- if (JFX_Platform.isFxApplicationThread()) body
- else JFX_Platform.runLater(new Runnable { def run = body })
- }
-
- def future[A](body: => A): Future[A] =
- {
- if (JFX_Platform.isFxApplicationThread()) Future.value(body)
- else {
- val promise = Future.promise[A]
- later { promise.fulfill_result(Exn.capture(body)) }
- promise
- }
- }
-}
--- a/src/Pure/System/swing_thread.scala Sat Sep 21 22:48:52 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-/* Title: Pure/System/swing_thread.scala
- Module: PIDE
- Author: Makarius
- Author: Fabian Immler, TU Munich
-
-Evaluation within the AWT/Swing thread.
-*/
-
-package isabelle
-
-import javax.swing.{SwingUtilities, Timer}
-import java.awt.event.{ActionListener, ActionEvent}
-
-
-object Swing_Thread
-{
- /* checks */
-
- def assert[A](body: => A) =
- {
- Predef.assert(SwingUtilities.isEventDispatchThread())
- body
- }
-
- def require[A](body: => A) =
- {
- Predef.require(SwingUtilities.isEventDispatchThread())
- body
- }
-
-
- /* main dispatch queue */
-
- def now[A](body: => A): A =
- {
- if (SwingUtilities.isEventDispatchThread()) body
- else {
- lazy val result = { assert(); Exn.capture(body) }
- SwingUtilities.invokeAndWait(new Runnable { def run = result })
- Exn.release(result)
- }
- }
-
- def future[A](body: => A): Future[A] =
- {
- if (SwingUtilities.isEventDispatchThread()) Future.value(body)
- else Future.fork { now(body) }
- }
-
- def later(body: => Unit)
- {
- if (SwingUtilities.isEventDispatchThread()) body
- else SwingUtilities.invokeLater(new Runnable { def run = body })
- }
-
-
- /* delayed actions */
-
- abstract class Delay extends
- {
- def invoke(): Unit
- def revoke(): Unit
- def postpone(time: Time): Unit
- }
-
- private def delayed_action(first: Boolean)(time: => Time)(action: => Unit): Delay =
- new Delay {
- private val timer = new Timer(time.ms.toInt, null)
- timer.setRepeats(false)
- timer.addActionListener(new ActionListener {
- override def actionPerformed(e: ActionEvent) {
- assert()
- timer.setInitialDelay(time.ms.toInt)
- action
- }
- })
-
- def invoke()
- {
- require()
- if (first) timer.start() else timer.restart()
- }
-
- def revoke()
- {
- require()
- timer.stop()
- timer.setInitialDelay(time.ms.toInt)
- }
-
- def postpone(alt_time: Time)
- {
- require()
- if (timer.isRunning) {
- timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
- timer.restart()
- }
- }
- }
-
- // delayed action after first invocation
- def delay_first = delayed_action(true) _
-
- // delayed action after last invocation
- def delay_last = delayed_action(false) _
-}
--- a/src/Pure/System/system_dialog.scala Sat Sep 21 22:48:52 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,212 +0,0 @@
-/* Title: Pure/Tools/system_dialog.scala
- Author: Makarius
-
-Dialog for system processes, with optional output window.
-*/
-
-package isabelle
-
-
-import java.awt.{GraphicsEnvironment, Point, Font}
-import javax.swing.WindowConstants
-import java.io.{File => JFile, BufferedReader, InputStreamReader}
-
-import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
- BorderPanel, Frame, TextArea, Component, Label}
-import scala.swing.event.ButtonClicked
-
-
-class System_Dialog extends Build.Progress
-{
- /* GUI state -- owned by Swing thread */
-
- private var _title = "Isabelle"
- private var _window: Option[Window] = None
- private var _return_code: Option[Int] = None
-
- private def check_window(): Window =
- {
- Swing_Thread.require()
-
- _window match {
- case Some(window) => window
- case None =>
- val window = new Window
- _window = Some(window)
-
- window.pack()
- val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
- window.location =
- new Point(point.x - window.size.width / 2, point.y - window.size.height / 2)
- window.visible = true
-
- window
- }
- }
-
- private val result = Future.promise[Int]
-
- private def conclude()
- {
- Swing_Thread.require()
- require(_return_code.isDefined)
-
- _window match {
- case None =>
- case Some(window) =>
- window.visible = false
- window.dispose
- _window = None
- }
-
- try { result.fulfill(_return_code.get) }
- catch { case ERROR(_) => }
- }
-
- def join(): Int = result.join
- def join_exit(): Nothing = sys.exit(join)
-
-
- /* window */
-
- private class Window extends Frame
- {
- title = _title
- iconImage = GUI.isabelle_image()
-
-
- /* text */
-
- val text = new TextArea {
- font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
- editable = false
- columns = 50
- rows = 20
- }
-
- val scroll_text = new ScrollPane(text)
-
-
- /* layout panel with dynamic actions */
-
- val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
- val layout_panel = new BorderPanel
- layout_panel.layout(scroll_text) = BorderPanel.Position.Center
- layout_panel.layout(action_panel) = BorderPanel.Position.South
-
- contents = layout_panel
-
- def set_actions(cs: Component*)
- {
- action_panel.contents.clear
- action_panel.contents ++= cs
- layout_panel.revalidate
- layout_panel.repaint
- }
-
-
- /* close */
-
- peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
-
- override def closeOperation {
- if (_return_code.isDefined) conclude()
- else stopping()
- }
-
- def stopping()
- {
- is_stopped = true
- set_actions(new Label("Stopping ..."))
- }
-
- val stop_button = new Button("Stop") {
- reactions += { case ButtonClicked(_) => stopping() }
- }
-
- var do_auto_close = true
- def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
-
- val auto_close = new CheckBox("Auto close") {
- reactions += {
- case ButtonClicked(_) => do_auto_close = this.selected
- if (can_auto_close) conclude()
- }
- }
- auto_close.selected = do_auto_close
- auto_close.tooltip = "Automatically close dialog when finished"
-
- set_actions(stop_button, auto_close)
-
-
- /* exit */
-
- val delay_exit =
- Swing_Thread.delay_first(Time.seconds(1.0))
- {
- if (can_auto_close) conclude()
- else {
- val button =
- new Button(if (_return_code == Some(0)) "OK" else "Exit") {
- reactions += { case ButtonClicked(_) => conclude() }
- }
- set_actions(button)
- button.peer.getRootPane.setDefaultButton(button.peer)
- }
- }
- }
-
-
- /* progress operations */
-
- def title(txt: String): Unit =
- Swing_Thread.later {
- _title = txt
- _window.foreach(window => window.title = txt)
- }
-
- def return_code(rc: Int): Unit =
- Swing_Thread.later {
- _return_code = Some(rc)
- _window match {
- case None => conclude()
- case Some(window) => window.delay_exit.invoke
- }
- }
-
- override def echo(txt: String): Unit =
- Swing_Thread.later {
- val window = check_window()
- window.text.append(txt + "\n")
- val vertical = window.scroll_text.peer.getVerticalScrollBar
- vertical.setValue(vertical.getMaximum)
- }
-
- override def theory(session: String, theory: String): Unit =
- echo(session + ": theory " + theory)
-
- @volatile private var is_stopped = false
- override def stopped: Boolean = is_stopped
-
-
- /* system operations */
-
- def execute(cwd: JFile, env: Map[String, String], args: String*): Int =
- {
- val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
- proc.getOutputStream.close
-
- val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
- try {
- var line = stdout.readLine
- while (line != null) {
- echo(line)
- line = stdout.readLine
- }
- }
- finally { stdout.close }
-
- proc.waitFor
- }
-}
-
--- a/src/Pure/System/wrap_panel.scala Sat Sep 21 22:48:52 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,123 +0,0 @@
-/* Title: Pure/System/wrap_panel.scala
- Author: Makarius
-
-Panel with improved FlowLayout for wrapping of components over
-multiple lines, see also
-http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
-scala.swing.FlowPanel.
-*/
-
-package isabelle
-
-
-import java.awt.{FlowLayout, Container, Dimension}
-import javax.swing.{JComponent, JPanel, JScrollPane}
-
-import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane}
-
-
-object Wrap_Panel
-{
- val Alignment = FlowPanel.Alignment
-
- class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
- extends FlowLayout(align: Int, hgap: Int, vgap: Int)
- {
- override def preferredLayoutSize(target: Container): Dimension =
- layout_size(target, true)
-
- override def minimumLayoutSize(target: Container): Dimension =
- {
- val minimum = layout_size(target, false)
- minimum.width -= (getHgap + 1)
- minimum
- }
-
- private def layout_size(target: Container, preferred: Boolean): Dimension =
- {
- target.getTreeLock.synchronized
- {
- val target_width =
- if (target.getSize.width == 0) Integer.MAX_VALUE
- else target.getSize.width
-
- val hgap = getHgap
- val vgap = getVgap
- val insets = target.getInsets
- val horizontal_insets_and_gap = insets.left + insets.right + (hgap * 2)
- val max_width = target_width - horizontal_insets_and_gap
-
-
- /* fit components into rows */
-
- val dim = new Dimension(0, 0)
- var row_width = 0
- var row_height = 0
- def add_row()
- {
- dim.width = dim.width max row_width
- if (dim.height > 0) dim.height += vgap
- dim.height += row_height
- }
-
- for {
- i <- 0 until target.getComponentCount
- m = target.getComponent(i)
- if m.isVisible
- d = if (preferred) m.getPreferredSize else m.getMinimumSize()
- }
- {
- if (row_width + d.width > max_width) {
- add_row()
- row_width = 0
- row_height = 0
- }
-
- if (row_width != 0) row_width += hgap
-
- row_width += d.width
- row_height = row_height max d.height
- }
- add_row()
-
- dim.width += horizontal_insets_and_gap
- dim.height += insets.top + insets.bottom + vgap * 2
-
-
- /* special treatment for ScrollPane */
-
- val scroll_pane =
- GUI.ancestors(target).exists(
- {
- case _: JScrollPane => true
- case c: JComponent if Component.wrap(c).isInstanceOf[ScrollPane] => true
- case _ => false
- })
- if (scroll_pane && target.isValid)
- dim.width -= (hgap + 1)
-
- dim
- }
- }
- }
-}
-
-
-class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*)
- extends Panel with SequentialContainer.Wrapper
-{
- override lazy val peer: JPanel =
- new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
-
- def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*)
- def this() = this(Wrap_Panel.Alignment.Center)()
-
- contents ++= contents0
-
- private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
-
- def vGap: Int = layoutManager.getVgap
- def vGap_=(n: Int) { layoutManager.setVgap(n) }
- def hGap: Int = layoutManager.getHgap
- def hGap_=(n: Int) { layoutManager.setHgap(n) }
-}
--- a/src/Pure/build-jars Sat Sep 21 22:48:52 2013 +0200
+++ b/src/Pure/build-jars Sun Sep 22 14:30:34 2013 +0200
@@ -29,6 +29,15 @@
General/time.scala
General/timing.scala
General/xz_file.scala
+ GUI/color_value.scala
+ GUI/gui.scala
+ GUI/gui_setup.scala
+ GUI/html5_panel.scala
+ GUI/jfx_thread.scala
+ GUI/popup.scala
+ GUI/swing_thread.scala
+ GUI/system_dialog.scala
+ GUI/wrap_panel.scala
Isar/completion.scala
Isar/keyword.scala
Isar/outer_syntax.scala
@@ -45,27 +54,19 @@
PIDE/text.scala
PIDE/xml.scala
PIDE/yxml.scala
- System/color_value.scala
System/command_line.scala
System/event_bus.scala
- System/gui.scala
- System/gui_setup.scala
- System/html5_panel.scala
System/interrupt.scala
System/invoke_scala.scala
System/isabelle_charset.scala
System/isabelle_font.scala
System/isabelle_process.scala
System/isabelle_system.scala
- System/jfx_thread.scala
System/options.scala
System/platform.scala
System/session.scala
- System/swing_thread.scala
System/system_channel.scala
- System/system_dialog.scala
System/utf8.scala
- System/wrap_panel.scala
Thy/html.scala
Thy/present.scala
Thy/thy_header.scala
--- a/src/Tools/jEdit/lib/Tools/jedit Sat Sep 21 22:48:52 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sun Sep 22 14:30:34 2013 +0200
@@ -31,7 +31,6 @@
"src/osx_adapter.scala"
"src/output_dockable.scala"
"src/plugin.scala"
- "src/popup.scala"
"src/pretty_text_area.scala"
"src/pretty_tooltip.scala"
"src/process_indicator.scala"
--- a/src/Tools/jEdit/src/popup.scala Sat Sep 21 22:48:52 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-/* Title: Tools/jEdit/src/popup.scala
- Author: Makarius
-
-Popup within layered pane.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.awt.{Point, Dimension}
-import javax.swing.{JLayeredPane, JComponent}
-
-
-class Popup(
- layered: JLayeredPane,
- component: JComponent,
- location: Point,
- size: Dimension)
-{
- def show
- {
- component.setLocation(location)
- component.setSize(size)
- component.setPreferredSize(size)
- component.setOpaque(true)
- layered.add(component, JLayeredPane.POPUP_LAYER)
- layered.moveToFront(component)
- layered.repaint(component.getBounds())
- }
-
- def hide
- {
- val bounds = component.getBounds()
- layered.remove(component)
- layered.repaint(bounds)
- }
-}
-