# HG changeset patch # User wenzelm # Date 1379853034 -7200 # Node ID f5e9d182f64505d874c1d0129b488ad7295f8ffd # Parent 3746a78a2c01d21a53b11b7c39f7e96759059bc6 clarified location of GUI modules (which depend on Swing of JFX); diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/GUI/color_value.scala --- /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 + } + } +} + diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/GUI/gui.scala --- /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 + } +} + diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/GUI/gui_setup.scala --- /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) + } + } +} + diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/GUI/html5_panel.scala --- /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 +} diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/GUI/jfx_thread.scala --- /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 + } + } +} diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/GUI/popup.scala --- /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) + } +} + diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/GUI/swing_thread.scala --- /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) _ +} diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/GUI/system_dialog.scala --- /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 + } +} + diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/GUI/wrap_panel.scala --- /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) } +} diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/System/color_value.scala --- 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 - } - } -} - diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/System/gui.scala --- 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 - } -} - diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/System/gui_setup.scala --- 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) - } - } -} - diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/System/html5_panel.scala --- 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 -} diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/System/jfx_thread.scala --- 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 - } - } -} diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/System/swing_thread.scala --- 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) _ -} diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/System/system_dialog.scala --- 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 - } -} - diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/System/wrap_panel.scala --- 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) } -} diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/build-jars --- 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 diff -r 3746a78a2c01 -r f5e9d182f645 src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 3746a78a2c01 -r f5e9d182f645 src/Tools/jEdit/src/popup.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) - } -} -