Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Tools/jEdit/src/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 1 kB image not shown  

Quelle  font_info.scala   Sprache: Scala

 
/*  Title:      Tools/jEdit/src/font_info.scala
    Author:     Makarius

Font information, derived from main jEdit view font.
*/


package isabelle.jedit


import isabelle._


import java.awt.Font

import org.gjt.sp.jedit.jEdit


object Font_Info {
  /* size range */

  val min_size = 5
  val max_size = 250

  def restrict_size(size: Float): Float = size max min_size.toFloat min max_size.toFloat


  /* main 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, zoom: Zoom = null): Font_Info =
    Font_Info(main_family(), main_size(if (zoom == null) scale else scale * zoom.scale))

  class Zoom extends GUI.Zoom { tooltip = "Zoom factor for output font size" }


  /* incremental size change */

  object main_change {
    private def change_size(change: Float => Float): Unit = {
      GUI_Thread.require {}

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

    // owned by GUI thread
    private var steps = 0
    private val delay = Delay.last(PIDE.session.input_delay, gui = true) {
      change_size { size =>
        var i = size.round
        while (steps != 0 && i > 0) {
          if (steps > 0) { i += (i / 10) max 1; steps -= 1 }
          else { i -= (i / 10) max 1; steps += 1 }
        }
        steps = 0
        i.toFloat
      }
    }

    def step(i: Int): Unit = {
      steps += i
      delay.invoke()
    }

    def reset(size: Float): Unit = {
      delay.revoke()
      steps = 0
      change_size(_ => size)
    }
  }
}

sealed case class Font_Info(family: String, size: Float) {
  def font: Font = new Font(family, Font.PLAIN, size.round)
}

95%


¤ Dauer der Verarbeitung: 0.11 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.