--- a/src/Tools/jEdit/lib/Tools/jedit Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Mar 01 19:39:27 2014 +0100
@@ -16,6 +16,7 @@
"src/documentation_dockable.scala"
"src/find_dockable.scala"
"src/fold_handling.scala"
+ "src/font_info.scala"
"src/graphview_dockable.scala"
"src/info_dockable.scala"
"src/isabelle.scala"
--- a/src/Tools/jEdit/src/completion_popup.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Sat Mar 01 19:39:27 2014 +0100
@@ -196,7 +196,8 @@
def open_popup(result: Completion.Result)
{
val font =
- painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
+ painter.getFont.deriveFont(
+ Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
val range = result.range
def invalidate(): Unit = JEdit_Lib.invalidate_range(text_area, range)
--- a/src/Tools/jEdit/src/find_dockable.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/find_dockable.scala Sat Mar 01 19:39:27 2014 +0100
@@ -56,8 +56,8 @@
{
Swing_Thread.require()
- pretty_text_area.resize(Rendering.font_family(),
- (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
}
private val delay_resize =
@@ -121,7 +121,7 @@
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
setColumns(40)
setToolTipText(query_label.tooltip)
- setFont(GUI.imitate_font(Rendering.font_family(), getFont, 1.2))
+ setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
}
private case class Context_Entry(val name: String, val description: String)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/font_info.scala Sat Mar 01 19:39:27 2014 +0100
@@ -0,0 +1,58 @@
+/* Title: Tools/jEdit/src/jedit_font.scala
+ Author: Makarius
+
+Font information, derived from main view font.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import java.awt.Font
+
+import org.gjt.sp.jedit.{jEdit, View}
+
+
+object Font_Info
+{
+ val dummy: Font_Info = Font_Info("Dialog", 12.0f)
+
+
+ /* size range */
+
+ val min_size = 5
+ val max_size = 250
+
+ def restrict_size(size: Float): Float = size max min_size min max_size
+
+
+ /* jEdit font */
+
+ def main_family(): String = jEdit.getProperty("view.font")
+
+ def main_size(scale: Double = 1.0): Float =
+ restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat)
+
+ def main(scale: Double = 1.0): Font_Info =
+ Font_Info(main_family(), main_size(scale))
+
+ def main_change(change: Float => Float)
+ {
+ val size0 = main_size()
+ val size = restrict_size(change(size0)).round
+ if (size != size0) {
+ jEdit.setIntegerProperty("view.fontsize", size)
+ jEdit.propertiesChanged()
+ jEdit.saveSettings()
+ jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
+ }
+ }
+}
+
+sealed case class Font_Info(family: String, size: Float)
+{
+ def font: Font = new Font(family, Font.PLAIN, size.round)
+}
+
--- a/src/Tools/jEdit/src/info_dockable.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Sat Mar 01 19:39:27 2014 +0100
@@ -76,8 +76,8 @@
{
Swing_Thread.require()
- pretty_text_area.resize(Rendering.font_family(),
- (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
}
--- a/src/Tools/jEdit/src/isabelle.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sat Mar 01 19:39:27 2014 +0100
@@ -192,17 +192,17 @@
private var steps = 0
private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
{
- Rendering.font_size_change(i =>
+ Font_Info.main_change(size =>
{
- var j = i
- while (steps != 0 && j > 0) {
+ var i = size.round
+ while (steps != 0 && i > 0) {
if (steps > 0)
- { j += (j / 10) max 1; steps -= 1 }
+ { i += (i / 10) max 1; steps -= 1 }
else
- { j -= (j / 10) max 1; steps += 1 }
+ { i -= (i / 10) max 1; steps += 1 }
}
steps = 0
- j
+ i.toFloat
})
}
def step(i: Int) { steps += i; delay.invoke() }
@@ -212,7 +212,7 @@
def reset_font_size()
{
font_size.reset()
- Rendering.font_size_change(_ => PIDE.options.int("jedit_reset_font_size"))
+ Font_Info.main_change(_ => PIDE.options.int("jedit_reset_font_size").toFloat)
}
def increase_font_size() { font_size.step(1) }
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Mar 01 19:39:27 2014 +0100
@@ -30,7 +30,7 @@
protected var _end = int_to_pos(end)
override def getIcon: Icon = null
override def getShortString: String =
- "<html><span style=\"font-family: " + Rendering.font_family() + ";\">" +
+ "<html><span style=\"font-family: " + Font_Info.main_family() + ";\">" +
HTML.encode(_name) + "</span></html>"
override def getLongString: String = _name
override def getName: String = _name
--- a/src/Tools/jEdit/src/output_dockable.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Sat Mar 01 19:39:27 2014 +0100
@@ -41,8 +41,8 @@
{
Swing_Thread.require()
- pretty_text_area.resize(Rendering.font_family(),
- (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
}
private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 01 19:39:27 2014 +0100
@@ -61,8 +61,7 @@
Swing_Thread.require()
- private var current_font_family = "Dialog"
- private var current_font_size: Int = 12
+ private var current_font_info: Font_Info = Font_Info.dummy
private var current_body: XML.Body = Nil
private var current_base_snapshot = Document.Snapshot.init
private var current_base_results = Command.Results.empty
@@ -80,18 +79,19 @@
{
Swing_Thread.require()
- val font = new Font(current_font_family, Font.PLAIN, current_font_size)
+ val font = current_font_info.font
getPainter.setFont(font)
getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
- getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
+ getPainter.setStyles(
+ SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
val fold_line_style = new Array[SyntaxStyle](4)
for (i <- 0 to 3) {
fold_line_style(i) =
SyntaxUtilities.parseStyle(
jEdit.getProperty("view.style.foldLine." + i),
- current_font_family, current_font_size, true)
+ current_font_info.family, current_font_info.size.round, true)
}
getPainter.setFoldLineStyle(fold_line_style)
@@ -139,12 +139,11 @@
}
}
- def resize(font_family: String, font_size: Int)
+ def resize(font_info: Font_Info)
{
Swing_Thread.require()
- current_font_family = font_family
- current_font_size = font_size
+ current_font_info = font_info
refresh()
}
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 01 19:39:27 2014 +0100
@@ -199,8 +199,7 @@
}
})
- pretty_text_area.resize(Rendering.font_family(),
- Rendering.font_size("jedit_popup_font_scale").round)
+ pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale")))
/* main content */
--- a/src/Tools/jEdit/src/rendering.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Mar 01 19:39:27 2014 +0100
@@ -41,30 +41,6 @@
Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
- /* jEdit font */
-
- def font_family(): String = jEdit.getProperty("view.font")
-
- private def view_font_size(): Int = jEdit.getIntegerProperty("view.fontsize", 16)
- private val font_size0 = 5
- private val font_size1 = 250
-
- def font_size(scale: String): Float =
- (view_font_size() * PIDE.options.real(scale)).toFloat max font_size0 min font_size1
-
- def font_size_change(change: Int => Int)
- {
- val size0 = view_font_size()
- val size = change(size0) max font_size0 min font_size1
- if (size != size0) {
- jEdit.setIntegerProperty("view.fontsize", size)
- jEdit.propertiesChanged()
- jEdit.saveSettings()
- jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
- }
- }
-
-
/* popup window bounds */
def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Sat Mar 01 19:39:27 2014 +0100
@@ -84,7 +84,7 @@
private def do_paint()
{
Swing_Thread.later {
- text_area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
+ text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
}
}
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Mar 01 19:39:27 2014 +0100
@@ -181,7 +181,7 @@
def do_paint()
{
Swing_Thread.later {
- area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
+ area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
}
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Mar 01 19:39:27 2014 +0100
@@ -57,8 +57,8 @@
{
Swing_Thread.require()
- pretty_text_area.resize(Rendering.font_family(),
- (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
}
private val delay_resize =
--- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Mar 01 19:39:27 2014 +0100
@@ -26,7 +26,7 @@
private class Symbol_Component(val symbol: String) extends Button
{
private val decoded = Symbol.decode(symbol)
- private val font_size = Rendering.font_size("jedit_font_scale").round
+ private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
font =
Symbol.fonts.get(symbol) match {