diff --git a/src/Pure/ML/ml_statistics.scala b/src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala +++ b/src/Pure/ML/ml_statistics.scala @@ -1,324 +1,324 @@ /* Title: Pure/ML/ml_statistics.scala Author: Makarius ML runtime statistics. */ package isabelle import scala.annotation.tailrec import scala.collection.mutable import scala.collection.immutable.{SortedSet, SortedMap} import scala.swing.{Frame, Component} import org.jfree.data.xy.{XYSeries, XYSeriesCollection} import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} import org.jfree.chart.plot.PlotOrientation object ML_Statistics { /* properties */ val Now = new Properties.Double("now") def now(props: Properties.T): Double = Now.unapply(props).get /* memory status */ val Heap_Size = new Properties.Long("size_heap") val Heap_Free = new Properties.Long("size_heap_free_last_GC") val GC_Percent = new Properties.Int("GC_percent") sealed case class Memory_Status(heap_size: Long, heap_free: Long, gc_percent: Int) { def heap_used: Long = (heap_size - heap_free) max 0 def heap_used_fraction: Double = if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size def gc_progress: Option[Double] = if (1 <= gc_percent && gc_percent <= 100) Some((gc_percent - 1) * 0.01) else None } def memory_status(props: Properties.T): Memory_Status = { val heap_size = Heap_Size.get(props) val heap_free = Heap_Free.get(props) val gc_percent = GC_Percent.get(props) Memory_Status(heap_size, heap_free, gc_percent) } /* monitor process */ def monitor(pid: Long, stats_dir: String = "", delay: Time = Time.seconds(0.5), consume: Properties.T => Unit = Console.println) { def progress_stdout(line: String) { val props = Library.space_explode(',', line).flatMap((entry: String) => Library.space_explode('=', entry) match { case List(a, b) => Some((a, b)) case _ => None }) if (props.nonEmpty) consume(props) } val env_prefix = if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n" Bash.process(env_prefix + "exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " + ML_Syntax.print_double(delay.seconds)), cwd = Path.explode("~~").file) .result(progress_stdout = progress_stdout, strict = false).check } /* protocol handler */ class Handler extends Session.Protocol_Handler { private var session: Session = null private var monitoring: Future[Unit] = Future.value(()) override def init(session: Session): Unit = synchronized { this.session = session } override def exit(): Unit = synchronized { session = null monitoring.cancel } private def consume(props: Properties.T): Unit = synchronized { if (session != null) { - val props1 = (session.xml_cache.props(props ::: Platform.jvm_statistics())) + val props1 = (session.xml_cache.props(props ::: Java_Statistics.jvm_statistics())) session.runtime_statistics.post(Session.Runtime_Statistics(props1)) } } private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.ML_Statistics(pid, stats_dir) => monitoring = Future.thread("ML_statistics") { monitor(pid, stats_dir = stats_dir, consume = consume) } true case _ => false } } override val functions = List(Markup.ML_Statistics.name -> ml_statistics) } /* memory fields (mega bytes) */ def mem_print(x: Long): Option[String] = if (x == 0L) None else Some(x.toString + " M") def mem_scale(x: Long): Long = x / 1024 / 1024 def mem_field_scale(name: String, x: Double): Double = if (heap_fields._2.contains(name) || program_fields._2.contains(name)) mem_scale(x.toLong).toDouble else x val CODE_SIZE = "size_code" val STACK_SIZE = "size_stacks" val HEAP_SIZE = "size_heap" /* standard fields */ type Fields = (String, List[String]) val tasks_fields: Fields = ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent", "tasks_total")) val workers_fields: Fields = ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) val GC_fields: Fields = ("GCs", List("partial_GCs", "full_GCs", "share_passes")) val heap_fields: Fields = ("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free", "size_heap_free_last_full_GC", "size_heap_free_last_GC")) val program_fields: Fields = ("Program", List("size_code", "size_stacks")) val threads_fields: Fields = ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) val time_fields: Fields = ("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC")) val speed_fields: Fields = ("Speed", List("speed_CPU", "speed_GC")) private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC") val java_heap_fields: Fields = ("Java heap", List("java_heap_size", "java_heap_used")) val java_thread_fields: Fields = ("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active")) val main_fields: List[Fields] = List(heap_fields, tasks_fields, workers_fields) val other_fields: List[Fields] = List(threads_fields, GC_fields, program_fields, time_fields, speed_fields, java_heap_fields, java_thread_fields) val all_fields: List[Fields] = main_fields ::: other_fields /* content interpretation */ final case class Entry(time: Double, data: Map[String, Double]) { def get(field: String): Double = data.getOrElse(field, 0.0) } val empty: ML_Statistics = apply(Nil) def apply(ml_statistics0: List[Properties.T], heading: String = "", domain: String => Boolean = (key: String) => true): ML_Statistics = { require(ml_statistics0.forall(props => Now.unapply(props).isDefined)) val ml_statistics = ml_statistics0.sortBy(now) val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head) val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start val fields = SortedSet.empty[String] ++ (for { props <- ml_statistics.iterator (x, _) <- props.iterator if x != Now.name && domain(x) } yield x) val content = { var last_edge = Map.empty[String, (Double, Double, Double)] val result = new mutable.ListBuffer[ML_Statistics.Entry] for (props <- ml_statistics) { val time = now(props) - time_start // rising edges -- relative speed val speeds = (for { (key, value) <- props.iterator key1 <- time_speed.get(key) if domain(key1) } yield { val (x0, y0, s0) = last_edge.getOrElse(key, (0.0, 0.0, 0.0)) val x1 = time val y1 = java.lang.Double.parseDouble(value) val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0) if (y1 > y0) { last_edge += (key -> (x1, y1, s1)) (key1, s1.toString) } else (key1, s0.toString) }).toList val data = SortedMap.empty[String, Double] ++ (for { (x, y) <- props.iterator ++ speeds.iterator if x != Now.name && domain(x) z = java.lang.Double.parseDouble(y) if z != 0.0 } yield { (x.intern, mem_field_scale(x, z)) }) result += ML_Statistics.Entry(time, data) } result.toList } new ML_Statistics(heading, fields, content, time_start, duration) } } final class ML_Statistics private( val heading: String, val fields: Set[String], val content: List[ML_Statistics.Entry], val time_start: Double, val duration: Double) { /* content */ def maximum(field: String): Double = (0.0 /: content)({ case (m, e) => m max e.get(field) }) def average(field: String): Double = { @tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double = list match { case Nil => acc case e :: es => val t = e.time sum(t, es, (t - t0) * e.get(field) + acc) } content match { case Nil => 0.0 case List(e) => e.get(field) case e :: es => sum(e.time, es, 0.0) / duration } } /* charts */ def update_data(data: XYSeriesCollection, selected_fields: List[String]) { data.removeAllSeries for (field <- selected_fields) { val series = new XYSeries(field) content.foreach(entry => series.add(entry.time, entry.get(field))) data.addSeries(series) } } def chart(title: String, selected_fields: List[String]): JFreeChart = { val data = new XYSeriesCollection update_data(data, selected_fields) ChartFactory.createXYLineChart(title, "time", "value", data, PlotOrientation.VERTICAL, true, true, true) } def chart(fields: ML_Statistics.Fields): JFreeChart = chart(fields._1, fields._2) def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit = fields.map(chart).foreach(c => GUI_Thread.later { new Frame { iconImage = GUI.isabelle_image() title = heading contents = Component.wrap(new ChartPanel(c)) visible = true } }) } diff --git a/src/Pure/System/java_statistics.scala b/src/Pure/System/java_statistics.scala new file mode 100644 --- /dev/null +++ b/src/Pure/System/java_statistics.scala @@ -0,0 +1,45 @@ +/* Title: Pure/System/java_statistics.scala + Author: Makarius + +Java runtime statistics. +*/ + +package isabelle + + +object Java_Statistics +{ + /* memory status */ + + sealed case class Memory_Status(heap_size: Long, heap_free: Long) + { + def heap_used: Long = (heap_size - heap_free) max 0 + def heap_used_fraction: Double = + if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size + } + + def memory_status(): Memory_Status = + { + val heap_size = Runtime.getRuntime.totalMemory() + val heap_used = heap_size - Runtime.getRuntime.freeMemory() + Memory_Status(heap_size, heap_used) + } + + + /* JVM statistics */ + + def jvm_statistics(): Properties.T = + { + val status = memory_status() + val threads = Thread.activeCount() + val workers = Isabelle_Thread.pool.getPoolSize + val workers_active = Isabelle_Thread.pool.getActiveCount + + List( + "java_heap_size" -> status.heap_size.toString, + "java_heap_used" -> status.heap_used.toString, + "java_threads_total" -> threads.toString, + "java_workers_total" -> workers.toString, + "java_workers_active" -> workers_active.toString) + } +} diff --git a/src/Pure/System/platform.scala b/src/Pure/System/platform.scala --- a/src/Pure/System/platform.scala +++ b/src/Pure/System/platform.scala @@ -1,106 +1,71 @@ /* Title: Pure/System/platform.scala Author: Makarius System platform identification. */ package isabelle object Platform { /* platform family */ val is_linux: Boolean = System.getProperty("os.name", "") == "Linux" val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X" val is_windows: Boolean = System.getProperty("os.name", "").startsWith("Windows") def family: Family.Value = if (is_linux) Family.linux else if (is_macos) Family.macos else if (is_windows) Family.windows else error("Failed to determine current platform family") object Family extends Enumeration { val linux, macos, windows = Value def unapply(name: String): Option[Value] = try { Some(withName(name)) } catch { case _: NoSuchElementException => None } def parse(name: String): Value = unapply(name) getOrElse error("Bad platform family: " + quote(name)) } /* platform identifiers */ private val X86 = """i.86|x86""".r private val X86_64 = """amd64|x86_64""".r def cpu_arch: String = System.getProperty("os.arch", "") match { case X86() => "x86" case X86_64() => "x86_64" case _ => error("Failed to determine CPU architecture") } def os_name: String = family match { case Family.macos => "darwin" case _ => family.toString } lazy val jvm_platform: String = cpu_arch + "-" + os_name /* JVM version */ private val Version = """1\.(\d+)\.0_(\d+)""".r lazy val jvm_version: String = System.getProperty("java.version") match { case Version(a, b) => a + "u" + b case a => a } /* JVM name */ val jvm_name: String = System.getProperty("java.vm.name", "") - - - /* memory status */ - - sealed case class Memory_Status(heap_size: Long, heap_free: Long) - { - def heap_used: Long = (heap_size - heap_free) max 0 - def heap_used_fraction: Double = - if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size - } - - def memory_status(): Memory_Status = - { - val heap_size = Runtime.getRuntime.totalMemory() - val heap_used = heap_size - Runtime.getRuntime.freeMemory() - Memory_Status(heap_size, heap_used) - } - - - /* JVM statistics */ - - def jvm_statistics(): Properties.T = - { - val status = memory_status() - val threads = Thread.activeCount() - val workers = Isabelle_Thread.pool.getPoolSize - val workers_active = Isabelle_Thread.pool.getActiveCount - - List( - "java_heap_size" -> status.heap_size.toString, - "java_heap_used" -> status.heap_used.toString, - "java_threads_total" -> threads.toString, - "java_workers_total" -> workers.toString, - "java_workers_active" -> workers_active.toString) - } } diff --git a/src/Pure/build-jars b/src/Pure/build-jars --- a/src/Pure/build-jars +++ b/src/Pure/build-jars @@ -1,307 +1,308 @@ #!/usr/bin/env bash # # Author: Makarius # # build-jars - build Isabelle/Scala # # Requires proper Isabelle settings environment. ## sources declare -a SOURCES=( src/HOL/Tools/Nitpick/kodkod.scala src/Pure/Admin/afp.scala src/Pure/Admin/build_cygwin.scala src/Pure/Admin/build_doc.scala src/Pure/Admin/build_fonts.scala src/Pure/Admin/build_history.scala src/Pure/Admin/build_jdk.scala src/Pure/Admin/build_log.scala src/Pure/Admin/build_polyml.scala src/Pure/Admin/build_release.scala src/Pure/Admin/build_status.scala src/Pure/Admin/check_sources.scala src/Pure/Admin/ci_profile.scala src/Pure/Admin/components.scala src/Pure/Admin/isabelle_cronjob.scala src/Pure/Admin/isabelle_devel.scala src/Pure/Admin/jenkins.scala src/Pure/Admin/other_isabelle.scala src/Pure/Concurrent/consumer_thread.scala src/Pure/Concurrent/counter.scala src/Pure/Concurrent/delay.scala src/Pure/Concurrent/event_timer.scala src/Pure/Concurrent/future.scala src/Pure/Concurrent/isabelle_thread.scala src/Pure/Concurrent/mailbox.scala src/Pure/Concurrent/par_list.scala src/Pure/Concurrent/synchronized.scala src/Pure/GUI/color_value.scala src/Pure/GUI/gui.scala src/Pure/GUI/gui_thread.scala src/Pure/GUI/popup.scala src/Pure/GUI/wrap_panel.scala src/Pure/General/antiquote.scala src/Pure/General/bytes.scala src/Pure/General/cache.scala src/Pure/General/codepoint.scala src/Pure/General/comment.scala src/Pure/General/completion.scala src/Pure/General/csv.scala src/Pure/General/date.scala src/Pure/General/exn.scala src/Pure/General/file.scala src/Pure/General/file_watcher.scala src/Pure/General/graph.scala src/Pure/General/graph_display.scala src/Pure/General/graphics_file.scala src/Pure/General/http.scala src/Pure/General/json.scala src/Pure/General/linear_set.scala src/Pure/General/logger.scala src/Pure/General/long_name.scala src/Pure/General/mercurial.scala src/Pure/General/multi_map.scala src/Pure/General/output.scala src/Pure/General/path.scala src/Pure/General/position.scala src/Pure/General/pretty.scala src/Pure/General/properties.scala src/Pure/General/rdf.scala src/Pure/General/scan.scala src/Pure/General/sha1.scala src/Pure/General/sql.scala src/Pure/General/ssh.scala src/Pure/General/symbol.scala src/Pure/General/time.scala src/Pure/General/timing.scala src/Pure/General/untyped.scala src/Pure/General/url.scala src/Pure/General/utf8.scala src/Pure/General/uuid.scala src/Pure/General/value.scala src/Pure/General/word.scala src/Pure/General/xz.scala src/Pure/Isar/document_structure.scala src/Pure/Isar/keyword.scala src/Pure/Isar/line_structure.scala src/Pure/Isar/outer_syntax.scala src/Pure/Isar/parse.scala src/Pure/Isar/token.scala src/Pure/ML/ml_console.scala src/Pure/ML/ml_lex.scala src/Pure/ML/ml_process.scala src/Pure/ML/ml_statistics.scala src/Pure/ML/ml_syntax.scala src/Pure/PIDE/byte_message.scala src/Pure/PIDE/command.scala src/Pure/PIDE/command_span.scala src/Pure/PIDE/document.scala src/Pure/PIDE/document_id.scala src/Pure/PIDE/document_status.scala src/Pure/PIDE/editor.scala src/Pure/PIDE/headless.scala src/Pure/PIDE/line.scala src/Pure/PIDE/markup.scala src/Pure/PIDE/markup_tree.scala src/Pure/PIDE/protocol.scala src/Pure/PIDE/protocol_handlers.scala src/Pure/PIDE/protocol_message.scala src/Pure/PIDE/prover.scala src/Pure/PIDE/query_operation.scala src/Pure/PIDE/rendering.scala src/Pure/PIDE/resources.scala src/Pure/PIDE/session.scala src/Pure/PIDE/text.scala src/Pure/PIDE/xml.scala src/Pure/PIDE/yxml.scala src/Pure/ROOT.scala src/Pure/System/bash.scala src/Pure/System/command_line.scala src/Pure/System/cygwin.scala src/Pure/System/distribution.scala src/Pure/System/getopts.scala src/Pure/System/isabelle_charset.scala src/Pure/System/isabelle_fonts.scala src/Pure/System/isabelle_process.scala src/Pure/System/isabelle_system.scala src/Pure/System/isabelle_tool.scala + src/Pure/System/java_statistics.scala src/Pure/System/linux.scala src/Pure/System/numa.scala src/Pure/System/options.scala src/Pure/System/platform.scala src/Pure/System/posix_interrupt.scala src/Pure/System/process_result.scala src/Pure/System/progress.scala src/Pure/System/scala.scala src/Pure/System/system_channel.scala src/Pure/System/tty_loop.scala src/Pure/Thy/bibtex.scala src/Pure/Thy/export.scala src/Pure/Thy/export_theory.scala src/Pure/Thy/file_format.scala src/Pure/Thy/html.scala src/Pure/Thy/latex.scala src/Pure/Thy/present.scala src/Pure/Thy/sessions.scala src/Pure/Thy/thy_element.scala src/Pure/Thy/thy_header.scala src/Pure/Thy/thy_syntax.scala src/Pure/Tools/build.scala src/Pure/Tools/build_docker.scala src/Pure/Tools/check_keywords.scala src/Pure/Tools/debugger.scala src/Pure/Tools/doc.scala src/Pure/Tools/dump.scala src/Pure/Tools/fontforge.scala src/Pure/Tools/main.scala src/Pure/Tools/mkroot.scala src/Pure/Tools/phabricator.scala src/Pure/Tools/print_operation.scala src/Pure/Tools/profiling_report.scala src/Pure/Tools/scala_project.scala src/Pure/Tools/server.scala src/Pure/Tools/server_commands.scala src/Pure/Tools/simplifier_trace.scala src/Pure/Tools/spell_checker.scala src/Pure/Tools/task_statistics.scala src/Pure/Tools/update.scala src/Pure/Tools/update_cartouches.scala src/Pure/Tools/update_comments.scala src/Pure/Tools/update_header.scala src/Pure/Tools/update_then.scala src/Pure/Tools/update_theorems.scala src/Pure/library.scala src/Pure/pure_thy.scala src/Pure/term.scala src/Pure/term_xml.scala src/Pure/thm_name.scala src/Tools/Graphview/graph_file.scala src/Tools/Graphview/graph_panel.scala src/Tools/Graphview/graphview.scala src/Tools/Graphview/layout.scala src/Tools/Graphview/main_panel.scala src/Tools/Graphview/metrics.scala src/Tools/Graphview/model.scala src/Tools/Graphview/mutator.scala src/Tools/Graphview/mutator_dialog.scala src/Tools/Graphview/mutator_event.scala src/Tools/Graphview/popups.scala src/Tools/Graphview/shapes.scala src/Tools/Graphview/tree_panel.scala src/Tools/VSCode/src/build_vscode.scala src/Tools/VSCode/src/channel.scala src/Tools/VSCode/src/document_model.scala src/Tools/VSCode/src/dynamic_output.scala src/Tools/VSCode/src/grammar.scala src/Tools/VSCode/src/preview_panel.scala src/Tools/VSCode/src/protocol.scala src/Tools/VSCode/src/server.scala src/Tools/VSCode/src/state_panel.scala src/Tools/VSCode/src/vscode_rendering.scala src/Tools/VSCode/src/vscode_resources.scala src/Tools/VSCode/src/vscode_spell_checker.scala ) ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS]" echo echo " Options are:" echo " -f fresh build" echo exit 1 } function fail() { echo "$1" >&2 exit 2 } [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" ## process command line # options FRESH="" while getopts "f" OPT do case "$OPT" in f) FRESH=true ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -ne 0 ] && usage ## target TARGET_DIR="lib/classes" TARGET_JAR="$TARGET_DIR/Pure.jar" TARGET_SHASUM="$TARGET_DIR/Pure.shasum" function target_shasum() { shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null } function target_clean() { rm -rf "$TARGET_DIR" } [ -n "$FRESH" ] && target_clean ## build target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null if [ "$?" -ne 0 ]; then echo "### Building Isabelle/Scala ..." target_clean BUILD_DIR="$TARGET_DIR/build" mkdir -p "$BUILD_DIR" ( export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \ -d "$BUILD_DIR" "${SOURCES[@]}" ) || fail "Failed to compile sources" CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider" mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")" echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE" cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/." cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/." isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \ -C "$BUILD_DIR" META-INF \ -C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR" rm -rf "$BUILD_DIR" target_shasum > "$TARGET_SHASUM" fi diff --git a/src/Tools/jEdit/src/status_widget.scala b/src/Tools/jEdit/src/status_widget.scala --- a/src/Tools/jEdit/src/status_widget.scala +++ b/src/Tools/jEdit/src/status_widget.scala @@ -1,222 +1,222 @@ /* Title: Tools/jEdit/src/status_widget.scala Author: Makarius ML status bar: heap and garbage collection. */ package isabelle.jedit import isabelle._ import java.awt.{Color, Dimension, Graphics, Graphics2D, Insets, RenderingHints} import java.awt.font.FontRenderContext import java.awt.event.{ActionEvent, ActionListener, MouseAdapter, MouseEvent} import javax.swing.{JComponent, JLabel, Timer} import org.gjt.sp.jedit.{View, jEdit} import org.gjt.sp.jedit.gui.statusbar.{StatusWidgetFactory, Widget} object Status_Widget { /** generic GUI **/ private val template = "ABC: 99999/99999MB" abstract class GUI(view: View) extends JComponent { /* init */ setFont(new JLabel().getFont) private val font_render_context = new FontRenderContext(null, true, false) private val line_metrics = getFont.getLineMetrics(template, font_render_context) { val bounds = getFont.getStringBounds(template, font_render_context) val dim = new Dimension(bounds.getWidth.toInt, bounds.getHeight.toInt) setPreferredSize(dim) setMaximumSize(dim) } setForeground(jEdit.getColorProperty("view.status.foreground")) setBackground(jEdit.getColorProperty("view.status.background")) def progress_foreground: Color = jEdit.getColorProperty("view.status.memory.foreground") def progress_background: Color = jEdit.getColorProperty("view.status.memory.background") /* paint */ def get_status: (String, Double) override def paintComponent(gfx: Graphics) { super.paintComponent(gfx) val insets = new Insets(0, 0, 0, 0) val width = getWidth - insets.left - insets.right val height = getHeight - insets.top - insets.bottom - 1 val (text, fraction) = get_status val width2 = (width * fraction).toInt val text_bounds = gfx.getFont.getStringBounds(text, font_render_context) val text_x = insets.left + ((width - text_bounds.getWidth).toInt / 2) val text_y = (insets.top + line_metrics.getAscent).toInt gfx.asInstanceOf[Graphics2D]. setRenderingHint( RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON) gfx.setColor(progress_background) gfx.fillRect(insets.left, insets.top, width2, height) gfx.setColor(progress_foreground) gfx.setClip(insets.left, insets.top, width2, height) gfx.drawString(text, text_x, text_y) gfx.setColor(getForeground) gfx.setClip(insets.left + width2, insets.top, getWidth - insets.left - width2, height) gfx.drawString(text, text_x, text_y) } /* mouse listener */ def action: String addMouseListener(new MouseAdapter { override def mouseClicked(evt: MouseEvent) { if (evt.getClickCount == 2) { view.getInputHandler.invokeAction(action) } } }) } /** Java **/ class Java_GUI(view: View) extends GUI(view) { /* component state -- owned by GUI thread */ - private var status = Platform.memory_status() + private var status = Java_Statistics.memory_status() def get_status: (String, Double) = { ("JVM: " + (status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB", status.heap_used_fraction) } - private def update_status(new_status: Platform.Memory_Status) + private def update_status(new_status: Java_Statistics.Memory_Status) { if (status != new_status) { status = new_status repaint() } } /* timer */ private val timer = new Timer(500, new ActionListener { override def actionPerformed(e: ActionEvent) { - update_status(Platform.memory_status()) + update_status(Java_Statistics.memory_status()) } }) override def addNotify() { super.addNotify() timer.start() } override def removeNotify() { super.removeNotify() timer.stop() } /* action */ setToolTipText("Java heap memory (double-click for monitor application)") override def action: String = "isabelle.jconsole" } class Java_Factory extends StatusWidgetFactory { override def getWidget(view: View): Widget = new Widget { override def getComponent: JComponent = new Java_GUI(view) } } /** ML **/ class ML_GUI(view: View) extends GUI(view) { /* component state -- owned by GUI thread */ private var status = ML_Statistics.memory_status(Nil) def get_status: (String, Double) = status.gc_progress match { case Some(p) => ("ML cleanup", 1.0 - p) case None => ("ML: " + (status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB", status.heap_used_fraction) } private def update_status(new_status: ML_Statistics.Memory_Status) { if (status != new_status) { status = new_status repaint() } } /* main */ private val main = Session.Consumer[Session.Runtime_Statistics](getClass.getName) { case stats => val status = ML_Statistics.memory_status(stats.props) GUI_Thread.later { update_status(status) } } override def addNotify() { super.addNotify() PIDE.session.runtime_statistics += main } override def removeNotify() { super.removeNotify() PIDE.session.runtime_statistics -= main } /* action */ setToolTipText("ML heap memory (double-click for monitor panel)") override def action: String = "isabelle-monitor-float" } class ML_Factory extends StatusWidgetFactory { override def getWidget(view: View): Widget = new Widget { override def getComponent: JComponent = new ML_GUI(view) } } }