# HG changeset patch # User wenzelm # Date 1347460064 -7200 # Node ID 8b144338e1a2bd34ef93961c2e14a90bb6000e5b # Parent 77c7ce7609cd866f48423c730ce6ce50f470320f some support for actual HTML rendering; diff -r 77c7ce7609cd -r 8b144338e1a2 src/Pure/System/html5_panel.scala --- 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 = +""" + + + + + + + +""" + + + /* 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))) + } }