#805 (Mar 15, 2017, 8:28:08 PM)

1. merged (detail / hgweb)
2. unused; (detail / hgweb)
3. misc tuning and modernization; (detail / hgweb)
4. clarified message; (detail / hgweb)
5. keep PIDE.plugin for the sake of still open dockables etc. -- jEdit exits these *after* the stop operation; (detail / hgweb)
6. keep style extender for the sake of potentially remaining token markers; (detail / hgweb)
7. dynamic session_options for tuning parameters and initial prover options; (detail / hgweb)
8. strict initialization of plugin.session: no user errors to be expected before session.start; (detail / hgweb)
9. resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
   PIDE._plugin indicates intialization state of Plugin;
   tuned; (detail / hgweb)
10. clarified initialization;
    tuned; (detail / hgweb)
11. clarified initialization; (detail / hgweb)
12. clarified modules; (detail / hgweb)
13. clarified modules; (detail / hgweb)
14. more explicit strict vs. non-strict initialization; (detail / hgweb)
15. more explicit options;
    tuned signature; (detail / hgweb)
16. unused; (detail / hgweb)
17. clarified fall-back base, e.g. relevant for "isabelle jedit -l BAD"; (detail / hgweb)
18. tuned whitespace; (detail / hgweb)
19. map values statically; (detail / hgweb)
20. clarified modules; (detail / hgweb)
21. tuned signature; (detail / hgweb)
22. tuned signature; (detail / hgweb)
23. tuned; (detail / hgweb)
24. tuned signature; (detail / hgweb)
25. clarified singleton module; (detail / hgweb)
26. proper plugin access; (detail / hgweb)
27. clarified modules; (detail / hgweb)
28. proper plugin access; (detail / hgweb)
29. tuned; (detail / hgweb)
30. prefer local variables; (detail / hgweb)
31. clarified modules; (detail / hgweb)
32. avoid global variables with implicit initialization; (detail / hgweb)
33. more robust early initialization; (detail / hgweb)
34. show user error as on command-line, e.g. relevant for unexpected crashes; (detail / hgweb)
35. afford early initialization of JEdit_Options, but it may lead to messy exception trace for malformed etc/preferences (see also 6eeaaefcea56);
    tuned signature; (detail / hgweb)
36. tuned message; (detail / hgweb)
37. normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection; (detail / hgweb)
38. always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again; (detail / hgweb)
39. avoid race condition between current_state().stable_tip_version and model.rendering(); (detail / hgweb)
40. tuned; (detail / hgweb)
41. updated dependencies; (detail / hgweb)
42. explicitly ignore "initialized" message; (detail / hgweb)
43. clarified shutdown; (detail / hgweb)
44. tuned; (detail / hgweb)
45. tuned; (detail / hgweb)
46. support for permanent phase_changed watcher; (detail / hgweb)
47. tuned; (detail / hgweb)
48. more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready; (detail / hgweb)
49. more robust debugger initialization, e.g. required for GUI components before actual session startup; (detail / hgweb)
50. more abstract module Document; (detail / hgweb)
51. tuned; (detail / hgweb)
52. misc tuning and simplification; (detail / hgweb)
53. more explicit Session.xml_cache; (detail / hgweb)
54. tuned; (detail / hgweb)
55. tuned signature; (detail / hgweb)
56. tuned signature; (detail / hgweb)
57. clarified modules; (detail / hgweb)
58. proper local debugger state, depending on session;
    tuned signature; (detail / hgweb)
59. more robust startup/init: let Session.stop wait for protocol handler initialization; (detail / hgweb)
60. tuned; (detail / hgweb)
61. tuned signature; (detail / hgweb)
62. tuned signature; (detail / hgweb)
63. more robust Session.stop: idempotent, avoid conflict with startup; (detail / hgweb)
64. more strict Session.start: no restart from terminated session; (detail / hgweb)
65. clarified Session.Phase; (detail / hgweb)

Started by an SCM change

This run spent:

• 5 min 4 sec waiting;
• 1 hr 30 min build duration;
• 1 hr 35 min total from scheduled to completion.