Skip to content
[Jenkins]Jenkins
log in
Started 1 yr 4 mo ago
Took 1 hr 55 min on workermtahpc
Success

#1864 (Jan 16, 2023, 2:38:33 AM)

Build Artifacts
Changes
  1. tuned; (detail / hgweb)
  2. clarified modules; (detail / hgweb)
  3. merged (detail / hgweb)
  4. more complete Bibtex database; (detail / hgweb)
  5. proper theory context for formal citations; (detail / hgweb)
  6. isabelle update -u cite; (detail / hgweb)
  7. clarified treatment of cite macro name; (detail / hgweb)
  8. explicit legacy_feature; (detail / hgweb)
  9. more robust: rely on PIDE markup instead of regex guess; (detail / hgweb)
  10. more index entries; (detail / hgweb)
  11. updated documentation; (detail / hgweb)
  12. clarified names; (detail / hgweb)
  13. tuned; (detail / hgweb)
  14. clarified options and defaults: avoid accidental changed of base logic due to augment_options(update_options); (detail / hgweb)
  15. update documentation: prefer control-symbol-cartouche form of "cite" antiquotations; (detail / hgweb)
  16. tuned; (detail / hgweb)
  17. proper language context; (detail / hgweb)
  18. proper normal form of adjacent XML.Text, notably for Bibtex.update_cite; (detail / hgweb)
  19. tuned whitespace; (detail / hgweb)
  20. more robust; (detail / hgweb)
  21. basic support for update_cite_commands; (detail / hgweb)
  22. more operations: use proper constants; (detail / hgweb)
  23. proper session_options (amending da13da82f6f9); (detail / hgweb)
  24. tuned signature; (detail / hgweb)
  25. tuned; (detail / hgweb)
  26. clarified types; (detail / hgweb)
  27. more explicit language context; (detail / hgweb)
  28. clarified signature: more explicit types; (detail / hgweb)
  29. support embedded syntax, for use with control symbols; (detail / hgweb)
  30. tuned; (detail / hgweb)
  31. tuned; (detail / hgweb)
  32. clarified default: final value is provided in Isabelle/Scala Latex.Cite.unapply; (detail / hgweb)
  33. more "cite" antiquotations; (detail / hgweb)
  34. clarified signature: more generic operations; (detail / hgweb)
  35. clarified check: this could be \nocite; (detail / hgweb)
  36. avoid confusion of markup element vs. property names; (detail / hgweb)
  37. clarified Latex markup: optional cite "location" consists of nested document text; (detail / hgweb)
  38. more explicit latex markup; (detail / hgweb)
  39. follow recent changes of Sledgehammer defaults, as 0a46b3dbd5ad exposes a hint in the source text; (detail / hgweb)
  40. One messy, messy proof (detail / hgweb)

Started by an SCM change

This run spent:

  • 1 hr 48 min waiting;
  • 1 hr 55 min build duration;
  • 3 hr 44 min total from scheduled to completion.
Revision: 11c0747a87fc477e4df0820f25d186c767d351bc