Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more documentation;
  2. support JVM runtime statistics;
  3. clarified worker threads;
  4. misc tuning, based on hints by IntelliJ IDEA;
  5. clarified GUI;
  6. tuned GUI;
  7. tuned GUI;
  8. clarified order for GUI;
  9. tuned;
  10. clarified GUI;
Changeset 72150:510ebf846696 by wenzelm:
more documentation;
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/Doc/JEdit/JEdit.thy (diff)
Changeset 72149:36a34f3a8cb8 by wenzelm:
support JVM runtime statistics;
The file was modified src/Pure/ML/ml_statistics.scala (diff)
The file was modified src/Pure/System/platform.scala (diff)
Changeset 72148:d2dc9bc3a3e1 by wenzelm:
clarified worker threads;
The file was modified src/Pure/Concurrent/isabelle_thread.scala (diff)
Changeset 72147:2375b38a42f8 by wenzelm:
misc tuning, based on hints by IntelliJ IDEA;
The file was modified src/Tools/jEdit/src/monitor_dockable.scala (diff)
Changeset 72146:d8dd3aa6dae9 by wenzelm:
clarified GUI;
The file was modified src/Pure/PIDE/protocol.ML (diff)
The file was modified src/Tools/jEdit/src/monitor_dockable.scala (diff)
Changeset 72145:25db9c4209ee by wenzelm:
tuned GUI;
The file was modified src/Tools/jEdit/src/monitor_dockable.scala (diff)
Changeset 72144:6a4e51ca53c3 by wenzelm:
tuned GUI;
The file was modified src/Tools/jEdit/src/ml_status.scala (diff)
Changeset 72143:4a46650bf701 by wenzelm:
clarified order for GUI;
The file was modified src/Pure/ML/ml_statistics.scala (diff)
Changeset 72142:6e8b5cdd4ba0 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/ml_status.scala (diff)
Changeset 72141:262d3c11a24d by wenzelm:
clarified GUI;
The file was modified src/Tools/jEdit/src/ml_status.scala (diff)