# 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 = +""" + + +
+ + +