replaced jedit_relative_font_size by jedit_font_scale;

--- 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)"

--- 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)
 

--- 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 */