Misc Bugs from 10/5 in PA GUI and Friends

[ghost]

Lots of little things to fix. I'm just copying my notes so there are no surprises later...

`===

2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today
- mmj2 :PA GUI Help needs updating:
- Proof Worksheet -> proof step numbers out of date
- File -> missing items
- Edit / Undo -> out of date

===

2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today

    - mmj2 : TL Menu Items:
            - Unable to set Theorem Loader Store Formulas ASIS to false
            - Unable to set Theorem Loader Audit Messages to false
            - Many problems setting Theorem Loader mmt folder, including
              showing an error message with a getYesNoAnswer() dialog!

===

2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today

    - mmj2 : File/Save Proof File
             File/Save As 
             File/Open Proof File   show default directory
             of user2, not the mmj2Path or the already given
             ProofAsstProofFolder.

===

2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today

    - mmj2 : File/New Proof asked for Theorem Label, accepted invalid
             label (see Proof Worksheet below): 

$( <PROOF_ASST> THEOREM=as;dfkljasdjklf;laaldfsjl;aadjksf;laadjksfl;adjksfl;adjksflk;ajsdkfl;jaskdlfjkl;aadksjflasjdfjlasdfasldfjklasdjfk;a;fdl;agjl;akgj LOC_AFTER=?

h1:: |- ?
2:?: |- ?
qed:?: |- ?

$)

===

2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today

    - mmj2 : Ctrl-U causes abort with following proof worksheet
             (and note that Highlighting is off, the dump just shows
             method/object names.) It is stored in blablah/mytemp/assdfsadf.mmp
             and all that is need to create the abort is to open proof file and
             hit ctrl-u.

Exception in thread "Thread-1" java.lang.NullPointerException
at mmj.pa.ProofAsst.unifyProofWorksheet(ProofAsst.java:1691)
at mmj.pa.ProofAsst.unify(ProofAsst.java:660)
at mmj.pa.ProofAsstGUI$44.send(ProofAsstGUI.java:2145)
at mmj.pa.ProofAsstGUI$RequestThreadStuff.run(ProofAsstGUI.java:2315)
at java.lang.Thread.run(Thread.java:748)

$( <PROOF_ASST> THEOREM=aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa LOC_AFTER=?

qed:?: |- ph

$)

====

2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today

    - mmj2 : runparm TheoremLoaderMMTFolder,myproofs/mmt 
             causes abort. 

             Attempting first batch test of UT19100updated.txt

END CommandLineArguments.displayArgumentOptionReport()

I-UT-0015 **** Processing RunParmFile Command #1 = ProofAsstHighlightingEnabled,no
I-UT-0015 **** Processing RunParmFile Command #2 = MacrosEnabled,no
I-UT-0015 **** Processing RunParmFile Command #3 = ProofAsstProofFolder,myproofs/mmp
I-UT-0015 **** Processing RunParmFile Command #4 = TheoremLoaderMMTFolder,myproofs/mmt
mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
java.lang.IllegalArgumentException: mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
at mmj.util.Boss.error(Boss.java:755)
at mmj.util.Boss.error(Boss.java:746)
at mmj.util.Boss.error(Boss.java:740)
at mmj.util.LogicalSystemBoss.getLogicalSystem(LogicalSystemBoss.java:164)
at mmj.util.TheoremLoaderBoss.getTlPreferences(TheoremLoaderBoss.java:105)
at mmj.util.TheoremLoaderBoss.editTheoremLoaderMMTFolder(TheoremLoaderBoss.java:158)
at mmj.util.Boss.lambda$0(Boss.java:107)
at mmj.util.Boss.doRunParmCommand(Boss.java:121)
at mmj.util.BatchFramework.executeRunParmCommand(BatchFramework.java:290)
at mmj.util.BatchFramework.runIt(BatchFramework.java:231)
at mmj.util.BatchMMJ2.main(BatchMMJ2.java:55)
Caused by: mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
... 10 more
mmj.pa.MMJException: A-UT-0200 Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
logout
Saving session...
...copying shared history...
...saving history...truncating history files...
...completed.

[Process completed]

RESOLVED: The RunParm cannot be input before LoadFile:

	TheoremLoaderMMTFolder,myproofs/mmt.

            (I did not know that.)

====

2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today

    - mmj2 : runparm file paths with '\' in RunParm causing 
             problems on Mac, but '/' ok. These are supposed
             to be system independent (in the code measures
             are required.)

====

2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today

    - mmj2 : Theorem Loader exports csbima12g to mmt folder
             with ANY proof format "normal", "packed" or "compressed"
             and gibberish? is the result?

             NEGATIVE: output in .mmt always packed format,
             which is not recognized when loaded by TL...

ProofAsstHighlightingEnabled,no
MacrosEnabled,no
LoadFile,RegressionTest1set.mm
VerifyProof,*
Parse,*
ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
ProofAsstProofFolder,myproofs/mmp/
TheoremLoaderMMTFolder,myproofs/mmt/temp
ExtractTheoremToMMTFolder,csbima12g

${
$d x y z $. $d A y $. $d A z $. $d B y $. $d B z $. $d C y $. $d C z $.
$d F y $. $d F z $.
$( Move class substitution in and out of the image of a function.
(Contributed by FL, 15-Dec-2006.) $)
csbima12g $p |- ( A e. C -> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A
/ x ]_ B ) ) $=
cA cC 1:wcel vy cA vx vy 2:cv cF cB 3:cima 4:csb csb vy cA vx 2 cF 5:csb
6:csb vy cA vx 2 cB 7:csb 8:csb 9:cima vx cA 3 csb vx cA cF 10:csb vx cA
cB 11:csb 12:cima vy vz cA 4 9 cC 1 vy vz 6 8 1 vy ax-17 vy vz cA 5 cC vz
13:cv cA wcel vy 14:ax-17 hbcsb1g vy vz cA 7 cC 14 hbcsb1g hbimad 2 cA
15:wceq 4 5 7 16:cima 6 7 cima 9 4 16 17:wceq 15 vx cv 2 18:wceq vx wex
17 vx vy a9e 18 17 vx vx vz vz 4 16 vx vz 2 3 vy 19:visset 13 2 wcel vx
20:ax-17 hbcsb1 vx vz 5 7 vx vz 2 cF 19 20 hbcsb1 vx vz 2 cB 19 20 hbcsb1
hbima hbeq 18 3 5 cB cima 4 16 18 cF 5 cB vx 2 cF csbeq1a imaeq1d vx 2 3
csbeq1a 18 cB 7 5 vx 2 cB csbeq1a imaeq2d 3eqtr3d 19.23ai ax-mp a1i 15 5
6 7 vy cA 5 csbeq1a imaeq1d 15 7 8 6 vy cA 7 csbeq1a imaeq2d 3eqtrd
csbiegf vx vy cA 3 cC csbcog 1 9 10 8 cima 12 1 6 10 8 vx vy cA cF cC
csbcog imaeq1d 1 8 11 10 vx vy cA cB cC csbcog imaeq2d eqtrd 3eqtr3d $.
$}

====

2018-10-05: ISSUE PA GUI Miscellaneous Bugs from today

    - mmj2 : Edit/Set Soft DJ Vars Error Handling = 2, Report is
             being processed exactly like 1, Ignore. There are
             supposed to be output error messages in the messages
             window. 

====
`