|
182 | 182 | character in a comment */
|
183 | 183 | /* 0.172 25-Jan-2019 nm mmwtex.c - comment out bug 2343 trap (not a bug) */
|
184 | 184 | /* 0.171 13-Dec-2018 nm metamath.c, mmcmdl.c, mmhlpa.c, mmcmds.c,h, mmwtex.c,h
|
185 |
| - - add fine-grained qualfiers to MARKUP command */ |
| 185 | + - add fine-grained qualifiers to MARKUP command */ |
186 | 186 | /* 0.170 12-Dec-2018 nm mmwtex.c - restore line accidentally deleted in 0.169 */
|
187 | 187 | /* 0.169 10-Dec-2018 nm metamath.c, mmcmds.c,h, mmcmdl.c, mmpars.c, mmhlpa.c,
|
188 | 188 | mmwtex.c - Add MARKUP command.
|
|
357 | 357 | 7-Mar-2016 nm mmwtex.c - added space between } and { in HTML output
|
358 | 358 | 6-Mar-2016 nm mmpars.c - disabled wrapping of formula lines in
|
359 | 359 | WRITE SOURCE.../REWRAP
|
360 |
| - 2-Mar-2016 nm metamat.c, mmcmdl.c, mmhlpb.c - added /FAST to |
| 360 | + 2-Mar-2016 nm metamath.c, mmcmdl.c, mmhlpb.c - added /FAST to |
361 | 361 | SAVE PROOF, SHOW PROOF */
|
362 | 362 | /* 0.123 25-Jan-2016 nm mmpars.c, mmdata.h, mmdata.c, mmpfas.c, mmcmds.,
|
363 | 363 | metamath.c, mmcmdl.c, mmwtex.c - unlocked SHOW PROOF.../PACKED,
|
|
413 | 413 | 3. Added blank lines before, after "---------Clip out the proof" proof
|
414 | 414 | 4. Generate date only if the proof is complete */
|
415 | 415 | /* 0.112 15-Apr-2015 nm metamath.c - fix bug 1121 (reported by S. O'Rear);
|
416 |
| - mwtex.c - add "img { margin-bottom: -4px }" to CSS to align symbol GIFs; |
417 |
| - mwtex.c - remove some hard coding for set.mm, for use with new nf.mm; |
| 416 | + mmwtex.c - add "img { margin-bottom: -4px }" to CSS to align symbol GIFs; |
| 417 | + mmwtex.c - remove some hard coding for set.mm, for use with new nf.mm; |
418 | 418 | metamath.c - fix comment parsing in WRITE BIBLIOGRAPHY to ignore
|
419 | 419 | math symbols */
|
420 | 420 | /* 0.111 22-Nov-2014 nm metamath.c, mmcmds.c, mmcmdl.c, mmhlpb.c - added
|
421 | 421 | /NO_NEW_AXIOMS_FROM qualifier to MINIMIZE_WITH; see HELP MINIMIZE_WITH.
|
422 |
| - 21-Nov-2014 Stepan O'Rear mmdata.c, mmhlpb.c - added ~ label range specifier |
| 422 | + 21-Nov-2014 Stefan O'Rear mmdata.c, mmhlpb.c - added ~ label range specifier |
423 | 423 | to wildcards; see HELP SEARCH */
|
424 | 424 | /* 0.110 2-Nov-2014 nm mmcmds.c - fixed bug 1114 (reported by Stefan O'Rear);
|
425 | 425 | metamath.c, mmhlpb.c - added "SHOW STATEMENT =" to show the statement
|
|
431 | 431 | /* 0.108 25-Jun-2014 nm
|
432 | 432 | (1) metamath.c, mmcmdl.c, mmhlpb.c - MINIMIZE_WITH now checks the size
|
433 | 433 | of the compressed proof, prevents $d violations, and tries forward and
|
434 |
| - reverse statment scanning order; /NO_DISTINCT, /BRIEF, /REVERSE |
| 434 | + reverse statement scanning order; /NO_DISTINCT, /BRIEF, /REVERSE |
435 | 435 | qualifiers were removed.
|
436 | 436 | (2) mminou.c - prevent hard breaks (in the middle of a word) in too-long
|
437 | 437 | lines (e.g. long URLs) in WRITE SOURCE .../REWRAP; just overflow the
|
|
463 | 463 | some cleanup */
|
464 | 464 | /* 0.07.99 1-Nov-2013 nm metamath.c, mmpfas.h,c, mmcmdl.h,c, mmhlpa.c,
|
465 | 465 | mmhlpb.c - added UNDO, REDO, SET UNDO commands (see HELP UNDO) */
|
466 |
| -/* 0.07.98 30-Oct-2013 Wolf Lammen mmvstr.c,h, mmiou.c, mmpars.c, |
| 466 | +/* 0.07.98 30-Oct-2013 Wolf Lammen mmvstr.c,h, mminou.c, mmpars.c, |
467 | 467 | mmdata.c - improve code style and program structure */
|
468 | 468 | /* 0.07.97 20-Oct-2013 Wolf Lammen mmvstr.c,h, metamath.c - improved linput();
|
469 | 469 | nm mmcmds.c, mmdata.c - tolerate bad proofs in SHOW TRACE_BACK etc. */
|
|
542 | 542 | /* 0.07.60 7-Jun-2011 nm mmpfas.c - fixed bug 1805 which occurred when doing
|
543 | 543 | MINIMIZE_WITH weq/ALLOW_GROWTH after DELETE DELETE FLOATING_HYPOTHESES */
|
544 | 544 | /* 0.07.59 11-Dec-2010 nm mmpfas.c - increased default SET SEARCH_LIMIT from
|
545 |
| - 10000 to 25000 to accomodate df-plig web page in set.mm */ |
| 545 | + 10000 to 25000 to accommodate df-plig web page in set.mm */ |
546 | 546 | /* 0.07.58 9-Dec-2010 nm mmpars.c - detect if same symbol is used with both
|
547 | 547 | $c and $v, in order to conform with Metamath spec */
|
548 | 548 | /* 0.07.57 19-Oct-2010 nm mmpars.c - fix bug causing incorrect line count
|
@@ -722,10 +722,10 @@ void command(int argc, char *argv[]);
|
722 | 722 |
|
723 | 723 | /*! \fn int main(int argc, char *argv[])
|
724 | 724 | * \brief entry point of the metamath program
|
725 |
| - * \param argc int number of commandline parameters |
726 |
| - * \param argv (char*)[] array of \a argc commandline parameters, followed by NULL |
| 725 | + * \param argc int number of command line parameters |
| 726 | + * \param argv (char*)[] array of \a argc command line parameters, followed by NULL |
727 | 727 | * \return success 0 else failure
|
728 |
| - * |
| 728 | + * |
729 | 729 | * Running metamath
|
730 | 730 | * ./metamath 'read set.mm' 'verify proof *'
|
731 | 731 | * will start main with \a argc set to 2, argv[0] to "read set.mm", argv[1]
|
@@ -824,7 +824,7 @@ void command(int argc, char *argv[]) {
|
824 | 824 | flag reverseFlag;
|
825 | 825 | long detailStep;
|
826 | 826 | flag noIndentFlag; /* Flag to use non-indented display */
|
827 |
| - long splitColumn; /* Column at which formula starts in nonindented display */ |
| 827 | + long splitColumn; /* Column at which formula starts in non-indented display */ |
828 | 828 | flag skipRepeatedSteps; /* NO_REPEATED_STEPS qualifier */
|
829 | 829 | flag texFlag; /* Flag for TeX */
|
830 | 830 | flag saveFlag; /* Flag to save in source */
|
@@ -1134,7 +1134,7 @@ void command(int argc, char *argv[]) {
|
1134 | 1134 | let(&str1, cat(str1, g_fullArg[i], " ", NULL));
|
1135 | 1135 | }
|
1136 | 1136 | }
|
1137 |
| - let(&str1, left(str1, (long)(strlen(str1)) - 1)); /* Trim trailing spc */ |
| 1137 | + let(&str1, left(str1, (long)(strlen(str1)) - 1)); /* Trim trailing space */ |
1138 | 1138 | if (g_toolsMode && g_listFile_fp != NULL) {
|
1139 | 1139 | /* Put line in list.tmp as command */
|
1140 | 1140 | fprintf(g_listFile_fp, "%s\n", str1); /* Print to list command file */
|
@@ -1302,7 +1302,7 @@ void command(int argc, char *argv[]) {
|
1302 | 1302 | if (!g_commandFilePtr[g_commandFileNestingLevel + 1]) continue;
|
1303 | 1303 | /* Couldn't open (err msg was provided) */
|
1304 | 1304 | g_commandFileNestingLevel++;
|
1305 |
| - g_commandFileName[g_commandFileNestingLevel] = ""; /* Initialize if nec. */ |
| 1305 | + g_commandFileName[g_commandFileNestingLevel] = ""; /* Initialize if necessary */ |
1306 | 1306 | let(&g_commandFileName[g_commandFileNestingLevel], g_fullArg[1]);
|
1307 | 1307 |
|
1308 | 1308 | g_commandFileSilent[g_commandFileNestingLevel] = 0;
|
@@ -1565,7 +1565,7 @@ void command(int argc, char *argv[]) {
|
1565 | 1565 | while (1) {
|
1566 | 1566 | p = instr(p + 1, str2, chr(((vstring)(g_fullArg[2]))[i]));
|
1567 | 1567 | if (!p) break;
|
1568 |
| - /* Put spaces arount special one-char tokens */ |
| 1568 | + /* Put spaces around special one-char tokens */ |
1569 | 1569 | let(&str2, cat(left(str2, p - 1), " ",
|
1570 | 1570 | mid(str2, p, 1),
|
1571 | 1571 | " ", right(str2, p + 1), NULL));
|
@@ -3216,7 +3216,7 @@ void command(int argc, char *argv[]) {
|
3216 | 3216 | }
|
3217 | 3217 |
|
3218 | 3218 | if (cmdMatches("SHOW MEMORY")) {
|
3219 |
| - j = 32000000; /* The largest we'ed ever look for */ |
| 3219 | + j = 32000000; /* The largest we'd ever look for */ |
3220 | 3220 | i = getFreeSpace(j);
|
3221 | 3221 | if (i > j-3) {
|
3222 | 3222 | print2("At least %ld bytes of memory are free.\n",j);
|
@@ -3693,7 +3693,7 @@ void command(int argc, char *argv[]) {
|
3693 | 3693 | if (!pipFlag) {
|
3694 | 3694 | parseProof(g_showStatement); /* Prints message if severe error */
|
3695 | 3695 | if (g_WrkProof.errorSeverity > 1) {
|
3696 |
| - /* Prevent bugtrap in nmbrSquishProof -> nmbrGetSubProofLen |
| 3696 | + /* Prevent bug trap in nmbrSquishProof -> nmbrGetSubProofLen |
3697 | 3697 | if proof corrupted */
|
3698 | 3698 | print2(
|
3699 | 3699 | "?The proof has a severe error and cannot be displayed or saved.\n");
|
@@ -3930,7 +3930,7 @@ void command(int argc, char *argv[]) {
|
3930 | 3930 | mode before starting its output, so we must put out the
|
3931 | 3931 | g_printString ourselves here */
|
3932 | 3932 | fprintf(g_texFilePtr, "%s", g_printString);
|
3933 |
| - free_vstring(g_printString); /* We'll clr it anyway */ |
| 3933 | + free_vstring(g_printString); /* We'll clear it anyway */ |
3934 | 3934 | } else { /* !texFlag */
|
3935 | 3935 | /* Terminal output - display the statement if wildcard is used */
|
3936 | 3936 | if (!pipFlag) {
|
@@ -4526,7 +4526,7 @@ void command(int argc, char *argv[]) {
|
4526 | 4526 | /* Automatically interact with user if step not unified */
|
4527 | 4527 | /* ???We might want to add a setting to defeat this if user doesn't
|
4528 | 4528 | like it */
|
4529 |
| - /* Since ASSIGN LAST is often run from a commmand file, don't |
| 4529 | + /* Since ASSIGN LAST is often run from a command file, don't |
4530 | 4530 | interact if / NO_UNIFY is specified, so response is predictable */
|
4531 | 4531 | if (switchPos("/ NO_UNIFY") == 0) {
|
4532 | 4532 | interactiveUnifyStep(s - m + n - 1, 2); /* 2nd arg. means print msg if
|
@@ -5412,7 +5412,7 @@ void command(int argc, char *argv[]) {
|
5412 | 5412 | g_Statement[g_proveStatement].proofSectionPtr = str1;
|
5413 | 5413 |
|
5414 | 5414 | g_outputToString = 1; /* Suppress error messages */
|
5415 |
| - /* parseProof, verifyProof, cleanWkrProof must be |
| 5415 | + /* parseProof, verifyProof, cleanWrkProof must be |
5416 | 5416 | called in sequence to assign the g_WrkProof structure, verify
|
5417 | 5417 | the proof, and deallocate the g_WrkProof structure. Either none
|
5418 | 5418 | of them or all of them must be called. */
|
|
0 commit comments