# HG changeset patch
# User wenzelm
# Date 1353874229 -3600
# Node ID 6626bc5ed053887c9b1f006992b8602cba18015e
# Parent  788c8263e6342a94744a43290032b7672dd48a76
tuned signature;
uniform view.fontsize fallback;

diff -r 788c8263e634 -r 6626bc5ed053 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Sun Nov 25 21:10:29 2012 +0100
@@ -76,8 +76,8 @@
   {
     Swing_Thread.require()
 
-    pretty_text_area.resize(PIDE.font_family(),
-      (PIDE.font_size("jedit_font_scale") * zoom_factor / 100).round)
+    pretty_text_area.resize(Rendering.font_family(),
+      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
   }
 
 
diff -r 788c8263e634 -r 6626bc5ed053 src/Tools/jEdit/src/isabelle_actions.scala
--- a/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 20:59:32 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 21:10:29 2012 +0100
@@ -19,9 +19,8 @@
 
   def change_font_size(view: View, change: Int => Int)
   {
-    val FONT_SIZE = "view.fontsize"
-    val size = change(jEdit.getIntegerProperty(FONT_SIZE, 12)) max 5
-    jEdit.setIntegerProperty(FONT_SIZE, size)
+    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
+    jEdit.setIntegerProperty("view.fontsize", size)
     jEdit.propertiesChanged()
     jEdit.saveSettings()
     view.getStatus.setMessageAndClear("Text font size: " + size)
diff -r 788c8263e634 -r 6626bc5ed053 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 25 21:10:29 2012 +0100
@@ -47,8 +47,8 @@
   {
     Swing_Thread.require()
 
-    pretty_text_area.resize(PIDE.font_family(),
-      (PIDE.font_size("jedit_font_scale") * zoom_factor / 100).round)
+    pretty_text_area.resize(Rendering.font_family(),
+      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
   }
 
   private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
diff -r 788c8263e634 -r 6626bc5ed053 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 20:59:32 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 21:10:29 2012 +0100
@@ -47,14 +47,6 @@
   }
 
 
-  /* font */
-
-  def font_family(): String = jEdit.getProperty("view.font")
-
-  def font_size(scale: String): Float =
-    (jEdit.getIntegerProperty("view.fontsize", 16) * options.real(scale)).toFloat
-
-
   /* document model and view */
 
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
diff -r 788c8263e634 -r 6626bc5ed053 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Nov 25 20:59:32 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Nov 25 21:10:29 2012 +0100
@@ -68,8 +68,8 @@
 
   val pretty_text_area = new Pretty_Text_Area(view)
   pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
-  pretty_text_area.resize(PIDE.font_family(),
-    PIDE.font_size("jedit_tooltip_font_scale").round)
+  pretty_text_area.resize(Rendering.font_family(),
+    Rendering.font_size("jedit_tooltip_font_scale").round)
   pretty_text_area.update(rendering.snapshot, body)
 
   pretty_text_area.registerKeyboardAction(action_listener, "close_all",
diff -r 788c8263e634 -r 6626bc5ed053 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 20:59:32 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 21:10:29 2012 +0100
@@ -14,7 +14,7 @@
 import javax.swing.Icon
 
 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
-import org.gjt.sp.jedit.GUIUtilities
+import org.gjt.sp.jedit.{jEdit, GUIUtilities}
 
 import scala.collection.immutable.SortedMap
 
@@ -58,6 +58,14 @@
   val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
 
 
+  /* jEdit font */
+
+  def font_family(): String = jEdit.getProperty("view.font")
+
+  def font_size(scale: String): Float =
+    (jEdit.getIntegerProperty("view.fontsize", 16) * PIDE.options.real(scale)).toFloat
+
+
   /* token markup -- text styles */
 
   private val command_style: Map[String, Byte] =
diff -r 788c8263e634 -r 6626bc5ed053 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sun Nov 25 21:10:29 2012 +0100
@@ -24,7 +24,7 @@
   private class Symbol_Component(val symbol: String) extends Button
   {
     private val decoded = Symbol.decode(symbol)
-    private val font_size = PIDE.font_size("jedit_font_scale").round
+    private val font_size = Rendering.font_size("jedit_font_scale").round
 
     font =
       Symbol.fonts.get(symbol) match {