store.json (settings file) not created by SaveSettings or SettingsFile RunParms (on Mac)

[ghost]

SettingsFile,MY-pa-store.json
LoadSettings
BLAHBLAH
RunProofAsstGUI
SaveSettings

generates E-UT-1602, Saving Settings File Failed error message.

The java doc for the code in mmj.pa.SessionStore#save()

try (PrintStream s = new PrintStream(file)) {
            s.println(dat);

indicates that the file will be created, but nooo...

Seems to me that in the SettingsFile code, if the filename is valid but it does not exist at that time, then create an empty file. Boom. Problem solved.

[ghost]

@digama0 : Added code in setSettings() of

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

setSettings()

    try {
        if (!file.exists())
            file.createNewFile();
    } catch (final IOException e) {
        throw error(e, ERRMSG_CREATE_FAILED, e.getMessage());
    }

Assuming this is a bug, not intended (must be local to Mac because impossible to believe intentionally doing this.)

[digama0]

So the problem is that new PrintStream doesn't create the file if it doesn't already exist? Surely there is an option for that. I would prefer that this is done in SessionStore#save() since that way we don't create an empty file if we never bother to save settings in the end for whatever reason.

[ghost]

Ok. i propose to move the "fix" to SessionStore.

There is a different way to create a PrintStream. Probably longer -- the doc says this is a convenience constructor

...creates the necessary intermediate OutputStreamWriter <eclipse-javadoc:%E2%98%82=mmj2/%5C/Library%5C/Java%5C/JavaVirtualMachines%5C/jdk1.8.0_181.jdk%5C/Contents%5C/Home%5C/jre%5C/lib%5C/rt.jar%3Cjava.io(PrintStream.class%E2%98%83PrintStream~PrintStream~Ljava.io.File;%E2%98%82java.io.OutputStreamWriter>, which will encode characters using the default charset <eclipse-javadoc:%E2%98%82=mmj2/%5C/Library%5C/Java%5C/JavaVirtualMachines%5C/jdk1.8.0_181.jdk%5C/Contents%5C/Home%5C/jre%5C/lib%5C/rt.jar%3Cjava.io(PrintStream.class%E2%98%83PrintStream~PrintStream~Ljava.io.File;%E2%98%82java.nio.charset.Charset%E2%98%82defaultCharset%E2%98%82> for this instance of the Java virtual machine.

I don't care about the empty settings file because once they start using settings then they won't stop and it is irrelevant if it was once empty.

I already put the fix into StoreBoss but it is easy to move it. Let's take action and move forward. I will just add it to the rest of my "fixes". About a dozen modules at this point. I think the Search works much better now and I've done a little elsewhere. Just need more testing and I'm working on setting that up now (it will be manual at first while I work out the issues ...)

Best, Mel.

On Sep 29, 2018, at 18:59, Mario Carneiro notifications@github.com wrote:

So the problem is that new PrintStream doesn't create the file if it doesn't already exist? Surely there is an option for that. I would prefer that this is done in SessionStore#save() since that way we don't create an empty file if we never bother to save settings in the end for whatever reason.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/digama0/mmj2/issues/11#issuecomment-425687745, or mute the thread https://github.com/notifications/unsubscribe-auth/ApDxkY4cBfKdYVE6z60FBGgnPgFvwNGNks5ugCWRgaJpZM4XAR24.

[ghost]

ok @digama0 -- moved to mmj.pa.SessionStore.java :

if (file.exists()) Files.copy(file.toPath(), file.toPath() .resolveSibling(file.getName() + PaConstants.BACKUP_SUFFIX), StandardCopyOption.REPLACE_EXISTING); else file.createNewFile();

(This is not the first time I have seen differences between Windows and Mac even when the doc promises cross-platform compatibility.)