# HG changeset patch # User wenzelm # Date 1347372654 -7200 # Node ID 97f8cb455691cfa942e0c74bd7ecaba16443702f # Parent b08f9d534a2ae4307c10a155e5d1ef8fb506aa81 replaced jedit_relative_font_size by jedit_font_scale; diff -r b08f9d534a2a -r 97f8cb455691 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Tue Sep 11 15:59:35 2012 +0200 +++ b/src/Tools/jEdit/etc/options Tue Sep 11 16:10:54 2012 +0200 @@ -6,8 +6,8 @@ option jedit_auto_start : bool = true -- "auto-start prover session on editor startup" -option jedit_relative_font_size : int = 100 - -- "relative font size of output panel wrt. main text area" +option jedit_font_scale : real = 1.0 + -- "scale factor of add-on panels wrt. main text area" option jedit_tooltip_font_size : int = 10 -- "tooltip font size (according to HTML)" diff -r b08f9d534a2a -r 97f8cb455691 src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 11 15:59:35 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 11 16:10:54 2012 +0200 @@ -16,9 +16,11 @@ { // FIXME avoid hard-wired stuff private val relevant_options = - Set("jedit_logic", "jedit_auto_start", "jedit_relative_font_size", "jedit_tooltip_font_size", + Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size", "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "jedit_load_delay") + relevant_options.foreach(Isabelle.options.value.check_name _) + private val components = Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options) diff -r b08f9d534a2a -r 97f8cb455691 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Sep 11 15:59:35 2012 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Tue Sep 11 16:10:54 2012 +0200 @@ -58,8 +58,7 @@ def font_family(): String = jEdit.getProperty("view.font") def font_size(): Float = - (jEdit.getIntegerProperty("view.fontsize", 16) * - options.int("jedit_relative_font_size")).toFloat / 100 + (jEdit.getIntegerProperty("view.fontsize", 16) * options.real("jedit_font_scale")).toFloat /* tooltip markup */