Skip to content

Commit

Permalink
Commit mm-0.154-2-Oct-2017
Browse files Browse the repository at this point in the history
  • Loading branch information
@nmegill @david-a-wheeler
nmegill authored and david-a-wheeler committed Feb 11, 2019
1 parent d7703ea commit fb281f5
Show file tree
Hide file tree
Showing 7 changed files with 97 additions and 39 deletions.
50 changes: 40 additions & 10 deletions metamath.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,10 @@
free of any copyright restrictions (i.e. public domain) in order to provide
this flexibility. Thank you. - NM */

#define MVERSION "0.153 1-Oct-2017"
#define MVERSION "0.154 2-Oct-2017"
/* 0.154 2-Oct-2017 nm mmunif.h,c mmcmds.c - add 2 more variables to ERASE;
metamath.c mmcmdl.c - remove obsolete OPEN/CLOSE HTML; mmhlpa.c mmhlpb.c -
fix typos reported by Benoit Jubin */
/* 0.153 1-Oct-2017 nm mmunif.c,h mmcmds.c - Re-initialize internal nmbrStrings
in unify() after 'erase' command reported by Benoit Jubin */
/* 0.152 26-Sep-2017 nm mmcmds.c - change default links from mpegif to mpeuni;
Expand Down Expand Up @@ -7167,7 +7170,7 @@ void command(int argc, char *argv[])
if (s < 3) s = 3; /* Less than 3 may cause a segmentation fault */
i = screenWidth;
screenWidth = s; /* 26-Sep-2017 nm - print with new screen width */
print2("Screen width has been changed from %ld to %ld\n",
print2("Screen width has been changed from %ld to %ld.\n",
i, s);
continue;
}
Expand All @@ -7176,11 +7179,12 @@ void command(int argc, char *argv[])
if (cmdMatches("SET HEIGHT")) { /* 18-Nov-05 nm Added */
s = (long)val(fullArg[2]); /* Screen height value */
if (s < 2) s = 2; /* Less than 2 makes no sense */
print2("Screen height has been changed from %ld to %ld\n",
screenHeight + 1, s);
i = screenHeight;
screenHeight = s - 1;
print2("Screen height has been changed from %ld to %ld.\n",
i + 1, s);
/* screenHeight is one less than the physical screen to account for the
prompt line after pausing. */
screenHeight = s - 1;
continue;
}

Expand Down Expand Up @@ -7272,25 +7276,33 @@ void command(int argc, char *argv[])
continue;
}

if (cmdMatches("OPEN TEX") || cmdMatches("OPEN HTML")) {
if (cmdMatches("OPEN TEX")) {
/* 2-Oct-2017 nm OPEN HTML is very obsolete, no need to warn anymore
if (cmdMatches("OPEN TEX") || cmdMatches("OPEN HTML") ) {
if (cmdMatches("OPEN HTML")) {
print2("?OPEN HTML is obsolete - use SHOW STATEMENT * / HTML\n");
continue;
}
*/

/* 17-Nov-2015 TODO: clean up mixed LaTeX/HTML attempts (check
texFileOpenFlag when switching to HTML & close LaTeX file) */

if (texDefsRead) {
/* Current limitation - can only read .def once */
if (cmdMatches("OPEN HTML") != htmlFlag) {
/* 2-Oct-2017 nm OPEN HTML is obsolete */
/*if (cmdMatches("OPEN HTML") != htmlFlag) {*/
if (htmlFlag) {
/* Actually it isn't clear to me this is still the case, but
to be safe I left it in */
print2("?You cannot use both LaTeX and HTML in the same session.\n");
print2(
"?You must EXIT and restart Metamath to switch to the other.\n");
continue;
}
}
htmlFlag = cmdMatches("OPEN HTML");
/* 2-Oct-2017 nm OPEN HTML is obsolete */
/*htmlFlag = cmdMatches("OPEN HTML");*/

/* Open a TeX file */
let(&texFileName,fullArg[2]);
Expand All @@ -7308,19 +7320,22 @@ void command(int argc, char *argv[])
texFilePtr = fSafeOpen(texFileName,"w");
if (!texFilePtr) continue; /* Couldn't open it (err msg was provided) */
texFileOpenFlag = 1;
/* 2-Oct-2017 nm OPEN HTML is obsolete */
print2("Created %s output file \"%s\".\n",
htmlFlag ? "HTML" : "LaTeX", texFileName);
printTexHeader(texHeaderFlag);
oldTexFlag = 0;
continue;
}

/* 2-Oct-2017 nm CLOSE HTML is obsolete */
/******
if (cmdMatches("CLOSE TEX") || cmdMatches("CLOSE HTML")) {
if (cmdMatches("CLOSE HTML")) {
print2("?CLOSE HTML is obsolete - use SHOW STATEMENT * / HTML\n");
print2("?CLOSE HTML is obsolete - use SHOW STATEMENT @ / HTML\n");
continue;
}
/* Close the TeX file */
/@ Close the TeX file @/
if (!texFileOpenFlag) {
print2("?Sorry, there is no %s file currently open.\n",
htmlFlag ? "HTML" : "LaTeX");
Expand All @@ -7334,6 +7349,21 @@ void command(int argc, char *argv[])
let(&texFileName,"");
continue;
}
*****/
if (cmdMatches("CLOSE TEX")) {
/* Close the TeX file */
if (!texFileOpenFlag) {
print2("?Sorry, there is no LaTeX file currently open.\n");
} else {
print2("The LaTeX output file \"%s\" has been closed.\n",
texFileName);
printTexTrailer(texHeaderFlag);
fclose(texFilePtr);
texFileOpenFlag = 0;
}
let(&texFileName,"");
continue;
}

/* Similar to Unix 'more' */
if (cmdMatches("MORE")) {
Expand Down
32 changes: 23 additions & 9 deletions mmcmdl.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,20 @@ flag processCommandLine(void)
"ASSIGN|REPLACE|MATCH|UNIFY|LET|INITIALIZE|DELETE|IMPROVE|",
/* 11-Sep-2016 nm Added EXPAND */
"MINIMIZE_WITH|EXPAND|UNDO|REDO|SAVE|DEMO|INVOKE|CLI|EXPLORE|TEX|",
"LATEX|HTML|COMMENTS|MORE|",
/*"LATEX|HTML|COMMENTS|MORE|",*/
/* 2-Oct-2017 nm Removed HTML */
"LATEX|COMMENTS|MORE|",
"TOOLS|MIDI|$|<$>", NULL))) goto pclbad;
if (cmdMatches("HELP OPEN")) {
if (!getFullArg(2, "LOG|TEX|HTML|<LOG>")) goto pclbad;
/*if (!getFullArg(2, "LOG|TEX|HTML|<LOG>")) goto pclbad;*/
/* 2-Oct-2017 nm Removed HTML */
if (!getFullArg(2, "LOG|TEX|<LOG>")) goto pclbad;
goto pclgood;
}
if (cmdMatches("HELP CLOSE")) {
if (!getFullArg(2, "LOG|TEX|HTML|<LOG>")) goto pclbad;
/*if (!getFullArg(2, "LOG|TEX|HTML|<LOG>")) goto pclbad;*/
/* 2-Oct-2017 nm Removed HTML */
if (!getFullArg(2, "LOG|TEX|<LOG>")) goto pclbad;
goto pclgood;
}
if (cmdMatches("HELP SHOW")) {
Expand Down Expand Up @@ -270,7 +276,9 @@ flag processCommandLine(void)
}

if (cmdMatches("OPEN")) {
if (!getFullArg(1,"LOG|TEX|HTML|<LOG>")) goto pclbad;
/*if (!getFullArg(1,"LOG|TEX|HTML|<LOG>")) goto pclbad;*/
/* 2-Oct-2017 nm Removed HTML */
if (!getFullArg(1,"LOG|TEX|<LOG>")) goto pclbad;
if (cmdMatches("OPEN LOG")) {
if (logFileOpenFlag) {
printLongLine(cat(
Expand Down Expand Up @@ -315,6 +323,9 @@ flag processCommandLine(void)
} /* End while for switch loop */

}

/* 2-Oct-2017 nm OPEN HTML is obsolete */
/*******
if (cmdMatches("OPEN HTML")) {
if (texFileOpenFlag) {
printLongLine(cat(
Expand All @@ -324,10 +335,10 @@ flag processCommandLine(void)
,NULL), "", " ");
goto pclbad;
}
if (!getFullArg(2,"* What is the name of HTML output file? "))
if (!getFullArg(2,"@ What is the name of HTML output file? "))
goto pclbad;
/* Get any switches */
/@ Get any switches @/
i = 2;
while (1) {
i++;
Expand All @@ -340,15 +351,18 @@ flag processCommandLine(void)
} else {
break;
}
break; /* Break if only 1 switch is allowed */
} /* End while for switch loop */
break; /@ Break if only 1 switch is allowed @/
} /@ End while for switch loop @/
}
****/
goto pclgood;
}

if (cmdMatches("CLOSE")) {
if (!getFullArg(1,"LOG|TEX|HTML|<LOG>")) goto pclbad;
/*if (!getFullArg(1,"LOG|TEX|HTML|<LOG>")) goto pclbad;*/
/* 2-Oct-2017 nm Removed HTML */
if (!getFullArg(1,"LOG|TEX|<LOG>")) goto pclbad;
goto pclgood;
}

Expand Down
8 changes: 7 additions & 1 deletion mmcmds.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4127,12 +4127,18 @@ void eraseSource(void) /* ERASE command */
/* Allocate big arrays */
initBigArrays();

/* 2-Oct-2017 nm Future possibilty: add 'reset' parameter to unify() to clear
the 5 variables below */
bracketMatchInit = 0; /* Clear to force mmunif.c to scan $a's again */
minSubstLen = 1; /* Initialize to the default SET EMPTY_SUBSTITUTION OFF */
/* 1-Oct-2017 Fix 'erase' bug found by Benoit Judin */
/* 1-Oct-2017 nm Fix 'erase' bug found by Benoit Jubin */
/* Clear firstConst to trigger clearing of lastConst and
oneConst in mmunif.c */
nmbrLet(&firstConst, NULL_NMBRSTRING);
/* 2-Oct-2017 nm Clear these directly so they will be truly deallocated
for valgrind */
nmbrLet(&lastConst, NULL_NMBRSTRING);
nmbrLet(&oneConst, NULL_NMBRSTRING);

/* 3-May-2016 nm */
getMarkupFlag(0, RESET); /* Erase the cached markup flag storage */
Expand Down
15 changes: 8 additions & 7 deletions mmhlpa.c
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*****************************************************************************/
/* Copyright (C) 2016 NORMAN MEGILL nm at alum.mit.edu */
/* Copyright (C) 2017 NORMAN MEGILL nm at alum.mit.edu */
/* License terms: GNU General Public License */
/*****************************************************************************/
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
Expand Down Expand Up @@ -540,8 +540,8 @@ H("");
H(" The substitution of symbol strings into variables may be subject to a");
H(" $d restriction:");
H("");
H(" $d - Disjoint variable restriction (meaning substititutions may not");
H(" share variables in common)");
H(" $d - Disjoint variable restriction (meaning substitutions may not");
H(" have variables in common)");
H(" Syntax: \"$d <symbol> ... <symbol> $.\" where <symbol> is active");
H(" and previously declared with $v, and all <symbol>s are distinct");
H("");
Expand Down Expand Up @@ -668,7 +668,7 @@ H(" ...");
H(" htmldef \"<mathtoken>\" as \"<HTML code for mathtoken symbol>\" ;");
H(" htmltitle \"<HTML code for title>\" ;");
H(" htmlhome \"<HTML code for home link>\" ;");
H(" htmlvarcolors \"<HTML code for variable color list>\" ;");
H(" htmlvarcolor \"<HTML code for variable color list>\" ;");
H(" htmlbibliography \"<HTML file>\" ;");
H(" (This <HTML file> is assumed to have a <A NAME=...> tag for each");
H(" bibiographic reference in the database comments. For example");
Expand Down Expand Up @@ -828,7 +828,8 @@ printHelp = !strcmp(saveHelpCmd, "HELP ERASE");
H("Syntax: ERASE");
H("");
H("This command will reset Metamath to its starting state, deleting any");
H("database that was READ in.");
H("database that was READ in. It does not reset parameters unrelated to the");
H("database i.e. those listed in SHOW SETTINGS.");
H("");


Expand Down Expand Up @@ -894,8 +895,8 @@ printHelp = !strcmp(saveHelpCmd, "HELP TOOLS");
H("Syntax: TOOLS");
H("");
H("This command invokes a utility to manipulate ASCII text files. Type TOOLS");
H("to enter this utility, which has its own HELP commands. Once inside you");
H("are inside, EXIT will return to Metamath.");
H("to enter this utility, which has its own HELP commands. Once you are");
H("inside, EXIT will return to Metamath.");
H("");

let(&saveHelpCmd, ""); /* Deallocate memory */
Expand Down
25 changes: 14 additions & 11 deletions mmhlpb.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW MEMORY");
H("Syntax: SHOW MEMORY");
H("");
H("This command shows the available memory left. It is not be meaningful");
H("This command shows the available memory left. It is not meaningful");
H("on modern machines with virtual memory.");
H("");

Expand Down Expand Up @@ -635,15 +635,18 @@ H("");


printHelp = !strcmp(saveHelpCmd, "HELP VERIFY MARKUP");
H("Syntax: VERIFY MARKUP <label-match> [/ DATE_SKIP] [/ FILE_SKIP]");
H("");
H("This command error-checks the latexdef, htmldef, and althtmldef statements");
H("in the $t statement of a Metamath source file. It also error-checks any");
H("`...`, ~ <label>, and [bibref] markups in statement descriptions.");
H("Finally, it verifies the date consistency of \"(Contributed by...)\",");
H("Syntax: VERIFY MARKUP <label-match> [/ DATE_SKIP] [/ FILE_SKIP] [/VERBOSE]");
H("");
H("This command checks comment markup and other informal conventions we have");
H("adopted. It error-checks the latexdef, htmldef, and althtmldef statements");
H("in the $t statement of a Metamath source file. It error-checks any `...`,");
H("~ <label>, and [bibref] markups in statement descriptions. It checks that");
H("$p and $a statements have the same content when their labels start with");
H("\"ax\" and \"ax-\" respectively but are otherwise identical, for example");
H("ax4 and ax-4. It verifies the date consistency of \"(Contributed by...)\",");
H("\"(Revised by...)\", and \"(Proof shortened by...)\", tags in the comment");
H("above each $a and $p statement. See HELP SEARCH for <label-match> rules.");
H("");
H("See HELP LANGUAGE, HELP HTML, and HELP SET DISCOURAGEMENT for markup syntax.");
H("Optional qualifiers:");
H(" / DATE_SKIP - This qualifier will skip date consistency checking,");
H(" which is usually not required for databases other than set.mm");
Expand Down Expand Up @@ -1047,14 +1050,14 @@ H("current subproof ending at <step> with a new complete subproof (if one");
H("can be found) ending with statement <label>. The replacement will be");
H("done only if complete subproofs can be found that match all of the");
H("hypotheses of <label>. REPLACE is equivalent to IMPROVE with the");
H("qualifiers / 3 / DEPTH 1 / SUBPROOF (see HELP IMPROVE), except that");
H("qualifiers / 3 / DEPTH 1 / SUBPROOFS (see HELP IMPROVE), except that");
H("it considers only statement <label> rather than scanning all preceding");
H("statements in the database, and it does somewhat more aggressive");
H("guessing of assignments to work ($nn) variables.");
H("");
H("REPLACE will also assign a complete subproof to a currently unknown");
H("(unassigned) step if a complete subproof can be found. In many cases,");
H("REPLACE provide an alternative to ASSIGN (with the same command syntax)");
H("REPLACE provides an alternative to ASSIGN (with the same command syntax)");
H("that will fill in more missing steps when it is successful. It is often");
H("useful to try REPLACE first and, if not successful, revert to ASSIGN.");
H("Note that REPLACE may take a long time to run compared to ASSIGN.");
Expand Down Expand Up @@ -1473,7 +1476,7 @@ H("");
H("Important note: The / PACKED and / EXPLICIT qualifiers save the proof");
H("in formats that are _not_ part of the Metamath standard and that probably");
H("will not be recognized by other Metamath proof verifiers. They are");
H("primarily intended to assist database maintainence. For example,");
H("primarily intended to assist database maintenance. For example,");
H(" SAVE PROOF * / EXPLICIT / PACKED / FAST");
H("will allow the order of $e and $f hypotheses to be changed without");
H("affecting any proofs.");
Expand Down
3 changes: 2 additions & 1 deletion mmunif.c
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/*****************************************************************************/
/* Copyright (C) 2012 NORMAN MEGILL nm at alum.mit.edu */
/* Copyright (C) 2017 NORMAN MEGILL nm at alum.mit.edu */
/* License terms: GNU General Public License */
/*****************************************************************************/
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
Expand Down Expand Up @@ -149,6 +149,7 @@ int nestingLevel = 0;

/* 8/29/99 For improving rejection of impossible substitutions */
/* 1-Oct-2017 nm Made firstConst global so eraseSource() can clear it */
/* 2-Oct-2017 nm Made them all global so valgrind won't complain */
nmbrString *firstConst = NULL_NMBRSTRING;
nmbrString *lastConst = NULL_NMBRSTRING;
nmbrString *oneConst = NULL_NMBRSTRING;
Expand Down
3 changes: 3 additions & 0 deletions mmunif.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,9 @@ extern flag bracketMatchInit; /* So eraseSource() (mmcmds.c) can clr it */

/* 1-Oct-2017 nm Made this global so eraseSource() (mmcmds.c) can clr it */
extern nmbrString *firstConst;
/* 2-Oct-2017 nm Made these global so eraseSource() (mmcmds.c) can clr themt */
extern nmbrString *lastConst;
extern nmbrString *oneConst;


nmbrString *makeSubstUnif(flag *newVarFlag,
Expand Down

0 comments on commit fb281f5

Please sign in to comment.