Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned messages;
  3. NEWS;
  4. proper profiling within command execution: messages require PIDE id;
  5. more systematic treatment of profiling mode;
  6. tuned message;
  7. prefer less intrusive tracing message;
  8. clarified documentation: tracing messages are not shown here;
  9. add missing file;
  10. more formal ML profiling messages;
  11. clarified modules;
Changeset 73844:8a9fd2ffb81d by wenzelm:
merged
Changeset 73843:014b944f4972 by wenzelm:
tuned messages;
The file was modified src/Pure/ML/ml_profiling.ML (diff)
The file was modified src/Pure/ML/ml_profiling.scala (diff)
Changeset 73842:9134ae401ad5 by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 73841:95484bd7e1ec by wenzelm:
proper profiling within command execution: messages require PIDE id;
The file was modified src/Pure/Isar/runtime.ML (diff)
The file was modified src/Pure/Tools/build.ML (diff)
Changeset 73840:a5200fa7cb4c by wenzelm:
more systematic treatment of profiling mode;
The file was modified src/Pure/ML/ml_profiling.ML (diff)
The file was modified src/Pure/ML/ml_profiling.scala (diff)
The file was modified src/Pure/Tools/build.ML (diff)
Changeset 73839:0638fa8c01bc by wenzelm:
tuned message;
The file was modified src/Pure/ML/ml_profiling.scala (diff)
Changeset 73838:0e6a5a6cc767 by wenzelm:
prefer less intrusive tracing message;
The file was modified src/Pure/ML/ml_profiling.ML (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
The file was modified src/Pure/Tools/profiling_report.scala (diff)
Changeset 73837:f72335f6a9ed by wenzelm:
clarified documentation: tracing messages are not shown here;
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 73836:690fdc14f7fb by wenzelm:
add missing file;
The file was addedsrc/Pure/ML/ml_profiling.scala
Changeset 73835:5dae03d50db1 by wenzelm:
more formal ML profiling messages;
The file was modified src/Pure/ML/ml_profiling.ML (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
The file was modified src/Pure/Tools/profiling_report.scala (diff)
The file was modified src/Pure/build-jars (diff)
Changeset 73834:364bac6691de by wenzelm:
clarified modules;
The file was modified src/Pure/General/output.ML (diff)
The file was modified src/Pure/ML/ml_profiling.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)