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

ghost commented 5 years ago

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 commented 5 years ago

mmj.util.StoreBoss attachment for review!

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

digama0 commented 5 years ago

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 commented 5 years ago

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 notifications@github.com 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 https://github.com/digama0/mmj2/issues/12#issuecomment-426535892, or mute the thread https://github.com/notifications/unsubscribe-auth/ApDxkak6GbURxfDK6eFQXRBJXJZLuOnwks5uhGS1gaJpZM4XExeO.

digama0 commented 5 years ago

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 commented 5 years ago

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 notifications@github.com 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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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.

digama0 / mmj2

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