1/* Title: Tools/jEdit/src/font_info.scala 2 Author: Makarius 3 4Font information, derived from main jEdit view font. 5*/ 6 7package isabelle.jedit 8 9 10import isabelle._ 11 12 13import java.awt.Font 14 15import org.gjt.sp.jedit.{jEdit, View} 16 17 18object Font_Info 19{ 20 /* size range */ 21 22 val min_size = 5 23 val max_size = 250 24 25 def restrict_size(size: Float): Float = size max min_size min max_size 26 27 28 /* main jEdit font */ 29 30 def main_family(): String = jEdit.getProperty("view.font") 31 32 def main_size(scale: Double = 1.0): Float = 33 restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat) 34 35 def main(scale: Double = 1.0): Font_Info = 36 Font_Info(main_family(), main_size(scale)) 37 38 39 /* incremental size change */ 40 41 object main_change 42 { 43 private def change_size(change: Float => Float) 44 { 45 GUI_Thread.require {} 46 47 val size0 = main_size() 48 val size = restrict_size(change(size0)).round 49 if (size != size0) { 50 jEdit.setIntegerProperty("view.fontsize", size) 51 jEdit.propertiesChanged() 52 jEdit.saveSettings() 53 jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size) 54 } 55 } 56 57 // owned by GUI thread 58 private var steps = 0 59 private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) 60 { 61 change_size(size => 62 { 63 var i = size.round 64 while (steps != 0 && i > 0) { 65 if (steps > 0) 66 { i += (i / 10) max 1; steps -= 1 } 67 else 68 { i -= (i / 10) max 1; steps += 1 } 69 } 70 steps = 0 71 i.toFloat 72 }) 73 } 74 75 def step(i: Int) 76 { 77 steps += i 78 delay.invoke() 79 } 80 81 def reset(size: Float) 82 { 83 delay.revoke() 84 steps = 0 85 change_size(_ => size) 86 } 87 } 88 89 90 /* zoom box */ 91 92 abstract class Zoom_Box extends GUI.Zoom_Box { tooltip = "Zoom factor for output font size" } 93} 94 95sealed case class Font_Info(family: String, size: Float) 96{ 97 def font: Font = new Font(family, Font.PLAIN, size.round) 98} 99 100