tuned signature;
authorwenzelm
Sun Nov 25 21:10:29 2012 +0100 (2012-11-25)
changeset 502066626bc5ed053
parent 50205 788c8263e634
child 50207 54be125d8cdc
tuned signature;
uniform view.fontsize fallback;
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/isabelle_actions.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/symbols_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Sun Nov 25 21:10:29 2012 +0100
     1.3 @@ -76,8 +76,8 @@
     1.4    {
     1.5      Swing_Thread.require()
     1.6  
     1.7 -    pretty_text_area.resize(PIDE.font_family(),
     1.8 -      (PIDE.font_size("jedit_font_scale") * zoom_factor / 100).round)
     1.9 +    pretty_text_area.resize(Rendering.font_family(),
    1.10 +      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
    1.11    }
    1.12  
    1.13  
     2.1 --- a/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 20:59:32 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 21:10:29 2012 +0100
     2.3 @@ -19,9 +19,8 @@
     2.4  
     2.5    def change_font_size(view: View, change: Int => Int)
     2.6    {
     2.7 -    val FONT_SIZE = "view.fontsize"
     2.8 -    val size = change(jEdit.getIntegerProperty(FONT_SIZE, 12)) max 5
     2.9 -    jEdit.setIntegerProperty(FONT_SIZE, size)
    2.10 +    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
    2.11 +    jEdit.setIntegerProperty("view.fontsize", size)
    2.12      jEdit.propertiesChanged()
    2.13      jEdit.saveSettings()
    2.14      view.getStatus.setMessageAndClear("Text font size: " + size)
     3.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 25 21:10:29 2012 +0100
     3.3 @@ -47,8 +47,8 @@
     3.4    {
     3.5      Swing_Thread.require()
     3.6  
     3.7 -    pretty_text_area.resize(PIDE.font_family(),
     3.8 -      (PIDE.font_size("jedit_font_scale") * zoom_factor / 100).round)
     3.9 +    pretty_text_area.resize(Rendering.font_family(),
    3.10 +      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
    3.11    }
    3.12  
    3.13    private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 20:59:32 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 21:10:29 2012 +0100
     4.3 @@ -47,14 +47,6 @@
     4.4    }
     4.5  
     4.6  
     4.7 -  /* font */
     4.8 -
     4.9 -  def font_family(): String = jEdit.getProperty("view.font")
    4.10 -
    4.11 -  def font_size(scale: String): Float =
    4.12 -    (jEdit.getIntegerProperty("view.fontsize", 16) * options.real(scale)).toFloat
    4.13 -
    4.14 -
    4.15    /* document model and view */
    4.16  
    4.17    def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
     5.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Nov 25 20:59:32 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Nov 25 21:10:29 2012 +0100
     5.3 @@ -68,8 +68,8 @@
     5.4  
     5.5    val pretty_text_area = new Pretty_Text_Area(view)
     5.6    pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
     5.7 -  pretty_text_area.resize(PIDE.font_family(),
     5.8 -    PIDE.font_size("jedit_tooltip_font_scale").round)
     5.9 +  pretty_text_area.resize(Rendering.font_family(),
    5.10 +    Rendering.font_size("jedit_tooltip_font_scale").round)
    5.11    pretty_text_area.update(rendering.snapshot, body)
    5.12  
    5.13    pretty_text_area.registerKeyboardAction(action_listener, "close_all",
     6.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 20:59:32 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 21:10:29 2012 +0100
     6.3 @@ -14,7 +14,7 @@
     6.4  import javax.swing.Icon
     6.5  
     6.6  import org.gjt.sp.jedit.syntax.{Token => JEditToken}
     6.7 -import org.gjt.sp.jedit.GUIUtilities
     6.8 +import org.gjt.sp.jedit.{jEdit, GUIUtilities}
     6.9  
    6.10  import scala.collection.immutable.SortedMap
    6.11  
    6.12 @@ -58,6 +58,14 @@
    6.13    val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
    6.14  
    6.15  
    6.16 +  /* jEdit font */
    6.17 +
    6.18 +  def font_family(): String = jEdit.getProperty("view.font")
    6.19 +
    6.20 +  def font_size(scale: String): Float =
    6.21 +    (jEdit.getIntegerProperty("view.fontsize", 16) * PIDE.options.real(scale)).toFloat
    6.22 +
    6.23 +
    6.24    /* token markup -- text styles */
    6.25  
    6.26    private val command_style: Map[String, Byte] =
     7.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
     7.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sun Nov 25 21:10:29 2012 +0100
     7.3 @@ -24,7 +24,7 @@
     7.4    private class Symbol_Component(val symbol: String) extends Button
     7.5    {
     7.6      private val decoded = Symbol.decode(symbol)
     7.7 -    private val font_size = PIDE.font_size("jedit_font_scale").round
     7.8 +    private val font_size = Rendering.font_size("jedit_font_scale").round
     7.9  
    7.10      font =
    7.11        Symbol.fonts.get(symbol) match {