some support for actual HTML rendering;
authorwenzelm
Wed Sep 12 16:27:44 2012 +0200 (2012-09-12)
changeset 493338b144338e1a2
parent 49332 77c7ce7609cd
child 49334 dbc169ddd404
some support for actual HTML rendering;
src/Pure/System/html5_panel.scala
     1.1 --- a/src/Pure/System/html5_panel.scala	Wed Sep 12 15:01:25 2012 +0200
     1.2 +++ b/src/Pure/System/html5_panel.scala	Wed Sep 12 16:27:44 2012 +0200
     1.3 @@ -6,11 +6,12 @@
     1.4  
     1.5  package isabelle
     1.6  
     1.7 +import com.sun.javafx.tk.{FontMetrics, Toolkit}
     1.8  
     1.9  import javafx.scene.Scene
    1.10  import javafx.scene.web.{WebView, WebEngine}
    1.11  import javafx.scene.input.KeyEvent
    1.12 -import javafx.scene.text.FontSmoothingType
    1.13 +import javafx.scene.text.{Font, FontSmoothingType}
    1.14  import javafx.scene.layout.{HBox, VBox, Priority}
    1.15  import javafx.geometry.{HPos, VPos, Insets}
    1.16  import javafx.event.EventHandler
    1.17 @@ -50,8 +51,30 @@
    1.18  }
    1.19  
    1.20  
    1.21 -class HTML5_Panel extends javafx.embed.swing.JFXPanel
    1.22 +class HTML5_Panel(main_css: String, init_font_family: String, init_font_size: Int)
    1.23 +  extends javafx.embed.swing.JFXPanel
    1.24  {
    1.25 +  /* HTML/CSS template */
    1.26 +
    1.27 +  def template(font_family: String, font_size: Int): String =
    1.28 +"""<?xml version="1.0" encoding="utf-8"?>
    1.29 +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
    1.30 +  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
    1.31 +<html xmlns="http://www.w3.org/1999/xhtml">
    1.32 +<head>
    1.33 +<style media="all" type="text/css">
    1.34 +""" + main_css +
    1.35 +"body { font-family: " + font_family + "; font-size: " + font_size + "px; }" +
    1.36 +"""
    1.37 +</style>
    1.38 +</head>
    1.39 +<body/>
    1.40 +</html>
    1.41 +"""
    1.42 +
    1.43 +
    1.44 +  /* main Web view */
    1.45 +
    1.46    private val future =
    1.47      JFX_Thread.future {
    1.48        val pane = new Web_View_Workaround
    1.49 @@ -70,9 +93,68 @@
    1.50        })
    1.51  
    1.52        setScene(new Scene(pane))
    1.53 +
    1.54 +      web_view.getEngine.loadContent(template(init_font_family, init_font_size))
    1.55        pane
    1.56      }
    1.57  
    1.58    def web_view: WebView = future.join.web_view
    1.59    def web_engine: WebEngine = web_view.getEngine
    1.60 +
    1.61 +
    1.62 +  /* internal state -- owned by JFX thread */
    1.63 +
    1.64 +  private var current_font_metrics: FontMetrics = null
    1.65 +  private var current_font_family = ""
    1.66 +  private var current_font_size: Int = 0
    1.67 +  private var current_margin: Int = 0
    1.68 +  private var current_body: XML.Body = Nil
    1.69 +
    1.70 +  // FIXME move to pretty.scala (!?)
    1.71 +  private def pretty_metric(metrics: FontMetrics): String => Double =
    1.72 +  {
    1.73 +    if (metrics == null) ((s: String) => s.length.toDouble)
    1.74 +    else {
    1.75 +      val unit = metrics.computeStringWidth(Pretty.space).toDouble
    1.76 +      ((s: String) => if (s == "\n") 1.0 else metrics.computeStringWidth(s) / unit)
    1.77 +    }
    1.78 +  }
    1.79 +
    1.80 +  def resize(font_family: String, font_size: Int): Unit = JFX_Thread.later {
    1.81 +    val font = new Font(font_family, font_size)
    1.82 +    val font_metrics = Toolkit.getToolkit().getFontLoader().getFontMetrics(font)
    1.83 +    val margin =  // FIXME Swing thread!?
    1.84 +      (getWidth() / (font_metrics.computeStringWidth(Pretty.space) max 1.0f)).toInt max 20
    1.85 +
    1.86 +    if (current_font_metrics == null ||
    1.87 +        current_font_family != font_family ||
    1.88 +        current_font_size != font_size ||
    1.89 +        current_margin != margin)
    1.90 +    {
    1.91 +      current_font_metrics = font_metrics
    1.92 +      current_font_family = font_family
    1.93 +      current_font_size = font_size
    1.94 +      current_margin = margin
    1.95 +      refresh()
    1.96 +    }
    1.97 +  }
    1.98 +
    1.99 +  def refresh(): Unit = JFX_Thread.later { render(current_body) }
   1.100 +
   1.101 +  def render(body: XML.Body): Unit = JFX_Thread.later {
   1.102 +    current_body = body
   1.103 +    val html_body =
   1.104 +      current_body.flatMap(div =>
   1.105 +        Pretty.formatted(List(div), current_margin, pretty_metric(current_font_metrics))
   1.106 +          .map(t =>
   1.107 +            XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Isabelle_Markup.MESSAGE))),
   1.108 +              HTML.spans(t, false))))  // FIXME user data (!??!)
   1.109 +
   1.110 +    // FIXME  web_engine.loadContent(template(current_font_family, current_font_size))
   1.111 +
   1.112 +    val document = web_engine.getDocument
   1.113 +    val html_root = document.getLastChild
   1.114 +    html_root.removeChild(html_root.getLastChild)
   1.115 +    html_root.appendChild(XML.document_node(document, XML.elem(HTML.BODY, html_body)))
   1.116 +  }
   1.117  }