Thomas has convinced me not to change Leo's session-handling code
significantly. I have closed #3417
<https://github.com/leo-editor/leo-editor/issues/3417> and its related PR:
Leo will retain its session-* commands and related documentation.
However, Leonistas disagree about *when *to write *session data *(a list
outlines). Some say, "Always." Others say, "Only if the command line had no
outlines."
We usually do not argue about preferences. However, a per-outline setting
won't do. And I refuse to add a command-line option to resolve this minor
question.
What to do? It's a puzzle.
When I awoke this morning, I saw the way forward. I'll add an Easter Egg to
Leo's startup and shutdown code. A tiny new plugin, *modify_sessions*, will
exploit the hidden code. Like this:
1: Restore the *g.app.loaded_session* ivar, inited (as before) to False.
2: Add the *g.app.always_write_session_data *ivar, inited to True.
3: Change the shutdown logic in two places:
if g.app.sessionManager and (
g.app.loaded_session or g.app.always_write_session_data
):
g.app.sessionManager.save_snapshot()
4: Create the modifiy_sessions plugin, containing (sans docstrings) only:
def init():
g.app.always_write_session_data = False
*Summary*
Leo will retain its session-* commands and related documentation.
Leonistas disagree about when Leo should write session data. Some say,
"Always." Others say, "Only if the command line had no outlines."
Neither a command-line option nor a per-outline setting can resolve this
question.
I'll modify PR #3215 <https://github.com/leo-editor/leo-editor/pull/3215> so
that Leo always writes session data. Those who prefer otherwise can enable
the modify_session plugin.
All your comments are welcome.
Edward
--
You received this message because you are subscribed to the Google Groups
"leo-editor" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/leo-editor/f0fbf1ae-85ef-4963-a2b5-edc0a9149eefn%40googlegroups.com.
