Skip to content

Commit

Permalink
Merge branch 'develop'
Browse files Browse the repository at this point in the history
  • Loading branch information
@digama0
digama0 committed May 11, 2017
2 parents 00c0d91 + 520bbc6 commit 065abfb
Show file tree
Hide file tree
Showing 8 changed files with 41 additions and 49 deletions.
10 changes: 5 additions & 5 deletions doc/javadoc/constant-values.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1515,7 +1515,7 @@ <h2 title="mmj.pa">mmj.pa.*</h2>
<!-- -->
</a><code>public&nbsp;static&nbsp;final&nbsp;java.lang.String</code></td>
<td><code><a href="mmj/pa/PaConstants.html#GENERAL_HELP_FRAME_TITLE">GENERAL_HELP_FRAME_TITLE</a></code></td>
<td class="colLast"><code>"Proof Assistant Help: General Information, Version 2.5.1 as of 29-Dec-2016"</code></td>
<td class="colLast"><code>"Proof Assistant Help: General Information, Version 2.5.2 as of 10-May-2017"</code></td>
</tr>
<tr class="altColor">
<td class="colFirst"><a name="mmj.pa.PaConstants.GENERAL_HELP_INFO_TEXT">
Expand Down Expand Up @@ -1613,7 +1613,7 @@ <h2 title="mmj.pa">mmj.pa.*</h2>
<!-- -->
</a><code>public&nbsp;static&nbsp;final&nbsp;java.lang.String</code></td>
<td><code><a href="mmj/pa/PaConstants.html#HELP_ABOUT_TEXT">HELP_ABOUT_TEXT</a></code></td>
<td class="colLast"><code>"mmj2 Version 2.5.1 as of 29-Dec-2016.\n\nCopyright (C) 2005 thru 2011 MEL O\'CAT via X178G243 (at) yahoo (dot) com \nLicense terms: GNU General Public License Version 2 or any later version.\n\nNote: The following copyright is included because ProofAsstGUI.java\nhas several snippets of code that are very similar, if not identical\nto snippets of code in the Java Tutorial.\n\nCopyright\u00a9 1995-2004 Sun Microsystems, Inc. All Rights Reserved.\nRedistribution and use in source and binary forms, with or without\nmodification, are permitted provided that the following conditions are\nmet\n* Redistribution of source code must retain the above copyright\n notice, this list of conditions and the following disclaimer.\n* Redistribution in binary form must reproduce the above copyright\n notice, this list of conditions and the following disclaimer in the\n documentation and/or other materials provided with the distribution.\n(See SunJavaTutorialLicense.html in the mmj2 distribution for the\nfor the disclaimer.)\n\nGarbage Collection Run (just now) Memory Totals follow:\n Max Memory = %s\n Free Memory = %s\n Total Memory = %s\n"</code></td>
<td class="colLast"><code>"mmj2 Version 2.5.2 as of 10-May-2017.\n\nCopyright (C) 2005 thru 2011 MEL O\'CAT via X178G243 (at) yahoo (dot) com \nLicense terms: GNU General Public License Version 2 or any later version.\n\nNote: The following copyright is included because ProofAsstGUI.java\nhas several snippets of code that are very similar, if not identical\nto snippets of code in the Java Tutorial.\n\nCopyright\u00a9 1995-2004 Sun Microsystems, Inc. All Rights Reserved.\nRedistribution and use in source and binary forms, with or without\nmodification, are permitted provided that the following conditions are\nmet\n* Redistribution of source code must retain the above copyright\n notice, this list of conditions and the following disclaimer.\n* Redistribution in binary form must reproduce the above copyright\n notice, this list of conditions and the following disclaimer in the\n documentation and/or other materials provided with the distribution.\n(See SunJavaTutorialLicense.html in the mmj2 distribution for the\nfor the disclaimer.)\n\nGarbage Collection Run (just now) Memory Totals follow:\n Max Memory = %s\n Free Memory = %s\n Total Memory = %s\n"</code></td>
</tr>
<tr class="altColor">
<td class="colFirst"><a name="mmj.pa.PaConstants.HELP_ABOUT_TITLE">
Expand Down Expand Up @@ -2530,7 +2530,7 @@ <h2 title="mmj.pa">mmj.pa.*</h2>
<!-- -->
</a><code>public&nbsp;static&nbsp;final&nbsp;java.lang.String</code></td>
<td><code><a href="mmj/pa/PaConstants.html#PROOF_ASST_GUI_STARTUP_MSG">PROOF_ASST_GUI_STARTUP_MSG</a></code></td>
<td class="colLast"><code>"Hi! I am mmj2 v2.5.1 as of 29-Dec-2016.\nVisit https://github.com/digama0/mmj2/ or\nhttp://code.google.com/p/metamath-mmj2/\nfor support or bug reports."</code></td>
<td class="colLast"><code>"Hi! I am mmj2 v2.5.2 as of 10-May-2017.\nVisit https://github.com/digama0/mmj2/ or\nhttp://code.google.com/p/metamath-mmj2/\nfor support or bug reports."</code></td>
</tr>
<tr class="rowColor">
<td class="colFirst"><a name="mmj.pa.PaConstants.PROOF_ASST_IMPORT_COMPARE_DJS_DEFAULT">
Expand Down Expand Up @@ -3153,14 +3153,14 @@ <h2 title="mmj.pa">mmj.pa.*</h2>
<!-- -->
</a><code>public&nbsp;static&nbsp;final&nbsp;java.lang.String</code></td>
<td><code><a href="mmj/pa/PaConstants.html#VERSION">VERSION</a></code></td>
<td class="colLast"><code>"2.5.1"</code></td>
<td class="colLast"><code>"2.5.2"</code></td>
</tr>
<tr class="altColor">
<td class="colFirst"><a name="mmj.pa.PaConstants.VERSION_DATE">
<!-- -->
</a><code>public&nbsp;static&nbsp;final&nbsp;java.lang.String</code></td>
<td><code><a href="mmj/pa/PaConstants.html#VERSION_DATE">VERSION_DATE</a></code></td>
<td class="colLast"><code>"29-Dec-2016"</code></td>
<td class="colLast"><code>"10-May-2017"</code></td>
</tr>
</tbody>
</table>
Expand Down
2 changes: 1 addition & 1 deletion mmj2jar/macros/definitionCheck.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,7 @@ function setMMDefinitionsCheck(axiom)
field += v + " ";
field += PaConstants.END_PROOF_STMT_TOKEN;
}
if (!field.isEmpty()) {
if (field.length() != 0) {
messages.accumInfoMessage(ERRMSG_PA_DEFINITION_FAIL_4,
axiom.label, field);
success = false;
Expand Down
2 changes: 1 addition & 1 deletion mmj2jar/macros/showDiscouraged.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ for each (var s in stmts) {
lines.add('Proof modification of "'+s.label+'" is discouraged ('+s.proof.length+' steps).');
useListTemp.clear();
for each (var rpn in s.proof)
if (rpn.stmt && useDisc.containsKey(rpn.stmt))
if (rpn && rpn.stmt && useDisc.containsKey(rpn.stmt))
useListTemp.add(rpn.stmt);
for each (var used in useListTemp)
useDisc.get(used).add(s);
Expand Down
2 changes: 1 addition & 1 deletion mmj2jar/macros/transformations.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ var badAssrtList = [
"fh1i fh3i hl0lt1",

"jaao anim12ii anim12i im2anan9r anim12dan rcla4dv impbid21d r19.21bi anim12ci",
"rcla4edv"
"rcla4edv bi2anan9r ineqan12d 3anassrs wunfv wunop evlfcl"
].join(" ").split(" ");

for each (var s in badAssrtList)
Expand Down
Binary file modified mmj2jar/mmj2.jar
View file
Binary file not shown.
7 changes: 3 additions & 4 deletions src/mmj/pa/DerivationStep.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -362,10 +362,9 @@ public boolean hasWorkVarsInStepOrItsHyps() {
*/
@Override
public boolean stmtIsIncomplete() {
if (isHypFldIncomplete() || formulaFldIncomplete
|| formulaParseTree == null)
return true;
return false;
return isHypFldIncomplete() || formulaFldIncomplete
|| formulaParseTree == null
|| getRef() == null && getLocalRef() == null;
}

@Override
Expand Down
4 changes: 2 additions & 2 deletions src/mmj/pa/PaConstants.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -171,10 +171,10 @@
public class PaConstants {

/** Version number string. */
public static final String VERSION = "2.5.1";
public static final String VERSION = "2.5.2";

/** Date for latest version. */
public static final String VERSION_DATE = "29-Dec-2016";
public static final String VERSION_DATE = "10-May-2017";

public static final String SYNONYM_TRUE_1 = "true";
public static final String SYNONYM_TRUE_2 = "on";
Expand Down
63 changes: 28 additions & 35 deletions src/mmj/tl/TheoremStmtGroup.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,7 @@ public void initializeMustAppend() {
public void validateTheoremSrcStmtProofLabels(
final LogicalSystem logicalSystem,
final Map<String, TheoremStmtGroup> theoremStmtGroupTbl)
throws TheoremLoaderException
throws TheoremLoaderException
{

final Map<String, Stmt> stmtTbl = logicalSystem.getStmtTbl();
Expand Down Expand Up @@ -195,7 +195,7 @@ public void validateTheoremSrcStmtProofLabels(

if (!getIsTheoremNew() &&

maxExistingMObjRef.getSeq() >= theorem.getSeq())
maxExistingMObjRef.getSeq() >= theorem.getSeq())
throw new TheoremLoaderException(
TlConstants.ERRMSG_PROOF_LABEL_SEQ_TOO_HIGH,
theoremLabel, theorem.getSeq(), ref.getLabel(),
Expand Down Expand Up @@ -247,7 +247,7 @@ public void queueForUpdates(final Queue<TheoremStmtGroup> readyQueue,
public void queueDependentsForUpdate(
final Deque<TheoremStmtGroup> readyQueue,
final List<TheoremStmtGroup> waitingList)
throws TheoremLoaderException
throws TheoremLoaderException
{
for (final TheoremStmtGroup g : usedByTheoremStmtGroupList)
g.reQueueAfterUsedTheoremUpdated(this, readyQueue, waitingList);
Expand Down Expand Up @@ -277,7 +277,7 @@ public void queueDependentsForUpdate(
*/
public void updateLogicalSystem(final LogicalSystem logicalSystem,
final Messages messages, final TlPreferences tlPreferences)
throws TheoremLoaderException, LangException
throws TheoremLoaderException, LangException
{
if (getIsTheoremNew())
addTheoremToLogicalSystem(logicalSystem, messages, tlPreferences);
Expand Down Expand Up @@ -509,9 +509,7 @@ public int compare(final TheoremStmtGroup o1,
- o2.theorem.getLogHypArrayLength();

if (n == 0)
n =

o1.theorem.getSeq() - o2.theorem.getSeq();
n = o1.theorem.getSeq() - o2.theorem.getSeq();

return n;
}
Expand All @@ -527,7 +525,7 @@ private void reQueueAfterUsedTheoremUpdated(
final TheoremStmtGroup usedTheoremStmtGroup,
final Deque<TheoremStmtGroup> readyQueue,
final List<TheoremStmtGroup> waitingList)
throws TheoremLoaderException
throws TheoremLoaderException
{

updateMaxExistingMObjRef(usedTheoremStmtGroup.theorem);
Expand Down Expand Up @@ -679,7 +677,11 @@ private void loadParsedInputIntoStmtGroup() throws TheoremLoaderException {
}

private boolean isLabelInLogHypList(final String label) {
return logHypSrcStmtList.contains(label);
for (final SrcStmt s : logHypSrcStmtList)
if (s.label.equals(label))
return true;

return false;
}

/**
Expand All @@ -694,7 +696,7 @@ private boolean isLabelInLogHypList(final String label) {
*/
private void validateStmtGroupData(final LogicalSystem logicalSystem,
final Messages messages, final TlPreferences tlPreferences)
throws TheoremLoaderException
throws TheoremLoaderException
{

final Map<String, Sym> symTbl = logicalSystem.getSymTbl();
Expand All @@ -713,14 +715,23 @@ private void validateStmtGroupData(final LogicalSystem logicalSystem,
private void validateDvSrcStmt(final SrcStmt dvSrcStmt,
final Map<String, Sym> symTbl) throws TheoremLoaderException
{

checkVarMObjRef(dvSrcStmt, symTbl);
for (final String s : dvSrcStmt.symList) {
final Sym sym = symTbl.get(s);
if (sym == null)
generateSymNotFndError(dvSrcStmt, s);
else
updateMaxExistingMObjRef(sym);
if (!(sym instanceof Var))
throw new TheoremLoaderException(
TlConstants.ERRMSG_DJ_VAR_SYM_NOT_A_VAR, s, dvSrcStmt.seq,
mmtTheoremFile.getSourceFileName());
}
}

private void validateLogHypSrcStmt(final TlPreferences tlPreferences,
final SrcStmt logHypSrcStmt, final Map<String, Sym> symTbl,
final Map<String, Stmt> stmtTbl, final int logHypIndex)
throws TheoremLoaderException
throws TheoremLoaderException
{

checkSymMObjRef(logHypSrcStmt, symTbl);
Expand Down Expand Up @@ -748,7 +759,7 @@ private void validateLogHypSrcStmt(final TlPreferences tlPreferences,

private void validateTheoremSrcStmt(final TlPreferences tlPreferences,
final Map<String, Sym> symTbl, final Map<String, Stmt> stmtTbl)
throws TheoremLoaderException
throws TheoremLoaderException
{

checkSymMObjRef(theoremSrcStmt, symTbl);
Expand Down Expand Up @@ -845,25 +856,9 @@ private void checkSymMObjRef(final SrcStmt x, final Map<String, Sym> symTbl)
}
}

private void checkVarMObjRef(final SrcStmt x, final Map<String, Sym> symTbl)
throws TheoremLoaderException
{
for (final String s : x.symList) {
final Sym sym = symTbl.get(s);
if (sym == null)
generateSymNotFndError(x, s);
else
updateMaxExistingMObjRef(sym);
if (!(sym instanceof Var))
throw new TheoremLoaderException(
TlConstants.ERRMSG_DJ_VAR_SYM_NOT_A_VAR, s, x.seq,
mmtTheoremFile.getSourceFileName());
}
}
private void generateSymNotFndError(final SrcStmt x, final String id)
throws TheoremLoaderException
{

throw new TheoremLoaderException(TlConstants.ERRMSG_SRC_STMT_SYM_NOTFND,
id, x.seq, mmtTheoremFile.getSourceFileName());
}
Expand All @@ -876,17 +871,15 @@ private void generateSymNotFndError(final SrcStmt x, final String id)

private void updateTheoremInLogicalSystem(final LogicalSystem logicalSystem,
final Messages messages, final TlPreferences tlPreferences)
throws TheoremLoaderException, LangException
throws TheoremLoaderException, LangException
{

wasTheoremUpdated = true;

theorem.setProof(logicalSystem.getStmtTbl(), theoremSrcStmt.proofList);

final DjVarsOption djVarsOption = tlPreferences.djVarsOption.get();
if (djVarsOption == DjVarsOption.NoUpdate) {}
else {

if (djVarsOption != DjVarsOption.NoUpdate) {
final List<DjVars> mandDjVarsUpdateList = new LinkedList<>();
final List<DjVars> optDjVarsUpdateList = new LinkedList<>();
buildMandAndOptDjVarsUpdateLists(logicalSystem.getSymTbl(),
Expand All @@ -906,7 +899,7 @@ else if (djVarsOption == DjVarsOption.Replace)

private void addTheoremToLogicalSystem(final LogicalSystem logicalSystem,
final Messages messages, final TlPreferences tlPreferences)
throws TheoremLoaderException, LangException
throws TheoremLoaderException, LangException
{

SrcStmt currSrcStmt;
Expand Down

0 comments on commit 065abfb

Please sign in to comment.