Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. show GC progress as "ML cleanup";
  2. ML status widget similar to org.gjt.sp.jedit.gui.statusbar.MemoryStatusWidgetFactory;
  3. support for Poly/ML memory status;
  4. clarified signature;
  5. removed pointless option "ML_statistics": always enabled;
  6. removed pointless GUI controls for ML_statistics --- no longer part of prover protocol (see also 38a64cc17403);
  7. support for GC state;
Changeset 72140:ae6544cf1c8c by wenzelm:
show GC progress as "ML cleanup";
The file was modified src/Tools/jEdit/src/ml_status.scala (diff)
Changeset 72139:f5c085dfa02f by wenzelm:
ML status widget similar to org.gjt.sp.jedit.gui.statusbar.MemoryStatusWidgetFactory;
The file was addedsrc/Tools/jEdit/src/ml_status.scala
The file was modified src/Tools/jEdit/lib/Tools/jedit (diff)
The file was modified src/Tools/jEdit/src/jEdit.props (diff)
The file was modified src/Tools/jEdit/src/services.xml (diff)
Changeset 72138:fa57d299b46b by wenzelm:
support for Poly/ML memory status;
The file was modified src/Pure/ML/ml_statistics.scala (diff)
Changeset 72137:ad277a335aa5 by wenzelm:
clarified signature;
The file was modified src/Pure/General/properties.scala (diff)
Changeset 72136:98dca728fc9c by wenzelm:
removed pointless option "ML_statistics": always enabled;
The file was modified etc/options (diff)
The file was modified src/Pure/ML/ml_statistics.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 72135:f67e83608745 by wenzelm:
removed pointless GUI controls for ML_statistics --- no longer part of prover protocol (see also 38a64cc17403);
The file was modified src/Tools/jEdit/src/isabelle.scala (diff)
The file was modified src/Tools/jEdit/src/monitor_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/protocol_dockable.scala (diff)
Changeset 72134:f40200b5bb3c by wenzelm:
support for GC state;
The file was modified src/Pure/ML/ml_statistics.ML (diff)