eliminated obsolete HTML/CSS functionality;
authorwenzelm
Thu Sep 27 15:38:28 2012 +0200 (2012-09-27 ago)
changeset 49612e6a53d203362
parent 49611 8e3c10eb6375
child 49613 2f6986e2ef06
eliminated obsolete HTML/CSS functionality;
src/Pure/System/html5_panel.scala
src/Tools/jEdit/etc/isabelle-jedit.css
src/Tools/jEdit/etc/settings
src/Tools/jEdit/src/html_panel.scala
src/Tools/jEdit/src/readme_dockable.scala
     1.1 --- a/src/Pure/System/html5_panel.scala	Thu Sep 27 15:09:32 2012 +0200
     1.2 +++ b/src/Pure/System/html5_panel.scala	Thu Sep 27 15:38:28 2012 +0200
     1.3 @@ -6,12 +6,11 @@
     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.{Font, FontSmoothingType}
    1.13 +import javafx.scene.text.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 @@ -51,30 +50,8 @@
    1.18  }
    1.19  
    1.20  
    1.21 -class HTML5_Panel(main_css: String, init_font_family: String, init_font_size: Int)
    1.22 -  extends javafx.embed.swing.JFXPanel
    1.23 +class HTML5_Panel 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 @@ -93,68 +70,9 @@
    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  }
     2.1 --- a/src/Tools/jEdit/etc/isabelle-jedit.css	Thu Sep 27 15:09:32 2012 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,17 +0,0 @@
     2.4 -/* additional style file for Isabelle/jEdit output */
     2.5 -
     2.6 -.message { margin-top: 0.3ex; background-color: #F0F0F0; }
     2.7 -
     2.8 -.writeln_message { }
     2.9 -.tracing_message { background-color: #F0F8FF; }
    2.10 -.warning_message { background-color: #EEE8AA; }
    2.11 -.error_message { background-color: #FFC1C1; }
    2.12 -
    2.13 -.intensify { background-color: #FFCC66; }
    2.14 -
    2.15 -.keyword { font-weight: bold; color: #009966; }
    2.16 -.operator { font-weight: bold; }
    2.17 -.command { font-weight: bold; color: #006699; }
    2.18 -
    2.19 -.sendback { background-color: #DCDCDC; }
    2.20 -.sendback:hover { background-color: #9DC75D; }
     3.1 --- a/src/Tools/jEdit/etc/settings	Thu Sep 27 15:09:32 2012 +0200
     3.2 +++ b/src/Tools/jEdit/etc/settings	Thu Sep 27 15:38:28 2012 +0200
     3.3 @@ -10,8 +10,6 @@
     3.4  -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit
     3.5  -Dscala.repl.no-threads=true"
     3.6  
     3.7 -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"
     3.8 -
     3.9  ISABELLE_JEDIT_OPTIONS=""
    3.10  
    3.11  ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
     4.1 --- a/src/Tools/jEdit/src/html_panel.scala	Thu Sep 27 15:09:32 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Thu Sep 27 15:38:28 2012 +0200
     4.3 @@ -9,195 +9,28 @@
     4.4  
     4.5  import isabelle._
     4.6  
     4.7 -import java.lang.System
     4.8  import java.io.StringReader
     4.9 -import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
    4.10 -import java.awt.event.MouseEvent
    4.11  
    4.12  import java.util.logging.{Logger, Level}
    4.13  
    4.14 -import org.w3c.dom.html2.HTMLElement
    4.15 -
    4.16  import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
    4.17  import org.lobobrowser.html.gui.HtmlPanel
    4.18 -import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
    4.19  import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
    4.20  
    4.21 -import scala.actors.Actor._
    4.22 -
    4.23 -
    4.24 -object HTML_Panel
    4.25 -{
    4.26 -  sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
    4.27 -  case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
    4.28 -  case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
    4.29 -  case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
    4.30 -  case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
    4.31 -  case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
    4.32 -}
    4.33 -
    4.34  
    4.35 -class HTML_Panel(initial_font_family: String, initial_font_size: Int) extends HtmlPanel
    4.36 +class HTML_Panel extends HtmlPanel
    4.37  {
    4.38 -  /** Lobo setup **/
    4.39 -
    4.40 -  /* global logging */
    4.41 +  Swing_Thread.require()
    4.42  
    4.43    Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
    4.44  
    4.45 -
    4.46 -  /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
    4.47 -
    4.48 -  val screen_resolution =
    4.49 -    if (GraphicsEnvironment.isHeadless()) 72
    4.50 -    else Toolkit.getDefaultToolkit().getScreenResolution()
    4.51 -
    4.52 -  def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
    4.53 -  def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
    4.54 -
    4.55 -
    4.56 -  /* contexts and event handling */
    4.57 -
    4.58 -  protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Map.empty
    4.59 -
    4.60    private val ucontext = new SimpleUserAgentContext
    4.61    private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
    4.62 -  {
    4.63 -    private def handle(event: HTML_Panel.Event): Boolean =
    4.64 -      if (handler.isDefinedAt(event)) { handler(event); false }
    4.65 -      else true
    4.66 -
    4.67 -    override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
    4.68 -      handle(HTML_Panel.Context_Menu(elem, event))
    4.69 -    override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
    4.70 -      handle(HTML_Panel.Mouse_Click(elem, event))
    4.71 -    override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
    4.72 -      handle(HTML_Panel.Double_Click(elem, event))
    4.73 -    override def onMouseOver(elem: HTMLElement, event: MouseEvent)
    4.74 -      { handle(HTML_Panel.Mouse_Over(elem, event)) }
    4.75 -    override def onMouseOut(elem: HTMLElement, event: MouseEvent)
    4.76 -      { handle(HTML_Panel.Mouse_Out(elem, event)) }
    4.77 -  }
    4.78 -
    4.79    private val builder = new DocumentBuilderImpl(ucontext, rcontext)
    4.80  
    4.81 -
    4.82 -  /* document template with style sheets */
    4.83 -
    4.84 -  private val template_head =
    4.85 -    """<?xml version="1.0" encoding="utf-8"?>
    4.86 -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
    4.87 -  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
    4.88 -<html xmlns="http://www.w3.org/1999/xhtml">
    4.89 -<head>
    4.90 -<style media="all" type="text/css">
    4.91 -""" +
    4.92 -  File.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
    4.93 -
    4.94 -  private val template_tail =
    4.95 -"""
    4.96 -</style>
    4.97 -</head>
    4.98 -<body/>
    4.99 -</html>
   4.100 -"""
   4.101 -
   4.102 -  private def template(font_family: String, font_size: Int): String =
   4.103 -    template_head +
   4.104 -    "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" +
   4.105 -    template_tail
   4.106 -
   4.107 -
   4.108 -  /** main actor **/
   4.109 -
   4.110 -  /* internal messages */
   4.111 -
   4.112 -  private case class Resize(font_family: String, font_size: Int)
   4.113 -  private case class Render_Document(url: String, text: String)
   4.114 -  private case class Render(body: XML.Body)
   4.115 -  private case class Render_Sync(body: XML.Body)
   4.116 -  private case object Refresh
   4.117 -
   4.118 -  private val main_actor = actor {
   4.119 -
   4.120 -    /* internal state */
   4.121 -
   4.122 -    var current_font_metrics: FontMetrics = null
   4.123 -    var current_font_family = ""
   4.124 -    var current_font_size: Int = 0
   4.125 -    var current_margin: Int = 0
   4.126 -    var current_body: XML.Body = Nil
   4.127 -
   4.128 -    def resize(font_family: String, font_size: Int)
   4.129 -    {
   4.130 -      val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size)))
   4.131 -      val (font_metrics, margin) =
   4.132 -        Swing_Thread.now {
   4.133 -          val metrics = getFontMetrics(font)
   4.134 -          (metrics, (getWidth() / (metrics.charWidth(Pretty.spc) max 1) - 4) max 20)
   4.135 -        }
   4.136 -      if (current_font_metrics == null ||
   4.137 -          current_font_family != font_family ||
   4.138 -          current_font_size != font_size ||
   4.139 -          current_margin != margin)
   4.140 -      {
   4.141 -        current_font_metrics = font_metrics
   4.142 -        current_font_family = font_family
   4.143 -        current_font_size = font_size
   4.144 -        current_margin = margin
   4.145 -        refresh()
   4.146 -      }
   4.147 -    }
   4.148 -
   4.149 -    def refresh() { render(current_body) }
   4.150 -
   4.151 -    def render_document(url: String, text: String)
   4.152 -    {
   4.153 -      val doc = builder.parse(new InputSourceImpl(new StringReader(text), url))
   4.154 -      Swing_Thread.later { setDocument(doc, rcontext) }
   4.155 -    }
   4.156 -
   4.157 -    def render(body: XML.Body)
   4.158 -    {
   4.159 -      current_body = body
   4.160 -      val html_body =
   4.161 -        current_body.flatMap(div =>
   4.162 -          Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
   4.163 -            .map(t =>
   4.164 -              XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Isabelle_Markup.MESSAGE))),
   4.165 -                HTML.spans(t, true))))
   4.166 -      val doc =
   4.167 -        builder.parse(
   4.168 -          new InputSourceImpl(
   4.169 -            new StringReader(template(current_font_family, current_font_size)), "http://localhost"))
   4.170 -      doc.removeChild(doc.getLastChild())
   4.171 -      doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
   4.172 -      Swing_Thread.later { setDocument(doc, rcontext) }
   4.173 -    }
   4.174 -
   4.175 -
   4.176 -    /* main loop */
   4.177 -
   4.178 -    resize(initial_font_family, initial_font_size)
   4.179 -
   4.180 -    loop {
   4.181 -      react {
   4.182 -        case Resize(font_family, font_size) => resize(font_family, font_size)
   4.183 -        case Refresh => refresh()
   4.184 -        case Render_Document(url, text) => render_document(url, text)
   4.185 -        case Render(body) => render(body)
   4.186 -        case Render_Sync(body) => render(body); reply(())
   4.187 -        case bad => System.err.println("main_actor: ignoring bad message " + bad)
   4.188 -      }
   4.189 -    }
   4.190 +  def render_document(url: String, html_text: String)
   4.191 +  {
   4.192 +    val doc = builder.parse(new InputSourceImpl(new StringReader(html_text), url))
   4.193 +    Swing_Thread.later { setDocument(doc, rcontext) }
   4.194    }
   4.195 -
   4.196 -
   4.197 -  /* external methods */
   4.198 -
   4.199 -  def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
   4.200 -  def refresh() { main_actor ! Refresh }
   4.201 -  def render_document(url: String, text: String) { main_actor ! Render_Document(url, text) }
   4.202 -  def render(body: XML.Body) { main_actor ! Render(body) }
   4.203 -  def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
   4.204  }
     5.1 --- a/src/Tools/jEdit/src/readme_dockable.scala	Thu Sep 27 15:09:32 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/readme_dockable.scala	Thu Sep 27 15:38:28 2012 +0200
     5.3 @@ -14,10 +14,11 @@
     5.4  
     5.5  class README_Dockable(view: View, position: String) extends Dockable(view, position)
     5.6  {
     5.7 -  private val readme = new HTML_Panel("SansSerif", 14)
     5.8 +  Swing_Thread.require()
     5.9 +
    5.10 +  private val readme = new HTML_Panel
    5.11    private val readme_path = Path.explode("$JEDIT_HOME/README.html")
    5.12 -  readme.render_document(
    5.13 -    Isabelle_System.platform_file_url(readme_path), File.try_read(List(readme_path)))
    5.14 +  readme.render_document(Isabelle_System.platform_file_url(readme_path), File.read(readme_path))
    5.15  
    5.16    set_content(readme)
    5.17  }