# HG changeset patch
# User wenzelm
# Date 1348753108 -7200
# Node ID e6a53d203362d945c1aeb80fcd9660e5d22149e6
# Parent 8e3c10eb63750758a363670650d90275cb4de669
eliminated obsolete HTML/CSS functionality;
diff -r 8e3c10eb6375 -r e6a53d203362 src/Pure/System/html5_panel.scala
--- 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 =
-"""
-
-
-
-
-
-
-
-"""
-
-
- /* 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)))
- }
}
diff -r 8e3c10eb6375 -r e6a53d203362 src/Tools/jEdit/etc/isabelle-jedit.css
--- 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; }
diff -r 8e3c10eb6375 -r e6a53d203362 src/Tools/jEdit/etc/settings
--- 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"
diff -r 8e3c10eb6375 -r e6a53d203362 src/Tools/jEdit/src/html_panel.scala
--- 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 =
- """
-
-
-