# HG changeset patch
# User wenzelm
# Date 1346612471 -7200
# Node ID 1067a639d42ad441deb8536a96a2a8182dce22a0
# Parent  8ead9e8b15fbf447f2b1d9f0d2a6d7fbe28d2f3d
basic setup for HTML5 panel;
more JFX_Thread.operations;

diff -r 8ead9e8b15fb -r 1067a639d42a src/Pure/System/html5_panel.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/html5_panel.scala	Sun Sep 02 21:01:11 2012 +0200
@@ -0,0 +1,78 @@
+/*  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 8ead9e8b15fb -r 1067a639d42a src/Pure/System/jfx_thread.scala
--- a/src/Pure/System/jfx_thread.scala	Sun Sep 02 19:26:05 2012 +0200
+++ b/src/Pure/System/jfx_thread.scala	Sun Sep 02 21:01:11 2012 +0200
@@ -25,4 +25,14 @@
     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 8ead9e8b15fb -r 1067a639d42a src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Sep 02 19:26:05 2012 +0200
+++ b/src/Pure/build-jars	Sun Sep 02 21:01:11 2012 +0200
@@ -44,6 +44,7 @@
   System/command_line.scala
   System/event_bus.scala
   System/gui_setup.scala
+  System/html5_panel.scala
   System/invoke_scala.scala
   System/isabelle_charset.scala
   System/isabelle_process.scala