Skip to content
Success

Changes

Summary

  1. enforce rebuild of Isabelle/ML, after various changes to build database management;
  2. more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
  3. tuned output;
  4. clarified database content: store actual value instead of index;
  5. more robust: disallow override;
  6. tuned messages;
  7. more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
  8. clarified signature: manage "verbose" flag via "progress";
  9. removed unused arguments: avoid ambiguity concerning progress/verbose;
  10. clarified protocol for "verbose" messages;
  11. clarified signature: manage "verbose" flag via "progress";
  12. tuned;
  13. tuned;
  14. more operations;
  15. tuned signature;
  16. more robust: proper bound checks;
  17. enforce rebuild of Isabelle/ML, after various changes to build database management;
  18. clarified modules;
  19. clarified signature: manage "verbose" flag via "progress";
  20. clarified treatment of "verbose" messages, e.g. Progress.theory(); always store messages within database, with explicit "verbose" flag: client-side will decide about output;
  21. proper "val verbose" (amending 2e2b2bd6b2d2);
  22. tuned whitespace;
  23. more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
  24. support progress backed by database; moved Build_Progress.Context.progress/log to class Build_Process: database is available here;
  25. tuned;
  26. tuned messages;
  27. clarified signature: require just one "override def echo(message: Progress.Message): Unit";
  28. tuned signature;
  29. tuned signature;
  30. clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
  31. proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo;
Changeset 77528:26ec258e5cf8 by wenzelm:
enforce rebuild of Isabelle/ML, after various changes to build database management;
The file was modified src/Pure/ROOT.ML (diff)
Changeset 77527:790085b1002f by wenzelm:
more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
The file was modified src/Pure/General/sql.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77526:e3ed231fa214 by wenzelm:
tuned output;
The file was modified src/Pure/System/host.scala (diff)
Changeset 77525:de6fb423fd4b by wenzelm:
clarified database content: store actual value instead of index;
The file was modified src/Pure/System/host.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77524:a3dda42cd110 by wenzelm:
more robust: disallow override;
The file was modified src/Pure/System/progress.scala (diff)
Changeset 77523:9398c48ea3d2 by wenzelm:
tuned messages;
The file was modified src/Pure/Tools/server.scala (diff)
Changeset 77522:a1d30297cd61 by wenzelm:
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77521:5642de4d225d by wenzelm:
clarified signature: manage "verbose" flag via "progress";
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala (diff)
The file was modified src/Pure/Admin/ci_build.scala (diff)
The file was modified src/Pure/Thy/browser_info.scala (diff)
The file was modified src/Pure/Thy/document_build.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)
The file was modified src/Pure/Tools/update.scala (diff)
Changeset 77520:84aa349ed597 by wenzelm:
removed unused arguments: avoid ambiguity concerning progress/verbose;
The file was modified src/Pure/Thy/document_build.scala (diff)
Changeset 77519:12ace037d05e by wenzelm:
clarified protocol for "verbose" messages;
The file was modified NEWS (diff)
The file was modified src/Doc/System/Server.thy (diff)
The file was modified src/Pure/Tools/server.scala (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)
Changeset 77518:fda4da0f80f4 by wenzelm:
clarified signature: manage "verbose" flag via "progress";
The file was modified src/Pure/General/mercurial.scala (diff)
The file was modified src/Pure/General/rsync.scala (diff)
The file was modified src/Pure/Tools/sync.scala (diff)
Changeset 77517:ede77a627b3a by wenzelm:
tuned;
The file was modified src/Pure/General/rsync.scala (diff)
The file was modified src/Pure/Thy/document_build.scala (diff)
The file was modified src/Pure/Tools/sync.scala (diff)
Changeset 77516:71e3e144dc08 by wenzelm:
tuned;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 77515:6aae7486e94a by wenzelm:
more operations;
The file was modified src/Pure/ROOT.scala (diff)
The file was modified src/Pure/library.scala (diff)
Changeset 77514:acaa89cb977b by wenzelm:
tuned signature;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77513:43bfb65ee9b3 by wenzelm:
more robust: proper bound checks;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77512:9853251b958e by wenzelm:
enforce rebuild of Isabelle/ML, after various changes to build database management;
The file was modified src/Pure/ROOT.ML (diff)
Changeset 77511:3d6db917bd1b by wenzelm:
clarified modules;
The file was modified src/Pure/General/logger.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77510:f5d6cd98b16a by wenzelm:
clarified signature: manage "verbose" flag via "progress";
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala (diff)
The file was modified src/Pure/Admin/build_csdp.scala (diff)
The file was modified src/Pure/Admin/build_e.scala (diff)
The file was modified src/Pure/Admin/build_minisat.scala (diff)
The file was modified src/Pure/Admin/build_polyml.scala (diff)
The file was modified src/Pure/Admin/build_spass.scala (diff)
The file was modified src/Pure/Admin/build_status.scala (diff)
The file was modified src/Pure/Admin/build_vampire.scala (diff)
The file was modified src/Pure/Admin/build_verit.scala (diff)
The file was modified src/Pure/Admin/build_zipperposition.scala (diff)
The file was modified src/Pure/Admin/ci_build.scala (diff)
The file was modified src/Pure/Thy/document_build.scala (diff)
The file was modified src/Pure/Tools/build_docker.scala (diff)
The file was modified src/Pure/Tools/dotnet_setup.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
The file was modified src/Tools/VSCode/src/build_vscodium.scala (diff)
Changeset 77509:3bc49507bae5 by wenzelm:
clarified treatment of &quot;verbose&quot; messages, e.g. Progress.theory();<br>always store messages within database, with explicit &quot;verbose&quot; flag: client-side will decide about output;
The file was modified src/Pure/Admin/build_release.scala (diff)
The file was modified src/Pure/General/ssh.scala (diff)
The file was modified src/Pure/System/components.scala (diff)
The file was modified src/Pure/System/progress.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
The file was modified src/Pure/Tools/server.scala (diff)
The file was modified src/Tools/VSCode/src/channel.scala (diff)
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/session_build.scala (diff)
Changeset 77508:7d13996ffecc by wenzelm:
proper &quot;val verbose&quot; (amending 2e2b2bd6b2d2);
The file was modified src/Tools/VSCode/src/channel.scala (diff)
Changeset 77507:8dfe2fbc98e7 by wenzelm:
tuned whitespace;
The file was modified src/Pure/System/progress.scala (diff)
Changeset 77506:a8175b950173 by wenzelm:
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
The file was modified src/Pure/System/progress.scala (diff)
Changeset 77505:7ee426daafa3 by wenzelm:
support progress backed by database;<br>moved Build_Progress.Context.progress/log to class Build_Process: database is available here;
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77504:fd40e36045fd by wenzelm:
tuned;
The file was modified src/Pure/System/isabelle_system.scala (diff)
The file was modified src/Pure/System/options.scala (diff)
The file was modified src/Pure/System/progress.scala (diff)
The file was modified src/Pure/Tools/build_docker.scala (diff)
The file was modified src/Tools/jEdit/jedit_main/isabelle_sidekick.scala (diff)
Changeset 77503:daf632e9ce7e by wenzelm:
tuned messages;
The file was modified src/Pure/System/progress.scala (diff)
Changeset 77502:2e2b2bd6b2d2 by wenzelm:
clarified signature: require just one &quot;override def echo(message: Progress.Message): Unit&quot;;
The file was modified src/Pure/System/progress.scala (diff)
The file was modified src/Pure/Tools/server.scala (diff)
The file was modified src/Tools/VSCode/src/channel.scala (diff)
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/session_build.scala (diff)
Changeset 77501:2d8815f98537 by wenzelm:
tuned signature;
The file was modified src/Pure/General/output.scala (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
Changeset 77500:bbb78dba6f68 by wenzelm:
tuned signature;
The file was modified src/Pure/General/output.scala (diff)
Changeset 77499:8fc94efa954a by wenzelm:
clarified signature: more uniform Progress.verbose, avoid adhoc &quot;override def theory()&quot;;
The file was modified src/Pure/System/progress.scala (diff)
The file was modified src/Tools/VSCode/src/channel.scala (diff)
The file was modified src/Tools/jEdit/src/session_build.scala (diff)
Changeset 77498:2d12cb7ff829 by wenzelm:
proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo;
The file was modified src/Pure/System/progress.scala (diff)
The file was modified src/Tools/VSCode/src/channel.scala (diff)
The file was modified src/Tools/jEdit/src/session_build.scala (diff)