Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Tools/jEdit/src/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 1 kB

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

quality95%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

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.