src/Tools/jEdit/src/jedit/html_panel.scala
changeset 37164 8b4617ad1593
parent 37069 7d796b72099f
child 37202 382a56c9f295
     1.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 28 16:01:25 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 28 17:48:18 2010 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  import isabelle._
     1.5  
     1.6  import java.io.StringReader
     1.7 -import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
     1.8 +import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
     1.9  import java.awt.event.MouseEvent
    1.10  
    1.11  import java.util.logging.{Logger, Level}
    1.12 @@ -36,7 +36,11 @@
    1.13  }
    1.14  
    1.15  
    1.16 -class HTML_Panel(system: Isabelle_System, initial_font_size: Int) extends HtmlPanel
    1.17 +class HTML_Panel(
    1.18 +    system: Isabelle_System,
    1.19 +    initial_font_family: String,
    1.20 +    initial_font_size: Int)
    1.21 +  extends HtmlPanel
    1.22  {
    1.23    /** Lobo setup **/
    1.24  
    1.25 @@ -101,9 +105,9 @@
    1.26  </html>
    1.27  """
    1.28  
    1.29 -  private def template(font_size: Int): String =
    1.30 +  private def template(font_family: String, font_size: Int): String =
    1.31      template_head +
    1.32 -    "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
    1.33 +    "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px }" +
    1.34      template_tail
    1.35  
    1.36  
    1.37 @@ -111,7 +115,7 @@
    1.38  
    1.39    /* internal messages */
    1.40  
    1.41 -  private case class Resize(font_size: Int)
    1.42 +  private case class Resize(font_family: String, font_size: Int)
    1.43    private case class Render(body: List[XML.Tree])
    1.44    private case object Refresh
    1.45  
    1.46 @@ -120,22 +124,26 @@
    1.47      /* internal state */
    1.48  
    1.49      var current_font_metrics: FontMetrics = null
    1.50 +    var current_font_family = ""
    1.51      var current_font_size: Int = 0
    1.52      var current_margin: Int = 0
    1.53      var current_body: List[XML.Tree] = Nil
    1.54  
    1.55 -    def resize(font_size: Int)
    1.56 +    def resize(font_family: String, font_size: Int)
    1.57      {
    1.58 +      val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size)))
    1.59        val (font_metrics, margin) =
    1.60          Swing_Thread.now {
    1.61 -          val metrics = getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
    1.62 +          val metrics = getFontMetrics(font)
    1.63            (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
    1.64          }
    1.65        if (current_font_metrics == null ||
    1.66 +          current_font_family != font_family ||
    1.67            current_font_size != font_size ||
    1.68            current_margin != margin)
    1.69        {
    1.70          current_font_metrics = font_metrics
    1.71 +        current_font_family = font_family
    1.72          current_font_size = font_size
    1.73          current_margin = margin
    1.74          refresh()
    1.75 @@ -153,7 +161,8 @@
    1.76              .map(t => XML.Elem(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE)), HTML.spans(t))))
    1.77        val doc =
    1.78          builder.parse(
    1.79 -          new InputSourceImpl(new StringReader(template(current_font_size)), "http://localhost"))
    1.80 +          new InputSourceImpl(
    1.81 +            new StringReader(template(current_font_family, current_font_size)), "http://localhost"))
    1.82        doc.removeChild(doc.getLastChild())
    1.83        doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
    1.84        Swing_Thread.later { setDocument(doc, rcontext) }
    1.85 @@ -162,11 +171,11 @@
    1.86  
    1.87      /* main loop */
    1.88  
    1.89 -    resize(initial_font_size)
    1.90 +    resize(initial_font_family, initial_font_size)
    1.91  
    1.92      loop {
    1.93        react {
    1.94 -        case Resize(font_size) => resize(font_size)
    1.95 +        case Resize(font_family, font_size) => resize(font_family, font_size)
    1.96          case Refresh => refresh()
    1.97          case Render(body) => render(body)
    1.98          case bad => System.err.println("main_actor: ignoring bad message " + bad)
    1.99 @@ -177,7 +186,7 @@
   1.100  
   1.101    /* external methods */
   1.102  
   1.103 -  def resize(font_size: Int) { main_actor ! Resize(font_size) }
   1.104 +  def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
   1.105    def refresh() { main_actor ! Refresh }
   1.106    def render(body: List[XML.Tree]) { main_actor ! Render(body) }
   1.107  }