--- a/src/Pure/System/html5_panel.scala Thu Sep 27 15:09:32 2012 +0200
+++ b/src/Pure/System/html5_panel.scala Thu Sep 27 15:38:28 2012 +0200
@@ -6,12 +6,11 @@
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.{Font, FontSmoothingType}
+import javafx.scene.text.FontSmoothingType
import javafx.scene.layout.{HBox, VBox, Priority}
import javafx.geometry.{HPos, VPos, Insets}
import javafx.event.EventHandler
@@ -51,30 +50,8 @@
}
-class HTML5_Panel(main_css: String, init_font_family: String, init_font_size: Int)
- extends javafx.embed.swing.JFXPanel
+class HTML5_Panel 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
@@ -93,68 +70,9 @@
})
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)))
- }
}
--- a/src/Tools/jEdit/etc/isabelle-jedit.css Thu Sep 27 15:09:32 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-/* additional style file for Isabelle/jEdit output */
-
-.message { margin-top: 0.3ex; background-color: #F0F0F0; }
-
-.writeln_message { }
-.tracing_message { background-color: #F0F8FF; }
-.warning_message { background-color: #EEE8AA; }
-.error_message { background-color: #FFC1C1; }
-
-.intensify { background-color: #FFCC66; }
-
-.keyword { font-weight: bold; color: #009966; }
-.operator { font-weight: bold; }
-.command { font-weight: bold; color: #006699; }
-
-.sendback { background-color: #DCDCDC; }
-.sendback:hover { background-color: #9DC75D; }
--- a/src/Tools/jEdit/etc/settings Thu Sep 27 15:09:32 2012 +0200
+++ b/src/Tools/jEdit/etc/settings Thu Sep 27 15:38:28 2012 +0200
@@ -10,8 +10,6 @@
-Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit
-Dscala.repl.no-threads=true"
-JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
-
ISABELLE_JEDIT_OPTIONS=""
ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
--- a/src/Tools/jEdit/src/html_panel.scala Thu Sep 27 15:09:32 2012 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala Thu Sep 27 15:38:28 2012 +0200
@@ -9,195 +9,28 @@
import isabelle._
-import java.lang.System
import java.io.StringReader
-import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
-import java.awt.event.MouseEvent
import java.util.logging.{Logger, Level}
-import org.w3c.dom.html2.HTMLElement
-
import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
import org.lobobrowser.html.gui.HtmlPanel
-import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
-import scala.actors.Actor._
-
-
-object HTML_Panel
-{
- sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
- case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
-}
-
-class HTML_Panel(initial_font_family: String, initial_font_size: Int) extends HtmlPanel
+class HTML_Panel extends HtmlPanel
{
- /** Lobo setup **/
-
- /* global logging */
+ Swing_Thread.require()
Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
-
- /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
-
- val screen_resolution =
- if (GraphicsEnvironment.isHeadless()) 72
- else Toolkit.getDefaultToolkit().getScreenResolution()
-
- def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
- def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
-
-
- /* contexts and event handling */
-
- protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Map.empty
-
private val ucontext = new SimpleUserAgentContext
private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
- {
- private def handle(event: HTML_Panel.Event): Boolean =
- if (handler.isDefinedAt(event)) { handler(event); false }
- else true
-
- override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
- handle(HTML_Panel.Context_Menu(elem, event))
- override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
- handle(HTML_Panel.Mouse_Click(elem, event))
- override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
- handle(HTML_Panel.Double_Click(elem, event))
- override def onMouseOver(elem: HTMLElement, event: MouseEvent)
- { handle(HTML_Panel.Mouse_Over(elem, event)) }
- override def onMouseOut(elem: HTMLElement, event: MouseEvent)
- { handle(HTML_Panel.Mouse_Out(elem, event)) }
- }
-
private val builder = new DocumentBuilderImpl(ucontext, rcontext)
-
- /* document template with style sheets */
-
- private val template_head =
- """<?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">
-""" +
- File.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
-
- private val template_tail =
-"""
-</style>
-</head>
-<body/>
-</html>
-"""
-
- private def template(font_family: String, font_size: Int): String =
- template_head +
- "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" +
- template_tail
-
-
- /** main actor **/
-
- /* internal messages */
-
- private case class Resize(font_family: String, font_size: Int)
- private case class Render_Document(url: String, text: String)
- private case class Render(body: XML.Body)
- private case class Render_Sync(body: XML.Body)
- private case object Refresh
-
- private val main_actor = actor {
-
- /* internal state */
-
- var current_font_metrics: FontMetrics = null
- var current_font_family = ""
- var current_font_size: Int = 0
- var current_margin: Int = 0
- var current_body: XML.Body = Nil
-
- def resize(font_family: String, font_size: Int)
- {
- val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size)))
- val (font_metrics, margin) =
- Swing_Thread.now {
- val metrics = getFontMetrics(font)
- (metrics, (getWidth() / (metrics.charWidth(Pretty.spc) max 1) - 4) 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() { render(current_body) }
-
- def render_document(url: String, text: String)
- {
- val doc = builder.parse(new InputSourceImpl(new StringReader(text), url))
- Swing_Thread.later { setDocument(doc, rcontext) }
- }
-
- def render(body: XML.Body)
- {
- current_body = body
- val html_body =
- current_body.flatMap(div =>
- Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
- .map(t =>
- XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Isabelle_Markup.MESSAGE))),
- HTML.spans(t, true))))
- val doc =
- builder.parse(
- new InputSourceImpl(
- new StringReader(template(current_font_family, current_font_size)), "http://localhost"))
- doc.removeChild(doc.getLastChild())
- doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
- Swing_Thread.later { setDocument(doc, rcontext) }
- }
-
-
- /* main loop */
-
- resize(initial_font_family, initial_font_size)
-
- loop {
- react {
- case Resize(font_family, font_size) => resize(font_family, font_size)
- case Refresh => refresh()
- case Render_Document(url, text) => render_document(url, text)
- case Render(body) => render(body)
- case Render_Sync(body) => render(body); reply(())
- case bad => System.err.println("main_actor: ignoring bad message " + bad)
- }
- }
+ def render_document(url: String, html_text: String)
+ {
+ val doc = builder.parse(new InputSourceImpl(new StringReader(html_text), url))
+ Swing_Thread.later { setDocument(doc, rcontext) }
}
-
-
- /* external methods */
-
- def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
- def refresh() { main_actor ! Refresh }
- def render_document(url: String, text: String) { main_actor ! Render_Document(url, text) }
- def render(body: XML.Body) { main_actor ! Render(body) }
- def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
}
--- a/src/Tools/jEdit/src/readme_dockable.scala Thu Sep 27 15:09:32 2012 +0200
+++ b/src/Tools/jEdit/src/readme_dockable.scala Thu Sep 27 15:38:28 2012 +0200
@@ -14,10 +14,11 @@
class README_Dockable(view: View, position: String) extends Dockable(view, position)
{
- private val readme = new HTML_Panel("SansSerif", 14)
+ Swing_Thread.require()
+
+ private val readme = new HTML_Panel
private val readme_path = Path.explode("$JEDIT_HOME/README.html")
- readme.render_document(
- Isabelle_System.platform_file_url(readme_path), File.try_read(List(readme_path)))
+ readme.render_document(Isabelle_System.platform_file_url(readme_path), File.read(readme_path))
set_content(readme)
}