| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Pure/General/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle space.scala Sprache: Scala |
|||||||||
|
/* Title: Pure/General/space.scala
Author: Makarius Storage space based on bytes. */ package isabelle import java.util.Locale import scala.annotation.tailrec object Space { def bytes(bs: Long): Space = new Space(bs) val zero: Space = bytes(0L) private val units: List[String] = List("B", "KiB", "MiB", "GiB", "TiB", "PiB", "EiB") def B(x: Double): Space = bytes(x.round) def KiB(x: Double): Space = B(x * 1024) def MiB(x: Double): Space = KiB(x * 1024) def GiB(x: Double): Space = MiB(x * 1024) def TiB(x: Double): Space = GiB(x * 1024) def PiB(x: Double): Space = TiB(x * 1024) def EiB(x: Double): Space = PiB(x * 1024) } final class Space private(val bytes: Long) extends AnyVal { def + (other: Space): Space = new Space(bytes + other.bytes) def - (other: Space): Space = new Space(bytes - other.bytes) def * (scalar: Double): Space = new Space((bytes * scalar).round) def / (other: Space): Double = B / other.B def is_proper: Boolean = bytes > 0 def is_relevant: Boolean = MiB >= 1.0 def used(free: Space): Space = new Space((bytes - free.bytes) max 0) def used_fraction(free: Space): Double = if (is_proper && used(free).is_proper) used(free).B / B else 0.0 def B: Double = bytes.toDouble def KiB: Double = B / 1024 def MiB: Double = KiB / 1024 def GiB: Double = MiB / 1024 def TiB: Double = GiB / 1024 def PiB: Double = TiB / 1024 def EiB: Double = PiB / 1024 override def toString: String = Value.Long(bytes) def print: String = { @tailrec def print_unit(x: Double, units: List[String]): String = if (x.abs < 1024 || units.tail.isEmpty) { val s = String.format(Locale.ROOT, "%.1f", x.asInstanceOf[AnyRef]) Library.perhaps_unsuffix(".0", s) + " " + units.head } else print_unit(x / 1024, units.tail) print_unit(bytes.toDouble, Space.units) } def print_relevant: Option[String] = if (is_relevant) Some(print) else None } ¤ Dauer der Verarbeitung: 0.3 Sekunden ¤*© Formatika GbR, Deutschland |
|
2026-03-28