Default store.json not written relative to mmj2 path + load/saveSettings() quirk

[ghost]

Well, what I see is my store.json off somewhere in the /user2 directory, not the mmj2 directory.
That problem does not occur with a relative file name such as ocat-store.json, the program
is careful to resolve the path against mmj2. So I have a little patch for that in mmj2.util.StoreBoss.

Also I noticed that the SaveSettings and LoadSettings functions -- where ever called,
such as PA GUI -- were indirectly invoking the setSettingsFile() function used to process
the SettingsFile RunParm! That is incorrect because that RunParm is gone when PA GUI
is running.

I will upload the fixed StoreBoss later today most likely.

[ghost]

mmj.util.StoreBoss attachment for review!

https://github.com/ocatmetamath/mmj2/blob/ocatmetamath-patch-2/src/mmj/util/StoreBoss.java

[digama0]

I think the idea here is that SaveSettings and LoadSettings also take an optional argument in the same format as SettingsFile. That's why they are only calling it when they get more than zero args. That is,

SaveSettings,foo

is equivalent to

SettingsFIle,foo
SaveSettings

[ghost]

OK, got it. I put those back :0-) But still, StoreBoss.autoload() ... must not invoke loadSettings() ... protected void autoload() { if (!manualLoad) { //loadSettings(); //can't do this here -- no RunParm in hand. try { getStore().load(true); } catch (final IOException e) { throw error(e, ERRMSG_LOAD_FAILED, e.getMessage()); } } By the way, the User Guide should probably note that SaveSettings (or any other RunParm) inserted after the RunProofAsstGUI RunParm execute immediately. They don't wait for the GUI to terminate. It is started, not called. I will update github with the final adjustments today.

…

On Oct 3, 2018, at 00:18, Mario Carneiro ***@***.***> wrote: I think the idea here is that SaveSettings and LoadSettings also take an optional argument in the same format as SettingsFile. That's why they are only calling it when they get more than zero args. That is, SaveSettings,foo is equivalent to SettingsFIle,foo SaveSettings — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#12 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ApDxkak6GbURxfDK6eFQXRBJXJZLuOnwks5uhGS1gaJpZM4XExeO>.

[digama0]

I think all RunParms are synchronous except RunProofAsstGUI. (You would probably know better about this.) Then again, the RunParms file is basically structured as a configuration file so maybe it's not obvious that it's actually a really basic scripting language.

[ghost]

yes “think all RunParms are synchronous except RunProofAsstGUI. “ true runparm now misnamed. it was afterthought. next time create proper language for UI of app. .

…

On Oct 3, 2018, at 04:52, Mario Carneiro ***@***.***> wrote: I think all RunParms are synchronous except RunProofAsstGUI. (You would probably know better about this.) Then again, the RunParms file is basically structured as a configuration file so maybe it's not obvious that it's actually a really basic scripting language. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[ghost]

Ok, I just uploaded the "v2.5.2.1003" mmj2.jar.

See https://github.com/ocatmetamath/mmj2/tree/ocatmetamath-patch-2

I did more testing taking into account all my prior "fixes".
And it turned out that DisabledSettings needed work because
autoload() was un-disabling settings. So in StoreBoss we
keep state variables: enabled, file name parm, store. StoreBoss.

In other news, fyi, here are my notes from earlier:

`2018-10-03: NOTE SETTINGS
- mmj2 : I tested various RunParms with the scenario below.
Settings off, then on, then clear. What happens is:

             1) MacrosEnabled never goes to store.json, ever.
             2) Highlightng enabled only goes to store.json if
                different from the default, which is Yes (ON).
             3) Clear (the RunParm) clears the settings file name
                but does not revert all settings to their default.
                So that would affect batch regression testing. 
                Settings should normally be off in regression testing.
             4) Apparently the is no command to reset Settings to
                their default values. Simple enough though to simply
                delete the current store.json file (or whatever name.)

ProofAsstHighlightingEnabled,no
MacrosEnabled,no
ProofAsstProofFolder,myproofs
SettingsFile,OCAT-store-STUFFOFF.json
SaveSettings,OCAT-store-STUFFOFF.json

LoadSettings,OCAT-store-STUFFON.json
ProofAsstHighlightingEnabled,yes
MacrosEnabled,yes
ProofAsstProofFolder,../data/mmp/glauco-prob-rpt-01-totestsearch
SaveSettings,OCAT-store-STUFFON.json

Clear
SaveSettings
SaveSettings

`

[ghost]

OK, here is the "state of play" for Settings, as I understand the intent -- and which my code intends to match. This is the thing.

Settings:

1. when a user upgrades to the latest mmj2 Settings is automatically On. They are stored in \mmj2jar\store.json and nothing needs to be done by the user. User editing is allowed, and deletion
   of \mmj2jar\store.json resets everything to the defaults in the system.

2. The DisableSettings RunParm may be entered in the RunParms.txt file to prevent any storing
   of settings on disk. In memory Settings are used naturally, of course, but they are not saved
   between sessions. Any subsequent use of settings, via PA GUI LoadSettings or SaveSettings,
   or RunParms referencing Settings (SettingsFile, LoadSettings, SaveSettings) will re-Enable
   Settings.

3. The user may choose another file name, instead of store.json. RunParms SettingsFile,
   LoadSettings, and SaveSettings have a name parameter.

4. Do not input any Settings RunParms after the RunProofAsstGUI RunParm because it
   is merely a "start" command, not a call, and the command terminates immediately
   and then subsequent RunParms are processed, likely before the PA GUI is even shown.

5. It seems clear that the Search Options options need to be added to the JSON Settings
   scheme (except for ForWhat, that is search data, not a setting.)

[ghost]

Ok, I had that bit in #3 wrong: PA GUI File/Load Settings and File/Save Settings do not
re-enable Setting if they were disabled by RunParm DisableSettings. They just ignore
the request basically.

Here is a redo:

`Settings:

When a user upgrades to the latest mmj2, Settings is automatically Enabled. Settings are stored in \mmj2jar\store.json and nothing needs to be done by the user. User editing is allowed, and deletion
of \mmj2jar\store.json resets everything to the defaults in the system at the next file load operation.

The DisableSettings RunParm may be entered in the RunParms.txt file to prevent any storing
of settings on disk. In memory Settings are used, naturally, of course, but they are not saved
between sessions. Any subsequent use of settings, via PA GUI LoadSettings or SaveSettings
is ignored (no-op'd), while the RunParms referencing Settings (SettingsFile, LoadSettings,
SaveSettings) will re-Enable Settings.

The user may choose another file name, instead of store.json. RunParms SettingsFile,
LoadSettings, and SaveSettings have a name parameter.

Do not input any Settings RunParms after the RunProofAsstGUI RunParm because it
is merely a "start" command, not a call, and the command terminates immediately
and then subsequent RunParms are processed, likely before the PA GUI is even shown.

AND...It seems clear that the Search Options options need to be added to the JSON Settings
scheme (except for ForWhat, that is search data, not a setting.) Assuming that we are
committed to using Settings in the future...`

[ghost]

I finally figured out that "autosave on exit if enabled" is part of our deal with the users to
have Settings "just work out of the box". But because PA GUI operates asynchronously
we have to capture the exit from the app and do the save at that point; we cannot rely
on a SaveSettings RunParm to do this (or in the runIt() loop of BatchFramework.)

So...I added a save of settings to the File/Exit menu item. That works. Other methods of
exit such as closing the window or quitting Java do not execute the save even though
we have a Listener waiting for the window to close. I do not know why.

OK Here is the final on..

Settings:

When a user upgrades to the latest mmj2, Settings is automatically Enabled. Settings are stored in \mmj2jar\store.json automatically upon File/Exit from the PA GUI (other exit methods do not save.)

Nothing else needs to be done by the user. User editing is allowed, and deletion of \mmj2jar\store.json resets everything to the defaults with the next Load Settings operation.

The DisableSettings RunParm may be entered in the RunParms.txt file to prevent any use of settings on disk. In memory Settings are used, of course, but they are not saved between sessions. Any subsequent use of the PA GUI File/LoadSettings or File/SaveSettings has no effect. RunParms referencing Settings (SettingsFile, LoadSettings, SaveSettings) will re-Enable Settings.

The user may choose another file name, instead of store.json. RunParms SettingsFile, LoadSettings, and SaveSettings have a name parameter.

Do not input any Settings RunParms after the RunProofAsstGUI RunParm because it
is merely a "start" command, not a call, and the command terminates immediately
and then subsequent RunParms are processed, likely before the PA GUI is even shown.

Be sure to exit the PA GUI via File/Exit to ensure your Settings are saved to disk.

That is all.