Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. recovered document output from 6bc199a70bf9;
  3. clarified command_timings protocol;
  4. more robust: include reports from Thy_Output.present_thy/output_document;
  5. more complete report positions, notably for command 'back' (amending eca176f773e0);
  6. tuned signature;
  7. clarified signature;
  8. unused;
  9. unused;
  10. tuned;
  11. removed pointless case: messages should always carry proper position;
  12. clarified names;
  13. eliminated pointless transaction;
  14. tuned signature;
  15. clarified document_output vs. progress;
  16. clarified: more uniform;
  17. more robust;
  18. clarified signature and database layout;
  19. clarified messages;
  20. unused (see ac7ae5067783, 1c451e5c145f);
  21. unused;
  22. support for PIDE markup in batch build (inactive due to pide_reports=false);
  23. clarified signature;
  24. proper output of document sources (cf. d892f6d66402);
Changeset 72713:fabd29c73098 by wenzelm:
merged
Changeset 72712:d76b0f29c8fd by wenzelm:
recovered document output from 6bc199a70bf9;
The file was modified src/Pure/Thy/thy_info.ML (diff)
Changeset 72711:9e89c2e15d36 by wenzelm:
clarified command_timings protocol;
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72710:6bc199a70bf9 by wenzelm:
more robust: include reports from Thy_Output.present_thy/output_document;
The file was modified src/Pure/Thy/thy_info.ML (diff)
Changeset 72709:cb9d5af781b4 by wenzelm:
more complete report positions, notably for command 'back' (amending eca176f773e0);
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/System/isabelle_process.ML (diff)
Changeset 72708:0cc96d337e8f by wenzelm:
tuned signature;
The file was modified src/Pure/General/position.scala (diff)
The file was modified src/Pure/PIDE/command.scala (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/Thy/export_theory.scala (diff)
Changeset 72707:f1380c9f3806 by wenzelm:
clarified signature;
The file was modified src/Pure/General/position.ML (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
Changeset 72706:52d0b5fcb19d by wenzelm:
unused;
The file was modified src/Pure/General/position.ML (diff)
Changeset 72705:0471eb6a4b99 by wenzelm:
unused;
The file was modified src/Pure/Thy/thy_info.ML (diff)
Changeset 72704:e700e830562e by wenzelm:
tuned;
The file was modified src/Pure/PIDE/command.scala (diff)
Changeset 72703:eca176f773e0 by wenzelm:
removed pointless case: messages should always carry proper position;
The file was modified src/Pure/PIDE/command.scala (diff)
Changeset 72702:79a19657c170 by wenzelm:
clarified names;
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 72701:1c42ac589fa0 by wenzelm:
eliminated pointless transaction;
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72700:c6981f55e60d by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/presentation.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72699:ed59a506998f by wenzelm:
clarified document_output vs. progress;
The file was modified src/Pure/System/progress.scala (diff)
The file was modified src/Pure/Thy/presentation.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72698:6f83f7892317 by wenzelm:
clarified: more uniform;
The file was modified src/Pure/General/file.scala (diff)
Changeset 72697:e16f85e3c288 by wenzelm:
more robust;
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72696:7af210f1f13b by wenzelm:
clarified signature and database layout;
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/Thy/presentation.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72695:45cd55248ffd by wenzelm:
clarified messages;
The file was modified src/Pure/Admin/build_log.scala (diff)
The file was modified src/Pure/Thy/presentation.scala (diff)
Changeset 72694:0116e487e4fe by wenzelm:
unused (see ac7ae5067783, 1c451e5c145f);
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 72693:0201ae367518 by wenzelm:
unused;
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72692:22aeec526ffd by wenzelm:
support for PIDE markup in batch build (inactive due to pide_reports=false);
The file was modified src/Pure/General/position.scala (diff)
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/command_span.scala (diff)
The file was modified src/Pure/PIDE/document.scala (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/PIDE/protocol_message.scala (diff)
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Pure/PIDE/session.scala (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72691:2126cf946086 by wenzelm:
clarified signature;
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 72690:53064415757a by wenzelm:
proper output of document sources (cf. d892f6d66402);
The file was modified src/Pure/Tools/dump.scala (diff)