reuse main view.font from jEdit;
authorwenzelm
Fri May 28 17:48:18 2010 +0200 (2010-05-28 ago)
changeset 371648b4617ad1593
parent 37163 a60f88087ee1
child 37165 c2e27ae53c2a
reuse main view.font from jEdit;
src/Tools/jEdit/src/jedit/html_panel.scala
src/Tools/jEdit/src/jedit/output_dockable.scala
src/Tools/jEdit/src/jedit/plugin.scala
     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  }
     2.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 28 16:01:25 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 28 17:48:18 2010 +0200
     2.3 @@ -24,7 +24,8 @@
     2.4  {
     2.5    Swing_Thread.assert()
     2.6  
     2.7 -  val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
     2.8 +  val html_panel =
     2.9 +    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
    2.10    add(html_panel, BorderLayout.CENTER)
    2.11  
    2.12  
    2.13 @@ -40,7 +41,8 @@
    2.14    private def handle_resize()
    2.15    {
    2.16      Swing_Thread.now {
    2.17 -      html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
    2.18 +      html_panel.resize(Isabelle.font_family(),
    2.19 +        scala.math.round(Isabelle.font_size() * zoom_factor / 100))
    2.20      }
    2.21    }
    2.22  
     3.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri May 28 16:01:25 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Fri May 28 17:48:18 2010 +0200
     3.3 @@ -71,6 +71,11 @@
     3.4        jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
     3.5    }
     3.6  
     3.7 +
     3.8 +  /* font */
     3.9 +
    3.10 +  def font_family(): String = jEdit.getProperty("view.font")
    3.11 +
    3.12    def font_size(): Float =
    3.13      (jEdit.getIntegerProperty("view.fontsize", 16) *
    3.14        Int_Property("relative-font-size", 100)).toFloat / 100