--- a/src/Pure/System/html5_panel.scala Wed Sep 12 15:01:25 2012 +0200
+++ b/src/Pure/System/html5_panel.scala Wed Sep 12 16:27:44 2012 +0200
@@ -6,11 +6,12 @@
package isabelle
+import com.sun.javafx.tk.{FontMetrics, Toolkit}
import javafx.scene.Scene
import javafx.scene.web.{WebView, WebEngine}
import javafx.scene.input.KeyEvent
-import javafx.scene.text.FontSmoothingType
+import javafx.scene.text.{Font, FontSmoothingType}
import javafx.scene.layout.{HBox, VBox, Priority}
import javafx.geometry.{HPos, VPos, Insets}
import javafx.event.EventHandler
@@ -50,8 +51,30 @@
}
-class HTML5_Panel extends javafx.embed.swing.JFXPanel
+class HTML5_Panel(main_css: String, init_font_family: String, init_font_size: Int)
+ extends javafx.embed.swing.JFXPanel
{
+ /* HTML/CSS template */
+
+ def template(font_family: String, font_size: Int): String =
+"""<?xml version="1.0" encoding="utf-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<style media="all" type="text/css">
+""" + main_css +
+"body { font-family: " + font_family + "; font-size: " + font_size + "px; }" +
+"""
+</style>
+</head>
+<body/>
+</html>
+"""
+
+
+ /* main Web view */
+
private val future =
JFX_Thread.future {
val pane = new Web_View_Workaround
@@ -70,9 +93,68 @@
})
setScene(new Scene(pane))
+
+ web_view.getEngine.loadContent(template(init_font_family, init_font_size))
pane
}
def web_view: WebView = future.join.web_view
def web_engine: WebEngine = web_view.getEngine
+
+
+ /* internal state -- owned by JFX thread */
+
+ private var current_font_metrics: FontMetrics = null
+ private var current_font_family = ""
+ private var current_font_size: Int = 0
+ private var current_margin: Int = 0
+ private var current_body: XML.Body = Nil
+
+ // FIXME move to pretty.scala (!?)
+ private def pretty_metric(metrics: FontMetrics): String => Double =
+ {
+ if (metrics == null) ((s: String) => s.length.toDouble)
+ else {
+ val unit = metrics.computeStringWidth(Pretty.space).toDouble
+ ((s: String) => if (s == "\n") 1.0 else metrics.computeStringWidth(s) / unit)
+ }
+ }
+
+ def resize(font_family: String, font_size: Int): Unit = JFX_Thread.later {
+ val font = new Font(font_family, font_size)
+ val font_metrics = Toolkit.getToolkit().getFontLoader().getFontMetrics(font)
+ val margin = // FIXME Swing thread!?
+ (getWidth() / (font_metrics.computeStringWidth(Pretty.space) max 1.0f)).toInt max 20
+
+ if (current_font_metrics == null ||
+ current_font_family != font_family ||
+ current_font_size != font_size ||
+ current_margin != margin)
+ {
+ current_font_metrics = font_metrics
+ current_font_family = font_family
+ current_font_size = font_size
+ current_margin = margin
+ refresh()
+ }
+ }
+
+ def refresh(): Unit = JFX_Thread.later { render(current_body) }
+
+ def render(body: XML.Body): Unit = JFX_Thread.later {
+ current_body = body
+ val html_body =
+ current_body.flatMap(div =>
+ Pretty.formatted(List(div), current_margin, pretty_metric(current_font_metrics))
+ .map(t =>
+ XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Isabelle_Markup.MESSAGE))),
+ HTML.spans(t, false)))) // FIXME user data (!??!)
+
+ // FIXME web_engine.loadContent(template(current_font_family, current_font_size))
+
+ val document = web_engine.getDocument
+ val html_root = document.getLastChild
+ html_root.removeChild(html_root.getLastChild)
+ html_root.appendChild(XML.document_node(document, XML.elem(HTML.BODY, html_body)))
+ }
}