diff --git a/src/metamath.c b/src/metamath.c index 021294de..cb2199b2 100644 --- a/src/metamath.c +++ b/src/metamath.c @@ -5,58 +5,56 @@ /*****************************************************************************/ /*34567890123456 (79-character line to adjust editor window) 2345678901234567*/ -/* Copyright notice: All code in this program that was written by Norman - Megill is public domain. However, the project includes code contributions - from other people which may be GPL licensed. For more details see: - https://github.com/metamath/metamath-exe/issues/7#issuecomment-675555069 */ +// Copyright notice: All code in this program that was written by Norman +// Megill is public domain. However, the project includes code contributions +// from other people which may be GPL licensed. For more details see: +// https://github.com/metamath/metamath-exe/issues/7#issuecomment-675555069 /*! \file * Contains main(), the starting point of metamath; executes or calls commands */ -/* The overall functionality of the modules is as follows: - metamath.c - Contains main(); executes or calls commands - mmcmdl.c - Command line interpreter - mmcmds.c - Extends metamath.c command() to execute SHOW and other - commands; added after command() became too bloated (still is:) - mmdata.c - Defines global data structures and manipulates arrays - with functions similar to BASIC string functions; - memory management; converts between proof formats - mmfatl.c - Fatal error handler - mmhlpa.c - The help file, part 1. - mmhlpb.c - The help file, part 2. - mminou.c - Basic input and output interface - mmpars.c - Parses the source file - mmpfas.c - Proof Assistant - mmunif.c - Unification algorithm for Proof Assistant - mmveri.c - Proof verifier for source file - mmvstr.c - BASIC-like string functions - mmwtex.c - LaTeX/HTML source generation - mmword.c - File revision utility (for TOOLS> UPDATE) (not generally useful) -*/ - -/* Compilation instructions (gcc on Unix/Linus/Cygwin, lcc on Windows): - 1. Make sure each .c file above is present in the compilation directory and - that each .c file (except metamath.c) has its corresponding .h file - present. - 2. In the directory where these files are present, type: - gcc m*.c -o metamath - 3. For full error checking, use: - gcc m*.c -o metamath -O2 -Wall -Wextra -Wmissing-prototypes \ +// The overall functionality of the modules is as follows: +// metamath.c - Contains main(); executes or calls commands +// mmcmdl.c - Command line interpreter +// mmcmds.c - Extends metamath.c command() to execute SHOW and other +// commands; added after command() became too bloated (still is:) +// mmdata.c - Defines global data structures and manipulates arrays +// with functions similar to BASIC string functions; +// memory management; converts between proof formats +// mmfatl.c - Fatal error handler +// mmhlpa.c - The help file, part 1. +// mmhlpb.c - The help file, part 2. +// mminou.c - Basic input and output interface +// mmpars.c - Parses the source file +// mmpfas.c - Proof Assistant +// mmunif.c - Unification algorithm for Proof Assistant +// mmveri.c - Proof verifier for source file +// mmvstr.c - BASIC-like string functions +// mmwtex.c - LaTeX/HTML source generation +// mmword.c - File revision utility (for TOOLS> UPDATE) (not generally useful) + +// Compilation instructions (gcc on Unix/Linus/Cygwin, lcc on Windows): +// 1. Make sure each .c file above is present in the compilation directory and +// that each .c file (except metamath.c) has its corresponding .h file +// present. +// 2. In the directory where these files are present, type: +// gcc m*.c -o metamath +// 3. For full error checking, use: +/* gcc m*.c -o metamath -O2 -Wall -Wextra -Wmissing-prototypes \ -Wmissing-declarations -Wshadow -Wpointer-arith -Wcast-align \ -Wredundant-decls -Wnested-externs -Winline -Wno-long-long \ - -Wconversion -Wstrict-prototypes -std=c99 -pedantic -Wunused-result - Note: gcc 4.9.2 (on Debian) fails with "unknown type name `ssize_t'" if - -std=c99 is used, so omit -std=c99 to work around this problem. - 4. For faster runtime, use these gcc options: - gcc m*.c -o metamath -O3 -funroll-loops -finline-functions \ - -fomit-frame-pointer -Wall -std=c99 -pedantic -fno-strict-overflow - 5. The Windows version in the download was compiled with lcc-win32 version 3.8: - lc -O m*.c -o metamath.exe - 6. On Linux, if you have autoconf, automake, and a C compiler, you - can compile with the command "autoreconf -i && ./configure && make". - See the README.TXT file for more information. -*/ + -Wconversion -Wstrict-prototypes -std=c99 -pedantic -Wunused-result */ +// Note: gcc 4.9.2 (on Debian) fails with "unknown type name `ssize_t'" if +// -std=c99 is used, so omit -std=c99 to work around this problem. +// 4. For faster runtime, use these gcc options: +/* gcc m*.c -o metamath -O3 -funroll-loops -finline-functions \ + -fomit-frame-pointer -Wall -std=c99 -pedantic -fno-strict-overflow */ +// 5. The Windows version in the download was compiled with lcc-win32 version 3.8: +// lc -O m*.c -o metamath.exe +// 6. On Linux, if you have autoconf, automake, and a C compiler, you +// can compile with the command "autoreconf -i && ./configure && make". +// See the README.TXT file for more information. /*! \def MVERSION * The current version of metamath. It is incremented each time the software @@ -74,633 +72,628 @@ * - the length is limited to 26 characters. */ #define MVERSION "0.199.pre 29-Jan-2022" -/* 0.199.pre - 30-Dec-2021 mc metamath.c mmdata.c mminou.c mmmaci.c - - Remove mmmaci and everything related to THINK_C compiler - 4-Jan-2022 mc - change VERIFY MARKUP /TOP_DATE_SKIP and /FILE_SKIP to - /TOP_DATE_CHECK and /FILE_CHECK (with opposite meaning), and make the - skip behavior the default. - 7-Sep-2022 bj mmwtex.c, mmhlpa.c Added CRITERIA CRITERION to [bib] - keywords */ -/* 0.198 nm 7-Aug-2021 mmpars.c - Fix cosmetic bug in WRITE SOURCE ... /REWRAP - that prevented end of sentence (e.g. period) from appearing in column 79, - thus causing some lines to be shorter than necessary. */ -/* 0.197 nm 2-Aug-2021 mmpars.c - put two spaces between $c,v on same line - in /rewrap; mmwtex.c mmhlpa.c mminou.c - minor edits */ -/* 0.196 nm 31-Dec-2020 metamath.c mmpars.c - fix bug that deleted comments - that were followed by ${, $}, $c, $v, $d on the same line */ -/* 0.195 nm 30-Dec-2020 metamath.c - temporarily disable /REWRAP until bug fixed - 27-Sep-2020 nm mmwtex.c - prevent "htmlexturl" links from wrapping */ -/* 0.194 26-Dec-2020 nm mmwtex.c - add keyword "htmlexturl" to $t - statement in .mm file */ -/* 0.193 12-Sep-2020 nm mmcmds.c mmdata.c,h mmwtex.c,h mmhlpa.c - make the - output of /EXTRACT stable in the sense that, with the same - parameter, extract(extract(file)) = extract(file) except that the date - stamp at the top will be updated. (The first extraction even if "*" will - usually be different because it discards non-relevant content. Note that - the include file directives "$( $[ Begin..." etc. and comments with "$j" are - currently discarded.) */ -/* 0.192 4-Sep-2020 nm metamath.c - fix bug */ -/* 0.191 4-Sep-2020 nm metamath.c - add comment close */ -/* 0.190 4-Sep-2020 nm mmcmds.c - fix bug in writeExtractedSource() */ -/* 0.189 4-Sep-2020 nm mmhlpa.c - add help for WRITE SOURCE .. /EXTRACT ... - 24-Aug-2020 nm metamath.c mmcmdl.c mmcmds.c,h mmdata.c,h mmhlpa.c - mmpars.c mmpfas.c mmunif.c mmwtex.c,h - Added - WRITE SOURCE ... /EXTRACT ... */ -/* 0.188 23-Aug-2020 nm mmwtex.c, mmhlpa.c Added CONCLUSION FACT INTRODUCTION - PARAGRAPH SCOLIA SCOLION SUBSECTION TABLE to [bib] keywords */ -/* 0.187 15-Aug-2020 nm All m*.c, m*.h - put "g_" in front of all global - variable names e.g. "statements" becomes "g_statements"; also capitalized - 1st letter of original name in case of global structs e.g. "statement" - becomes "g_Statement". - 9-Aug-2020 nm mmcmdl.c, mmhlpa.c - add HELP BIBLIOGRAPHY */ -/* 0.186 8-Aug-2020 nm mmwtex.c, mmhlpa.c - add CONJECTURE, RESULT to [bib] - keywords - 8-Aug-2020 nm mmpfas.c, metamath.c - print message when IMPROVE or - MINIMIZE_WITH uses another mathbox */ -/* 0.185 5-Aug-2020 nm metamath.c mmcmdl.c mmhlpb.c mmpfas.c,h mmcmds.c - mmwtex.c,h - add /INCLUDE_MATHBOXES to to IMPROVE; notify user upon ASSIGN - from another mathbox. - 18-Jul-2020 nm mmcmds.c, mmdata.c, mmhlpb.c, metamath.c - "PROVE =" will now - resume the previous MM-PA session if there was one; allow "~" to start/end - with blank (meaning first/last statement); add "@1234" */ -/* 0.184 17-Jul-2020 nm metamath.c mmcmdl.c mmcmds.c,h mmhlpb.c mmwtex.c,h - - add checking for mathbox independence to VERIFY MARKUP; add /MATHBOX_SKIP - 4-Jul-2020 nm mmwtex.c - correct error msg for missing althtmldef - 3-Jul-2020 nm metamath.c, mmhlpa.c - allow space in TOOLS> BREAK */ -/* 0.183 30-Jun-2020 30-Jun-2020 nm mmpars.c - refine prevention of - WRITE SOURCE.../REWRAP from modifying comments containing "" - (specifically, remove indentation alignment). - 25-Jun-2020 nm metamath.c, mmcmds.c,h mmcmdl.c mmhlpb.c - add underscore - checking in VERIFY MARKUP and add /UNDERSCORE_SKIP qualifier; also check - for trailing space on lines. - 20-Jun-2020 nm mmcmds.c - check for discouragement tags in *ALT, *OLD - labels in VERIFY MARKUP. - 19-Jun-2020 nm mminou.c,h, metamath.c, mmwtex.c - dynamically allocate - buffer in print2() using vsnprintf() to calculate size needed - 18-Jun-2020 nm mmpars.c - remove error check for $e <- $f assignments. See - https://groups.google.com/d/msg/metamath/Cx_d84uorf8/0FrNYTM9BAAJ */ -/* 0.182 12-Apr-2020 nm mmwtex.c, mmphlpa.c - add "Claim" to bib ref types */ -/* 0.181 12-Feb-2020 nm (reported by David Starner) metamath.c - fix bug causing - new axioms to be used by MINIMIZE_WITH */ -/* 0.180 10-Dec-2019 nm (bj 13-Sep-2019) mmpars.c - fix "line 0" in error msg - when label clashes with math symbol - 8-Dec-2019 nm (bj 13-Oct-2019) mmhlpa.c - improve TOOLS> HELP INSERT, DELETE - 8-Dec-2019 nm (bj 19-Sep-2019) mminou.c - change bug 1511 to error message - 30-Nov-2019 nm (bj 12-Oct-2019) mmwtex.c - trigger Most Recent link on - mmtheorems.html when there is a mathbox statement (currently set.mm and - iset.mm). - 30-Nov-2019 nm (bj 13-Sep-2019) mmhlpa.c - improve help for TOOLS> DELETE and - SUBSTITUTE. - 30-Nov-2019 nm (bj 13-Sep-2019) mmwtex.c - change "g_htmlHome" in warnings to - "htmlhome". */ -/* 0.179 29-Nov-2019 nm (bj 22-Sep-2019) metamath.c - MINIMIZE_WITH axiom trace - now starts from current NEW_PROOF instead of SAVEd proof. - 23-Nov-2019 nm (bj 4-Oct-2019) metamath.c - make sure traceback flags are - cleared after MINIMIZE_WITH - 20-Nov-2019 nm mmhlpa.c - add url pointer to HELP WRITE SOURCE /SPLIT - 18-Nov-2019 nm mmhlpa.c - clarify HELP WRITE SOURCE /REWRAP - 15-Oct-2019 nm mmdata.c - add bug check info for user - 14-Oct-2019 nm mmcmds.c - use '|->' (not 'e.') as syntax hint for maps-to - 14-Oct-2019 nm mmwtex.c - remove extraneous */ -/* 0.178 10-Aug-2019 nm mminou.c - eliminate redundant fopen in fSafeOpen - 6-Aug-2019 nm mmwtex.c,h, mmcmds.c - Add error check for >1 line - section name or missing closing decoration line in getSectionHeadings() - 4-Aug-2019 nm mmhlpb.c, mmcmdl.c, metamath.c - Add /ALLOW_NEW_AXIOMS, - renamed /ALLOW_GROWTH to /MAY_GROW - 17-Jul-2019 nm mmcmdl.c, mmhlpa.c, metamath.c - Add /NO_VERSIONING to - WRITE THEOREM_LIST - 17-Jul-2019 nm metamath.c - Change line of dashes between SHOW STATEMENT - output from hardcoded 79 to current g_screenWidth */ -/* 0.177 27-Apr-2019 nm mmcmds.c -"set" -> "setvar" in htmlAllowedSubst. - mmhlpb.c - fix typos in HELP IMPROVE. */ -/* 0.176 25-Mar-2019 nm metamath.c mmcmds.h mmcmds.c mmcmdl.c mmhlpb.c - - add /TOP_DATE_SKIP to VERIFY MARKUP */ -/* 0.175 8-Mar-2019 nm mmvstr.c - eliminate warning in gcc 8.3 (patch - provided by David Starner) */ -/* 0.174 22-Feb-2019 nm mmwtex.c - fix erroneous warning when using "[[" - bracket escape in comment */ -/* 0.173 3-Feb-2019 nm mmwtex.c - fix infinite loop when "[" was the first - character in a comment */ -/* 0.172 25-Jan-2019 nm mmwtex.c - comment out bug 2343 trap (not a bug) */ -/* 0.171 13-Dec-2018 nm metamath.c, mmcmdl.c, mmhlpa.c, mmcmds.c,h, mmwtex.c,h - - add fine-grained qualifiers to MARKUP command */ -/* 0.170 12-Dec-2018 nm mmwtex.c - restore line accidentally deleted in 0.169 */ -/* 0.169 10-Dec-2018 nm metamath.c, mmcmds.c,h, mmcmdl.c, mmpars.c, mmhlpa.c, - mmwtex.c - Add MARKUP command. - 9-Dec-2018 nm mmwtex.c - escape literal "[" with "[[" in comments. */ -/* 0.168 8-Dec-2018 nm metamath.c - validate that /NO_REPEATED_STEPS is used - only with /LEMMON. - 8-Dec-2018 nm mmcmds.c - fix bug #256 reported by Jim Kingdon - (https://github.com/metamath/set.mm/issues/497). */ -/* 0.167 13-Nov-2018 nm mmcmds.c - SHOW TRACE_BACK .../COUNT now uses proof - the way it's stored (previously, it always uncompressed the proof). The - new step count (for compressed proofs) corresponds to the step count the - user would see on the web pages. - 12-Nov-2018 nm mmcmds.c - added unlimited precision arithmetic - for SHOW TRACE_BACK .../COUNT/ESSENTIAL */ -/* 0.166 31-Oct-2018 nm mmwtex.c - workaround Chrome anchor bug - 30-Oct-2018 nm mmcmds.c - put "This theorem is referenced by" after - axioms and definitions used in HTML; use "(None)" instead of suppressing - line if nothing is referenced */ -/* 0.165 20-Oct-2018 nm mmwtex.c - added ~ mmtheorems#abc type anchor - in TOC details. mmwtex.c - fix bug (reported by Benoit Jubin) that - changes "_" in labels to subscript. mmcmdl.c - remove unused COMPLETE - qualifier from SHOW PROOF. mmwtex.c - enhance special cases of web page - spacing identified by Benoit Jubin */ -/* 0.164 5-Sep-2018 nm mmwtex.c, mmhlpb.c - added NOTE to bib keywords - 14-Aug-2018 nm metamath.c - added defaultScrollMode to prevent - SET SCROLL CONTINUOUS from reverting to PROMPTED after a SUBMIT command */ -/* 0.163 4-Aug-2018 nm mmwtex.c - removed 2nd "sandbox:bighdr" anchor - in mmtheorems.html; removed Firefox and IE references; changed breadcrumb - font to be consistent with other pages; put asterisk next to TOC entries - that have associated comments */ -/* FOR FUTURE REFERENCE: search for "Thierry" in mmwtex.c to modify the link - to tirix.org structured proof site */ -/* 0.162-thierry 3-Jun-2018 nm mmwtex.c - add link to tirix.org structured - proofs */ -/* 0.162 3-Jun-2018 nm mmpars.c - re-enabled error check for $c not in - outermost scope. mmhlpa.c mmhlpb.c- improve some help messages. - mmwtex.c - added "OBSERVATION", "PROOF", AND "STATEMENT" keywords for - WRITE BIBLIOGRAPHY */ -/* 0.161 2-Feb-2018 nm mmpars.c,h mmcmds.c mmwtex.c - fix wrong file name - and line number in error messages */ -/* 0.160 24-Jan-2018 nm mmpars.c - fix bug introduced in version 0.158 */ -/* 0.159 23-Jan-2018 nm mmpars.c - fix crash due to missing include file */ -/* 0.158 22-Jan-2018 nm mminou.c - strip CRs from Windows SUBMIT files - run on Linux */ -/* 0.157 15-Jan-2018 nm Major rewrite of READ-related functions. - Added HELP MARKUP. - 9-Jan-2018 nm Track line numbers for error messages in included files - 1-Jan-2018 nm Changed HOME_DIRECTORY to ROOT_DIRECTORY - 31-Dec-2017 nm metamath.c mmcmdl.c,h mmpars.c,h mmcmds.c,h mminou.c,h - mmwtex.c mmhlpb.c mmdata.h - add virtual includes "$( Begin $[...$] $)", - $( End $[...$] $)", "$( Skip $[...$] $)" */ -/* 0.156 8-Dec-2017 nm mmwtex.c - fix bug that incorrectly gave "verify markup" - errors when there was a mathbox statement without an "extended" section */ -/* 0.155 8-Oct-2017 nm mmcmdl.c - restore accidentally removed HELP HTML; - mmhlpb.c mmwtex.c mmwtex.h,c mmcmds.c metamath.c - improve HELP and make - other cosmetic changes per Benoit Jubin's suggestions */ -/* 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; - metamath.c - enforce minimum screen width = 3 to prevent crash reported - by Benoit Jubin */ -/* 0.151 20-Sep-2017 nm mmwtex.c - better matching to insert space between - A and y in "E. x e. ran A y R x" to prevent spurious spaces in thms rncoeq, - dfiun3g as reported by Benoit Jubin */ -/* 0.150 26-Aug-2017 nm mmcmds.c,mmwtex.h - fix hyperlink for Distinct variable - etc. lists so that it will point to mmset.html on other Explorers like NF. - Move the "Dummy variables..." to print after the "Proof of Theorem..." - line. */ -/* 0.149 21-Aug-2017 nm mmwtex.c,h mmcmds.c mmhlpb.c - add a subsubsection - "tiny" header with separator "-.-." to table of contents and theorem list; - see HELP WRITE THEOREM_LIST - 21-Aug-2017 nm mmcmds.c - remove bug check 255 - 19-Aug-2017 nm mmcmds.c - change mmset.html links to - ../mpeuni/mmset.html so they will work in NF Explorer etc. */ -/* 0.148 14-Aug-2017 nm mmcmds.c - hyperlink "Dummy variable(s)" */ -/* 0.147 13-Aug-2017 nm mmcmds.c,h - add "Dummy variable x is distinct from all - other variables." to proof web page */ -/* 0.146 26-Jun-2017 nm mmwtex.c - fix handling of local labels in - 'show proof.../tex' (bug 2341 reported by Eric Parfitt) */ -/* 0.145 16-Jun-2017 nm metamath.c mmpars.c - fix bug 1741 during - MINIMIZE_WITH; mmpfas.c - make duplicate bug numbers unique; mmhlpa.c - mmhlpb.c - adjust to prevent lcc compiler "Function too big for the - optimizer" - 29-May-2017 nm mmwtex.c mmhlpa.c - take out extraneous ... - markup tags in HTML output so w3c validator will pass */ -/* 0.144 15-May-2017 nm metamath.c mmcmds.c - add "(Revised by..." tag for - conversion of legacy .mm's if there is a 2nd date under the proof */ -/* 0.143 14-May-2017 nm metamath.c mmdata.c,h mmcmdl.c mmcmds.c mmhlpb.c - - added SET CONTRIBUTOR; for missing "(Contributed by..." use date - below proof if it exists, otherwise use today's date, in order to update - old .mm files. - 14-May-2017 Ari Ferrera - mmcmds.c - fix memory leaks in ERASE */ -/* 0.142 12-May-2017 nm metamath.c mmdata.c,h mmcmds.c - added - "#define DATE_BELOW_PROOF" in mmdata.h that if uncommented, will enable - use of the (soon-to-be obsolete) date below the proof - 4-May-2017 Ari Ferrera - mmcmds.c metamath.c mmdata.c mmcmdl.c - mminou.c mminou.h mmcmdl.h mmdata.h - fixed memory leaks and warnings - found by valgrind. - 3-May-2017 nm - metamath.c mmdata.c,h mmcmds.c,h mmpars.c,h mmhlpb.c - mmcmdl.c mmwtex.c - added xxChanged flags to statement structure so - that any part of the source can be changed; removed /CLEAN qualifier - of WRITE SOURCE; automatically put "(Contributed by ?who?..." during - SAVE NEW_PROOF or SAVE PROOF when it is missing; more VERIFY MARKUP - checking. */ -/* 0.141 2-May-2017 nm mmdata.c, metamath.c, mmcmds.c, mmhlpb.c - use - getContrib() date for WRITE RECENT instead of date below proof. This lets - us list recent $a's as well as $p's. Also, add caching to getContrib() for - speedup. */ -/* 0.140 1-May-2017 nm mmwtex.c, mmcmds.c, metamath.c - fix some LaTeX issues - reported by Ari Ferrera */ -/* 0.139 2-Jan-2017 nm metamath.c - print only one line for - 'save proof * /compressed/fast' */ -/* 0.138 26-Dec-2016 nm mmwtex.c - remove extraneous causing w3c - validation failure; put space after 1st x in "F/ x x = x"; - mmcmds.c - added checking for lines > 79 chars in VERIFY MARKUP; - mmcmds.c, mmcmdl.c, metamath.c, mmhlpb.c, mmcmds.h - added /VERBOSE to - VERIFY MARKUP */ -/* 0.137 20-Dec-2016 nm mmcmds.c - check ax-XXX $a vs axXXX $p label convention - in 'verify markup' - 18-Dec-2016 nm mmwtex.c, mmpars.c, mmdata.h - use true "header area" - between successive $a/$p for getSectionHeadings() mmcmds.c - add - header comment checking - 13-Dec-2016 nm mmdata.c,h - enhanced compareDates() to treat empty string as - older date. - 13-Dec-2016 nm metamath.c, mmcmds.c - moved mm* and Microsoft illegal file - name label check to verifyMarkup() (the VERIFY MARKUP command) instead of - checking on READ; added check of set.mm Version date to verifyMarkup(). - 13-Dec-2016 nm mmwtex.c,h - don't treat bracketed description text with - space as a bib label; add labelMatch parameter to writeBibliography() */ -/* 0.136 10-Oct-2016 mminou.c - fix resource leak bug reported by David - Binderman */ -/* 0.135 11-Sep-2016, 14-Sep-2016 metamath.c, mmpfas.c,h, mmdata.c,h, - mmpars.c,h mmcmds.c, mmcmdl.c, mmhlpb.c - added EXPAND command */ -/* 0.134 16-Aug-2016 mmwtex.c - added breadcrumbs to theorem pages; - metamath.c, mmcmdl.c, mmhlpb.c, mminou.c,.h - added /TIME to SAVE PROOF, - SHOW STATEMENT.../[ALT}HTML, MINIMIZE_WITH */ -/* 0.133 13-Aug-2016 mmwtex.c - improve mobile display with tag - mmpars.c - use updated Macintosh information */ -/* 0.132 10-Jul-2016 metamath.c, mmcmdl.c, mmcmds.c,.h, mmdata.c,.h, mmhlpb.c, - mmpfas.c - change "restricted" to "discouraged" to match set.mm markup - tags; add SET DISCOURAGEMENT OFF|ON (default ON) to turn off blocking for - convenience of advanced users - 6-Jul-2016 metamath.c - add "(void)" in front of "system(...)" to - suppress -Wunused-result warning */ -/* 0.131 10-Jun-2016 mminou.c - reverted change of 22-May-2016 because - 'minimize_with' depends on error message in string to prevent DV violations. - Todo: write a DV-checking routine for 'minimize_with', then revert - the 22-May-2016 fix for bug 126 (which only occurs when writing web - pages for .mm file with errors). - 9-Jun-2016 mmcmdl.c, metamath.c - added _EXIT_PA for use with - scripts that will give an error message outside of MM-PA> rather - than exiting metamath */ -/* 0.130 25-May-2016 mmpars.c - workaround clang warning about j = j; - mmvstr.c - workaround gcc -Wstrict-overflow warning */ -/* 0.129 24-May-2016 mmdata.c - fix bug 1393 */ -/* 0.128 22-May-2016 mminou.c - fixed error message going to html page - instead of to screen, triggering bug 126. */ -/* 0.127 10-May-2016 metamath.c, mmcmdl.c, mmhlpb.c - added /OVERRIDE to - PROVE */ -/* 0.126 3-May-2016 metamath.c, mmdata.h, mmdata.c, mmcmds.h, mmcmds.c, - mmcmdl.c, mmhlpb.c, mmpars.c - added getMarkupFlag() in mmdata.c; - Added /OVERRIDE added to ASSIGN, REPLACE, IMPROVE, MINIMIZE_WITH, - SAVE NEW_PROOF; PROVE gives warning about SAVE NEW_PROOF for locked - proof. Added SHOW RESTRICTED command. - 3-May-2016 m*.c - fix numerous conversion warnings provided by gcc 5.3.0 */ -/* 0.125 10-Mar-2016 mmpars.c - fixed bug parsing /EXPLICIT/PACKED format - 8-Mar-2016 nm mmdata.c - added "#nnn" to SHOW STATEMENT etc. to reference - statement number e.g. SHOW STATEMENT #58 shows a1i in set.mm. - 7-Mar-2016 nm mmwtex.c - added space between } and { in HTML output - 6-Mar-2016 nm mmpars.c - disabled wrapping of formula lines in - WRITE SOURCE.../REWRAP - 2-Mar-2016 nm metamath.c, mmcmdl.c, mmhlpb.c - added /FAST to - SAVE PROOF, SHOW PROOF */ -/* 0.123 25-Jan-2016 nm mmpars.c, mmdata.h, mmdata.c, mmpfas.c, mmcmds., - metamath.c, mmcmdl.c, mmwtex.c - unlocked SHOW PROOF.../PACKED, - added SHOW PROOF.../EXPLICIT */ -/* 0.122 14-Jan-2016 nm metamath.c, mmcmds.c, mmwtex.c, mmwtex.h - surrounded - math HTML output with "...; added htmlcss and - htmlfont $t commands - 10-Jan-2016 nm mmwtex.c - delete duplicate -4px style; metamath.c - - add   after char on mmascii.html - 3-Jan-2016 nm mmwtex.c - fix bug when doing SHOW STATEMENT * /ALT_HTML after - VERIFY MARKUP */ -/* 0.121 17-Nov-2015 nm metamath.c, mmcmdl.h, mmcmdl.c, mmcmds.h, mmcmds.c, - mmwtex.h, mmwtex.c, mmdata.h, mmdata.c - - 1. Moved WRITE BIBLIOGRAPHY code from metamath.c to its own function in - mmwtex.c; moved qsortStringCmp() from metamath.c to mmdata.c - 2. Added $t, comment markup, and bibliography checking to VERIFY MARKUP - 3. Added options to bug() bug-check interception to select aborting, - stepping to next bug, or ignoring subsequent bugs - 4. SHOW STATEMENT can now use both /HTML and /ALT_HTML in same session - 5. Added /HTML, /ALT_HTML to WRITE THEOREM_LIST and - WRITE RECENT_ADDITIONS */ -/* 0.120 7-Nov-2015 nm metamath.c, mmcmdl.c, mmpars.c - add VERIFY MARKUP - 4-Nov-2015 nm metamath.c, mmcmds.c/h, mmdata.c/h - move getDescription, - getSourceIndentation from mmcmds.c to mmdata.c. - metamath.c, mmdata.c - add and call parseDate() instead of in-line - code; add getContrib(), getProofDate(), buildDate(), compareDates(). */ -/* 0.119 18-Oct-2015 nm mmwtex.c - add summary TOC to Theorem List; improve - math symbol GIF image alignment - 2-Oct-2015 nm metamath.c, mmpfas.c, mmwtex.c - fix miscellaneous small - bugs or quirks */ -/* 0.118 18-Jul-2015 nm metamath.c, mmcmds.h, mmcmds.c, mmcmdl.c, mmhlpb.h, - mmhlpb.c - added /TO qualifier to SHOW TRACE_BACK. See - HELP SHOW TRACE_BACK. */ -/* 0.117 30-May-2015 - 1. nm mmwtex.c - move of Theorem List pages */ -/* 0.115 8-May-2015 nm mmwtex.c - added section header comments to - WRITE THEOREM_LIST and broke out Table of Contents page - 24-Apr-2015 nm metamath.c - add # bytes to end of "---Clip out the proof"; - reverted to no blank lines there (see 0.113 item 3) */ -/* 0.114 22-Apr-2015 nm mmcmds.c - put [-1], [-2],... offsets on 'show - new_proof/unknown' */ -/* 0.113 19-Apr-2015 so, nm metamath.c, mmdata.c - 1. SHOW LABEL % will show statements with changed proofs - 2. SHOW LABEL = will show the statement being proved in MM-PA - 3. Added blank lines before, after "---------Clip out the proof" proof - 4. Generate date only if the proof is complete */ -/* 0.112 15-Apr-2015 nm metamath.c - fix bug 1121 (reported by S. O'Rear); - mmwtex.c - add "img { margin-bottom: -4px }" to CSS to align symbol GIFs; - mmwtex.c - remove some hard coding for set.mm, for use with new nf.mm; - metamath.c - fix comment parsing in WRITE BIBLIOGRAPHY to ignore - math symbols */ -/* 0.111 22-Nov-2014 nm metamath.c, mmcmds.c, mmcmdl.c, mmhlpb.c - added - /NO_NEW_AXIOMS_FROM qualifier to MINIMIZE_WITH; see HELP MINIMIZE_WITH. - 21-Nov-2014 Stefan O'Rear mmdata.c, mmhlpb.c - added ~ label range specifier - to wildcards; see HELP SEARCH */ -/* 0.110 2-Nov-2014 nm mmcmds.c - fixed bug 1114 (reported by Stefan O'Rear); - metamath.c, mmhlpb.c - added "SHOW STATEMENT =" to show the statement - being proved in MM-PA (based on patch submitted by Stefan O'Rear) */ -/* 0.109 20-Aug-2014 nm mmwtex.c - fix corrupted HTML caused by misinterpreting - math symbols as comment markup (math symbols with _ [ ] or ~). Also, - allow https:// as well as http:// in ~ label markup. - 11-Jul-2014 wl mmdata.c - fix obscure crash in debugging mode db9 */ -/* 0.108 25-Jun-2014 nm - (1) metamath.c, mmcmdl.c, mmhlpb.c - MINIMIZE_WITH now checks the size - of the compressed proof, prevents $d violations, and tries forward and - reverse statement scanning order; /NO_DISTINCT, /BRIEF, /REVERSE - qualifiers were removed. - (2) mminou.c - prevent hard breaks (in the middle of a word) in too-long - lines (e.g. long URLs) in WRITE SOURCE .../REWRAP; just overflow the - screen width instead. - (3) mmpfas.c - fixed memory leak in replaceStatement() - (4) mmpfas.c - suppress inf. growth with MINIMIZE_WITH idi/ALLOW_GROWTH */ -/* 0.107 21-Jun-2014 nm metamath.c, mmcmdl.c, mmhlpb.c - added /SIZE qualifier - to SHOW PROOF; added SHOW ELAPSED_TIME; mmwtex.c - reformatted WRITE - THEOREM_LIST output; now "$(", newline, "######" starts a "part" */ -/* 0.106 30-Mar-2014 nm mmwtex.c - fix bug introduced by 0.105 that disabled - hyperlinks on literature refs in HTML comment. metamath.c - improve - messages */ -/* 0.105 15-Feb-2014 nm mmwtex.c - prevented illegal LaTeX output for certain - special characters in comments. */ -/* 0.104 14-Feb-2014 nm mmwtex.c - fixed bug 2312, mmcmds.c - enhanced ASSIGN - error message. */ -/* 0.103 4-Jan-2014 nm mmcmds.c,h - added "Allowed substitution hints" below - the "Distinct variable groups" list on generated web pages - mmwtex.c - added "*" to indicate DV's occur in Statement List entries. */ -/* 0.102 2-Jan-2014 nm mminou.c - made compressed proof line wrapping more - uniform at start of compressed part of proof */ -/* 0.101 27-Dec-2013 nm mmdata.h,c, mminou.c, mmcmdl.c, mmhlpb.c, mmvstr.c - - Improved storage efficiency of /COMPRESSED proofs (but with 20% slower run - time); added /OLD_COMPRESSION to specify old algorithm; removed end-of-line - space after label list in old algorithm; fixed linput() bug */ -/* 0.100 30-Nov-2013 nm mmpfas.c - reversed statement scan order in - proveFloating(), to speed up SHOW STATEMENT df-* /HTML; metamath.c - remove - the unknown date place holder in SAVE NEW_PROOF; Wolf Lammen mmvstr.c - - some cleanup */ -/* 0.07.99 1-Nov-2013 nm metamath.c, mmpfas.h,c, mmcmdl.h,c, mmhlpa.c, - mmhlpb.c - added UNDO, REDO, SET UNDO commands (see HELP UNDO) */ -/* 0.07.98 30-Oct-2013 Wolf Lammen mmvstr.c,h, mminou.c, mmpars.c, - mmdata.c - improve code style and program structure */ -/* 0.07.97 20-Oct-2013 Wolf Lammen mmvstr.c,h, metamath.c - improved linput(); - nm mmcmds.c, mmdata.c - tolerate bad proofs in SHOW TRACE_BACK etc. */ -/* 0.07.96 20-Sep-2013 Wolf Lammen mmvstr.c - revised cat(); - nm mmwtex.c, mminou.c - change a print2 to printLongLine to fix bug 1150 */ -/* 0.07.95 18-Sep-2013 Wolf Lammen mmvstr.c - optimized cat(); - nm metamath.c, mmcmds.c, mmdata.c, mmpars.c, mmpfas.c, mmvstr.c, - mmwtex.c - suppress some clang warnings */ -/* 0.07.94 28-Aug-2013 Alexey Merkulov mmcmds.c, mmpars.c - fixed several - memory leaks found by valgrind --leak-check=full --show-possibly-lost=no */ -/* 0.07.93 8-Jul-2013 Wolf Lammen mmvstr.c - simplified let() function; - also many minor changes in m*.c and m*.h to assist future refactoring */ -/* 0.07.92 28-Jun-2013 nm metamath.c mmcmds.c,h mmcmdl.c mmhlpb.c- added - /NO_REPEATED_STEPS for /LEMMON mode of SHOW PROOF, SHOW NEW_PROOF. - This reverts the /LEMMON mode default display change of 31-Jan-2010 - and invokes it when desired via /NO_REPEATED_STEPS. */ -/* 0.07.91 20-May-2013 nm metamath.c mmpfas.c,h mmcmds.c,h mmcmdl.c - mmhlpb.c- added /FORBID qualifier to MINIMIZE_WITH */ -/* 0.07.90 19-May-2013 nm metamath.c mmcmds.c mmcmdl.c mmhlpb.c - added /MATCH - qualifier to SHOW TRACE_BACK */ -/* 0.07.88 18-Nov-2012 nm mmcmds.c - fixed bug 243 */ -/* 0.07.87 17-Nov-2012 nm mmwtex.c - fixed formatting problem when label - markup ends a comment in SHOW PROOF ... /HTML */ -/* 0.07.86 27-Oct-2012 nm mmcmds.c, mmwtex.c, mmwtex.h - fixed ERASE bug - caused by imperfect re-initialization; reported by Wolf Lammen */ -/* 0.07.85 10-Oct-2012 nm metamath.c, mmcmdl.c, mmwtex.c, mmwtex.h, mmhlpb.c - - added /SHOW_LEMMAS to WRITE THEOREM_LIST to bypass lemma math suppression */ -/* 0.07.84 9-Oct-2012 nm mmcmds.c - fixed bug in getStatementNum() */ -/* 0.07.83 19-Sep-2012 nm mmwtex.c - fixed bug reported by Wolf Lammen */ -/* 0.07.82 16-Sep-2012 nm metamath.c, mmpfas.c - fixed REPLACE infinite loop; - improved REPLACE message for shared dummy variables */ -/* 0.07.81 14-Sep-2012 nm metamath.c, mmcmds.c, mmcmds.h, mmcmdl.c, mmhlpb.c - - added FIRST, LAST, +nn, -nn where missing from ASSIGN, REPLACE, - IMPROVE, LET STEP. Wildcards are allowed for PROVE, ASSIGN, REPLACE - labels provided there is a unique match. */ -/* 0.07.80 4-Sep-2012 nm metamath.c, mmpfas.c, mmpfas.h, mmcmdl.c, mmhlpb.c - - added / 1, / 2, / 3, / SUBPROOFS to IMPROVE to specify search level */ -/* 0.07.79 31-Aug-2012 nm m*.c - clean up some gcc warnings */ -/* 0.07.78 28-Aug-2012 nm mmpfas.c - fix bug in 0.07.77. */ -/* 0.07.77 25-Aug-2012 nm metamath.c, mmpfas.c - Enhanced IMPROVE algorithm to - allow non-shared dummy variables in unknown steps */ -/* 0.07.76 22-Aug-2012 nm metamath.c, mmpfas.c, mmcmdl.c, mmhlpb.c - - Enhanced IMPROVE algorithm to also try REPLACE algorithm */ -/* 0.07.75 14-Aug-2012 nm metamath.c - MINIMIZE_WITH now checks current - mathbox (but not other mathboxes) even if /INCLUDE_MATHBOXES is omitted */ -/* 0.07.74 18-Mar-2012 nm mmwtex.c, mmcmds.c, metamath.c - improved texToken() - error message */ -/* 0.07.73 26-Dec-2011 nm mmwtex.c, mmpars.c - added ... in - comments for passing through raw HTML code into HTML files generated with - SHOw STATEMENT xxx / HTML */ -/* 0.07.72 25-Dec-2011 nm (obsolete) */ -/* 0.07.71 10-Nov-2011 nm metamath.c, mmcmdl.c - added /REV to MINIMIZE_WITH */ -/* 0.07.70 6-Aug-2011 nm mmwtex.c - fix handling of double quotes inside - of htmldef strings to match spec in Metamath book Appendix A p. 156 */ -/* 0.07.69 9-Jul-2011 nm mmpars.c, mmvstr.c - Untab file in WRITE SOURCE - ... /REWRAP */ -/* 0.07.68 3-Jul-2011 nm metamath.c, mminou.h, mminou.c - Nested SUBMIT calls - (SUBMIT calls inside of a SUBMIT command file) are now allowed. - Also, mmdata.c - fix memory leak. */ -/* 0.07.67 2-Jul-2011 nm metamath.c, mmcmdl.c, mmhlpa.c - Added TAG command - to TOOLS. See HELP TAG under TOOLS. (The old special-purpose TAG command - was renamed to UPDATE.) */ -/* 0.07.66 1-Jul-2011 nm metamath.c, mmcmds.c, mmpars.c, mmpars.h - Added code - to strip spurious "$( [?] $)" in WRITE SOURCE ... /CLEAN output */ -/* 0.07.65 30-Jun-2011 nm mmwtex.c - Prevent processing [...] bibliography - brackets inside of `...` math strings in comments. */ -/* 0.07.64 28-Jun-2011 nm metamath.c, mmcmdl.c - Added /INCLUDE_MATHBOXES - qualifier to MINIMIZE_WITH; without it, MINIMIZE_WITH * will skip - checking user mathboxes. */ -/* 0.07.63 26-Jun-2011 nm mmwtex.c - check that .gifs exist for htmldefs */ -/* 0.07.62 18-Jun-2011 nm mmpars.c - fixed bug where redeclaration of active - $v was not detected */ -/* 0.07.61 12-Jun-2011 nm mmpfas.c, mmcmds.c, metamath.c, mmhlpb.c - added - /FORMAT and /REWRAP qualifiers to WRITE SOURCE to format according to set.mm - conventions - set HELP WRITE SOURCE */ -/* 0.07.60 7-Jun-2011 nm mmpfas.c - fixed bug 1805 which occurred when doing - MINIMIZE_WITH weq/ALLOW_GROWTH after DELETE DELETE FLOATING_HYPOTHESES */ -/* 0.07.59 11-Dec-2010 nm mmpfas.c - increased default SET SEARCH_LIMIT from - 10000 to 25000 to accommodate df-plig web page in set.mm */ -/* 0.07.58 9-Dec-2010 nm mmpars.c - detect if same symbol is used with both - $c and $v, in order to conform with Metamath spec */ -/* 0.07.57 19-Oct-2010 nm mmpars.c - fix bug causing incorrect line count - for error messages when non-ASCII character was found; mminou.h - - increase SET WIDTH maximum from 999 to 9999 */ -/* 0.07.56 27-Sep-2010 nm mmpars.c, mmpfas.c - check for $a's with - one token e.g. "$a wff $."; if found, turn SET EMPTY_SUBSTITUTION ON - automatically. (Suggested by Mel O'Cat; patent pending.) */ -/* 0.07.55 26-Sep-2010 nm mmunif.c, mmcmds.c, mmunif.h - check for mismatched - brackets in all $a's, so that if there are any, the bracket matching - algorithm (for fewer ambiguous unifications) in mmunif.c will be turned - off. */ -/* 0.07.54 25-Sep-2010 nm mmpars.c - added $f checking to conform to the - current Metamath spec, so footnote 2 on p. 92 of Metamath book is - no longer applicable. */ -/* 0.07.53 24-Sep-2010 nm mmveri.c - fixed bug(2106), reported by Michal - Burger */ -/* 0.07.52 14-Sep-2010 nm metamath.c, mmwtex.h, mmwtex.c, mmcmds.c, - mmcmdl.c, mmhlpb.c - rewrote the LaTeX output for easier hand-editing - and embedding in LaTeX documents. The old LaTeX output is still - available with /OLD_TEX on OPEN TEX, SHOW STATEMENT, and SHOW PROOF, - but it is obsolete and will be deleted eventually if no one objects. The - new /TEX output also replaces the old /SIMPLE_TEX, which was removed. */ -/* 0.07.51 9-Sep-2010 Stefan Allen mmwtex.c - put hyperlinks on hypothesis - label references in SHOW STATEMENT * /HTML, ALT_HTML output */ -/* 0.07.50 21-Feb-2010 nm mminou.c - "./metamath < empty", where "empty" is a - 0-byte file, now exits metamath instead of producing an infinite loop. - Also, ^D now exits metamath. Reported by Cai Yufei */ -/* 0.07.49 31-Jan-2010 nm mmcmds.c - Lemmon-style proofs (SHOW PROOF xxx - /LEMON/RENUMBER) no longer have steps with dummy labels; instead, steps - are now the same as in HTML page proofs. (There is a line to comment - out if you want to revert to old behavior.) */ -/* 0.07.48 11-Sep-2009 nm mmpars.c, mm, mmvstr.c, mmdata.c - Added detection of - non-whitespace around keywords (mmpars.c); small changes to eliminate - warnings in gcc 3.4.4 (mmvstr.c, mmdata.c) */ -/* 0.07.47 2-Aug-2009 nm mmwtex.c, mmwtex.h - added user name to mathbox - pages */ -/* 0.07.46 24-Jul-2009 nm metamath.c, mmwtex.c - changed name of sandbox - to "mathbox" */ -/* 0.07.45 15-Jun-2009 nm metamath.c, mmhlpb.c - put "!" before each line of - SET ECHO ON output to make them easy to identity for creating scripts */ -/* 0.07.44 12-May-2009 Stefan Allan, nm metamath.c, mmcmdl.c, mmwtex.c - - added SHOW STATEMENT / MNEMONICS - see HELP SHOW STATEMENT */ -/* 0.07.43 29-Aug-2008 nm mmwtex.c - workaround for Unicode huge font bug in - FireFox 3 */ -/* 0.07.42 8-Aug-2008 nm metamath.c - added sandbox, Hilbert Space colors to - Definition List */ -/* 0.07.41 29-Jul-2008 nm metamath.c, mmwtex.h, mmwtex.c - Added handling of - sandbox section of Metamath Proof Explorer web pages */ -/* 0.07.40 6-Jul-2008 nm metamath.c, mmcmdl.c, mmhlpa.c, mmhlpb.c - Added - / NO_VERSIONING qualifier for SHOW STATEMENT, so website can be regenerated - in place with less temporary space required. Also, the wildcard trigger - for mmdefinitions.html, etc. is more flexible (see HELP HTML). */ -/* 0.07.39 21-May-2008 nm metamath.c, mmhlpb.c - Added wildcard handling to - statement label in SHOW TRACE_BACK. All wildcards now allow - comma-separated lists [i.e. matchesList() instead of matches()] */ -/* 0.07.38 26-Apr-2008 nm metamath.c, mmdata.h, mmdata.c, mmvstr.c, mmhlpb.c - - Enhanced / EXCEPT qualifier for MINIMIZE_WITH to handle comma-separated - wildcard list. */ -/* 0.07.37 14-Apr-2008 nm metamath.c, mmcmdl.c, mmhlpb.c - Added / JOIN - qualifier to SEARCH. */ -/* 0.07.36 7-Jan-2008 nm metamath.c, mmcmdl.c, mmhlpb.c - Added wildcard - handling for labels in SHOW USAGE. */ -/* 0.07.35 2-Jan-2008 nm mmcmdl.c, metamath.c, mmhlpb.c - Changed keywords - COMPACT to PACKED and COLUMN to START_COLUMN so that SAVE/SHOW proof can use - C to abbreviate COMPRESSED. (PACKED format is supported but "unofficial," - used mainly for debugging purposes, and is not listed in HELP SAVE - PROOF.) */ -/* 0.07.34 19-Nov-2007 nm mmwtex.c, mminou.c - Added tooltips to proof step - hyperlinks in SHOW STATEMENT.../HTML,ALT_HTML output (suggested by Reinder - Verlinde) */ -/* 0.07.33 19-Jul-2007 nm mminou.c, mmvstr.c, mmdata.c, mmword.c - added fflush - after each printf() call for proper behavior inside emacs (suggested by - Frederic Line) */ -/* 0.07.32 29-Apr-2007 nm mminou.c - fSafeOpen now stops at gap; e.g. if ~2 - doesn't exist, ~1 will be renamed to ~2, but any ~3, etc. are not touched */ -/* 0.07.31 5-Apr-2007 nm mmwtex.c - Don't make "_" in hyperlink a subscript */ -/* 0.07.30 8-Feb-2007 nm mmcmds.c, mmwtex.c Added HTML statement number info to - SHOW STATEMENT.../FULL; friendlier "Contents+1" link in mmtheorems*.html */ -/* 0.07.29 6-Feb-2007 Jason Orendorff mmpfas.c - Patch to eliminate the - duplicate "Exceeded trial limit at step n" messages */ -/* 0.07.28 22-Dec-2006 nm mmhlpb.c - Added info on quotes to HELP LET */ -/* 0.07.27 23-Oct-2006 nm metamath.c, mminou.c, mmhlpa.c, mmhlpb.c - Added - / SILENT qualifier to SUBMIT command */ -/* 0.07.26 12-Oct-2006 nm mminou.c - Fixed bug when SUBMIT file was missing - a new-line at end of file (reported by Marnix Klooster) */ -/* 0.07.25 10-Oct-2006 nm metamath.c - Fixed bug invoking TOOLS as a ./metamath - command-line argument */ -/* 0.07.24 25-Sep-2006 nm mmcmdl.c Fixed bug in - SHOW NEW_PROOF/START_COLUMN nn/LEM */ -/* 0.07.23 31-Aug-2006 nm mmwtex.c - Added Home and Contents links to bottom of - WRITE THEOREM_LIST pages */ -/* 0.07.22 26-Aug-2006 nm metamath.c, mmcmdl.c, mmhlpb.c - Changed 'IMPROVE - STEP ' to 'IMPROVE ' for user convenience and to be consistent - with ASSIGN */ -/* 0.07.21 20-Aug-2006 nm mmwtex.c - Revised small colored numbers so that all - colors have the same grayscale brightness.. */ -/* 0.07.20 19-Aug-2006 nm mmpars.c - Made the error "Required hypotheses may - not be explicitly declared" in a compressed proof non-severe, so that we - can still SAVE the proof to reformat and recover it. */ -/* 0.07.19 11-Aug-06 nm mmcmds.c - "Distinct variable group(s)" is now - "group" or "groups" as appropriate. */ -/* 0.07.18 31-Jul-06 nm mmwtex.c - added table to contents to p.1 of output of - WRITE THEOREM_LIST command. */ -/* 0.07.17 4-Jun-06 nm mmpars.c - do not allow labels to match math symbols - (new spec proposed by O'Cat). mmwtex.c - made theorem name 1st in title, - for readability in Firefox tabs. */ -/* 0.07.16 16-Apr-06 nm metamath.c, mmcmdl.c, mmpfas.c, mmhlpb.c - allow step - to be negative (relative to end of proof) for ASSIGN, UNIFY, and LET STEP - (see their HELPs). Added INITIALIZE USER to delete LET STEP assignments - (see HELP INITIALIZE). Fixed bug in LET STEP (mmpfas.c). */ -/* 0.07.15 10-Apr-06 nm metamath.c, mmvstr.c - change dates from 2-digit to - 4-digit year; make compatible with older 2-digit year. */ -/* 0.07.14 21-Mar-06 nm mmpars.c - fix bug 1722 when compressed proof has - "Z" at beginning of proof instead of after a proof step. */ -/* 0.07.13 3-Feb-06 nm mmpfas.c - minor improvement to MINIMIZE_WITH */ -/* 0.07.12 30-Jan-06 nm metamath.c, mmcmds.c, mmdata.c, mmdata.h, mmhlpa.c, - mmhlpb.c - added "?" wildcard to match single character. See HELP SEARCH. */ -/* 0.07.11 7-Jan-06 nm metamath.c, mmcmdl.c, mmhlpb.c - added EXCEPT qualifier - to MINIMIZE_WITH */ -/* 0.07.10 28-Dec-05 nm metamath.c, mmcmds.c - cosmetic tweaks */ -/* 0.07.10 11-Dec-05 nm metamath.c, mmcmdl.c, mmhlpb.c - added ASSIGN FIRST - and IMPROVE FIRST commands. Also enhanced READ error message */ -/* 0.07.9 1-Dec-05 nm mmvstr.c - added comment on how to make portable */ -/* 0.07.9 18-Nov-05 nm metamath.c, mminou.c, mminou.h, mmcmdl.c, mmhlpb.c - - added SET HEIGHT command; changed SET SCREEN_WIDTH to SET WIDTH; changed - SET HENTY_FILTER to SET JEREMY_HENTY_FILTER (to make H for HEIGHT - unambiguous); added HELP for SET JEREMY_HENTY_FILTER */ -/* 0.07.8 15-Nov-05 nm mmunif.c - now detects wrong order in bracket matching - heuristic to further reduce ambiguous unifications in Proof Assistant */ -/* 0.07.7 12-Nov-05 nm mmunif.c - add "[","]" and "[_","]_" bracket matching - heuristic to reduce ambiguous unifications in Proof Assistant. - mmwtex.c - added heuristic for HTML spacing after "sum_" token. */ -/* 0.07.6 15-Oct-05 nm mmcmds.c,mmpars.c - fixed compressed proof algorithm - to match spec in book (with new algorithm due to Marnix Klooster). - Users are warned to convert proofs when the old compression is found. */ -/* 0.07.5 6-Oct-05 nm mmpars.c - fixed bug that reset "severe error in - proof" flag when a proof with severe error also had unknown steps */ -/* 0.07.4 1-Oct-05 nm mmcmds.c - ignored bug 235, which could happen for - non-standard logics */ -/* 0.07.3 17-Sep-05 nm mmpars.c - reinstated duplicate local label checking to - conform to strict spec */ -/* 0.07.2 19-Aug-05 nm mmwtex.c - suppressed math content for lemmas in - WRITE THEOREMS output */ -/* 0.07.1 28-Jul-05 nm Added SIMPLE_TEX qualifier to SHOW STATEMENT */ -/* 0.07: Official 0.07 22-Jun-05 corresponding to Metamath book */ -/* 0.07x: Fixed to work with AMD64 with 64-bit longs by - Waldek Hebisch; deleted unused stuff in mmdata.c */ -/* 0.07w: .mm date format like "$( [7-Sep-04] $)" is now - generated and permitted (old one is tolerated too for compatibility) */ -/* Metamath Proof Verifier - main program */ -/* See the book "Metamath" for description of Metamath and run instructions */ - -/*****************************************************************************/ - -/*----------------------------------------------------------------------*/ +// 0.199.pre +// 30-Dec-2021 mc metamath.c mmdata.c mminou.c mmmaci.c - +// Remove mmmaci and everything related to THINK_C compiler +// 4-Jan-2022 mc - change VERIFY MARKUP /TOP_DATE_SKIP and /FILE_SKIP to +// /TOP_DATE_CHECK and /FILE_CHECK (with opposite meaning), and make the +// skip behavior the default. +// 7-Sep-2022 bj mmwtex.c, mmhlpa.c Added CRITERIA CRITERION to [bib] +// keywords. +// 0.198 nm 7-Aug-2021 mmpars.c - Fix cosmetic bug in WRITE SOURCE ... /REWRAP +// that prevented end of sentence (e.g. period) from appearing in column 79, +// thus causing some lines to be shorter than necessary. +// 0.197 nm 2-Aug-2021 mmpars.c - put two spaces between $c,v on same line +// in /rewrap; mmwtex.c mmhlpa.c mminou.c - minor edits. +// 0.196 nm 31-Dec-2020 metamath.c mmpars.c - fix bug that deleted comments +// that were followed by ${, $}, $c, $v, $d on the same line. +// 0.195 nm 30-Dec-2020 metamath.c - temporarily disable /REWRAP until bug fixed. +// 27-Sep-2020 nm mmwtex.c - prevent "htmlexturl" links from wrapping. +// 0.194 26-Dec-2020 nm mmwtex.c - add keyword "htmlexturl" to $t +// statement in .mm file. +// 0.193 12-Sep-2020 nm mmcmds.c mmdata.c,h mmwtex.c,h mmhlpa.c - make the +// output of /EXTRACT stable in the sense that, with the same +// parameter, extract(extract(file)) = extract(file) except that the date +// stamp at the top will be updated. (The first extraction even if "*" will +// usually be different because it discards non-relevant content. Note that +// the include file directives "$( $[ Begin..." etc. and comments with "$j" are +// currently discarded). +// 0.192 4-Sep-2020 nm metamath.c - fix bug. +// 0.191 4-Sep-2020 nm metamath.c - add comment close. +// 0.190 4-Sep-2020 nm mmcmds.c - fix bug in writeExtractedSource(). +// 0.189 4-Sep-2020 nm mmhlpa.c - add help for WRITE SOURCE .. /EXTRACT ... +// 24-Aug-2020 nm metamath.c mmcmdl.c mmcmds.c,h mmdata.c,h mmhlpa.c +// mmpars.c mmpfas.c mmunif.c mmwtex.c,h - Added +// WRITE SOURCE ... /EXTRACT ... +// 0.188 23-Aug-2020 nm mmwtex.c, mmhlpa.c Added CONCLUSION FACT INTRODUCTION +// PARAGRAPH SCOLIA SCOLION SUBSECTION TABLE to [bib] keywords. +// 0.187 15-Aug-2020 nm All m*.c, m*.h - put "g_" in front of all global +// variable names e.g. "statements" becomes "g_statements"; also capitalized +// 1st letter of original name in case of global structs e.g. "statement" +// becomes "g_Statement". +// 9-Aug-2020 nm mmcmdl.c, mmhlpa.c - add HELP BIBLIOGRAPHY. +// 0.186 8-Aug-2020 nm mmwtex.c, mmhlpa.c - add CONJECTURE, RESULT to [bib] +// keywords. +// 8-Aug-2020 nm mmpfas.c, metamath.c - print message when IMPROVE or +// MINIMIZE_WITH uses another mathbox. +// 0.185 5-Aug-2020 nm metamath.c mmcmdl.c mmhlpb.c mmpfas.c,h mmcmds.c +// mmwtex.c,h - add /INCLUDE_MATHBOXES to to IMPROVE; notify user upon ASSIGN +// from another mathbox. +// 18-Jul-2020 nm mmcmds.c, mmdata.c, mmhlpb.c, metamath.c - "PROVE =" will now +// resume the previous MM-PA session if there was one; allow "~" to start/end +// with blank (meaning first/last statement); add "@1234". +// 0.184 17-Jul-2020 nm metamath.c mmcmdl.c mmcmds.c,h mmhlpb.c mmwtex.c,h - +// add checking for mathbox independence to VERIFY MARKUP; add /MATHBOX_SKIP +// 4-Jul-2020 nm mmwtex.c - correct error msg for missing althtmldef +// 3-Jul-2020 nm metamath.c, mmhlpa.c - allow space in TOOLS> BREAK. +// 0.183 30-Jun-2020 30-Jun-2020 nm mmpars.c - refine prevention of +// WRITE SOURCE.../REWRAP from modifying comments containing "" +// (specifically, remove indentation alignment). +// 25-Jun-2020 nm metamath.c, mmcmds.c,h mmcmdl.c mmhlpb.c - add underscore +// checking in VERIFY MARKUP and add /UNDERSCORE_SKIP qualifier; also check +// for trailing space on lines. +// 20-Jun-2020 nm mmcmds.c - check for discouragement tags in *ALT, *OLD +// labels in VERIFY MARKUP. +// 19-Jun-2020 nm mminou.c,h, metamath.c, mmwtex.c - dynamically allocate +// buffer in print2() using vsnprintf() to calculate size needed +// 18-Jun-2020 nm mmpars.c - remove error check for $e <- $f assignments. See +// https://groups.google.com/d/msg/metamath/Cx_d84uorf8/0FrNYTM9BAAJ. +// 0.182 12-Apr-2020 nm mmwtex.c, mmphlpa.c - add "Claim" to bib ref types. +// 0.181 12-Feb-2020 nm (reported by David Starner) metamath.c - fix bug causing +// new axioms to be used by MINIMIZE_WITH. +// 0.180 10-Dec-2019 nm (bj 13-Sep-2019) mmpars.c - fix "line 0" in error msg +// when label clashes with math symbol +// 8-Dec-2019 nm (bj 13-Oct-2019) mmhlpa.c - improve TOOLS> HELP INSERT, DELETE +// 8-Dec-2019 nm (bj 19-Sep-2019) mminou.c - change bug 1511 to error message +// 30-Nov-2019 nm (bj 12-Oct-2019) mmwtex.c - trigger Most Recent link on +// mmtheorems.html when there is a mathbox statement (currently set.mm and +// iset.mm). +// 30-Nov-2019 nm (bj 13-Sep-2019) mmhlpa.c - improve help for TOOLS> DELETE and +// SUBSTITUTE. +// 30-Nov-2019 nm (bj 13-Sep-2019) mmwtex.c - change "g_htmlHome" in warnings to +// "htmlhome". +// 0.179 29-Nov-2019 nm (bj 22-Sep-2019) metamath.c - MINIMIZE_WITH axiom trace +// now starts from current NEW_PROOF instead of SAVEd proof. +// 23-Nov-2019 nm (bj 4-Oct-2019) metamath.c - make sure traceback flags are +// cleared after MINIMIZE_WITH +// 20-Nov-2019 nm mmhlpa.c - add url pointer to HELP WRITE SOURCE /SPLIT +// 18-Nov-2019 nm mmhlpa.c - clarify HELP WRITE SOURCE /REWRAP +// 15-Oct-2019 nm mmdata.c - add bug check info for user +// 14-Oct-2019 nm mmcmds.c - use '|->' (not 'e.') as syntax hint for maps-to +// 14-Oct-2019 nm mmwtex.c - remove extraneous . +// 0.178 10-Aug-2019 nm mminou.c - eliminate redundant fopen in fSafeOpen. +// 6-Aug-2019 nm mmwtex.c,h, mmcmds.c - Add error check for >1 line +// section name or missing closing decoration line in getSectionHeadings(). +// 4-Aug-2019 nm mmhlpb.c, mmcmdl.c, metamath.c - Add /ALLOW_NEW_AXIOMS, +// renamed /ALLOW_GROWTH to /MAY_GROW. +// 17-Jul-2019 nm mmcmdl.c, mmhlpa.c, metamath.c - Add /NO_VERSIONING to +// WRITE THEOREM_LIST. +// 17-Jul-2019 nm metamath.c - Change line of dashes between SHOW STATEMENT +// output from hardcoded 79 to current g_screenWidth. +// 0.177 27-Apr-2019 nm mmcmds.c -"set" -> "setvar" in htmlAllowedSubst. +// mmhlpb.c - fix typos in HELP IMPROVE. +// 0.176 25-Mar-2019 nm metamath.c mmcmds.h mmcmds.c mmcmdl.c mmhlpb.c - +// add /TOP_DATE_SKIP to VERIFY MARKUP. +// 0.175 8-Mar-2019 nm mmvstr.c - eliminate warning in gcc 8.3 (patch +// provided by David Starner). +// 0.174 22-Feb-2019 nm mmwtex.c - fix erroneous warning when using "[[" +// bracket escape in comment. +// 0.173 3-Feb-2019 nm mmwtex.c - fix infinite loop when "[" was the first +// character in a comment. +// 0.172 25-Jan-2019 nm mmwtex.c - comment out bug 2343 trap (not a bug). +// 0.171 13-Dec-2018 nm metamath.c, mmcmdl.c, mmhlpa.c, mmcmds.c,h, mmwtex.c,h +// - add fine-grained qualifiers to MARKUP command. +// 0.170 12-Dec-2018 nm mmwtex.c - restore line accidentally deleted in 0.169. +// 0.169 10-Dec-2018 nm metamath.c, mmcmds.c,h, mmcmdl.c, mmpars.c, mmhlpa.c, +// mmwtex.c - Add MARKUP command. +// 9-Dec-2018 nm mmwtex.c - escape literal "[" with "[[" in comments. +// 0.168 8-Dec-2018 nm metamath.c - validate that /NO_REPEATED_STEPS is used +// only with /LEMMON. +// 8-Dec-2018 nm mmcmds.c - fix bug #256 reported by Jim Kingdon +// (https://github.com/metamath/set.mm/issues/497). +// 0.167 13-Nov-2018 nm mmcmds.c - SHOW TRACE_BACK .../COUNT now uses proof +// the way it's stored (previously, it always uncompressed the proof). The +// new step count (for compressed proofs) corresponds to the step count the +// user would see on the web pages. +// 12-Nov-2018 nm mmcmds.c - added unlimited precision arithmetic +// for SHOW TRACE_BACK .../COUNT/ESSENTIAL. +// 0.166 31-Oct-2018 nm mmwtex.c - workaround Chrome anchor bug. +// 30-Oct-2018 nm mmcmds.c - put "This theorem is referenced by" after +// axioms and definitions used in HTML; use "(None)" instead of suppressing +// line if nothing is referenced. +// 0.165 20-Oct-2018 nm mmwtex.c - added ~ mmtheorems#abc type anchor +// in TOC details. mmwtex.c - fix bug (reported by Benoit Jubin) that +// changes "_" in labels to subscript. mmcmdl.c - remove unused COMPLETE +// qualifier from SHOW PROOF. mmwtex.c - enhance special cases of web page +// spacing identified by Benoit Jubin. +// 0.164 5-Sep-2018 nm mmwtex.c, mmhlpb.c - added NOTE to bib keywords. +// 14-Aug-2018 nm metamath.c - added defaultScrollMode to prevent +// SET SCROLL CONTINUOUS from reverting to PROMPTED after a SUBMIT command. +// 0.163 4-Aug-2018 nm mmwtex.c - removed 2nd "sandbox:bighdr" anchor +// in mmtheorems.html; removed Firefox and IE references; changed breadcrumb +// font to be consistent with other pages; put asterisk next to TOC entries +// that have associated comments. +// FOR FUTURE REFERENCE: search for "Thierry" in mmwtex.c to modify the link +// to tirix.org structured proof site. +// 0.162-thierry 3-Jun-2018 nm mmwtex.c - add link to tirix.org structured +// proofs. +// 0.162 3-Jun-2018 nm mmpars.c - re-enabled error check for $c not in +// outermost scope. mmhlpa.c mmhlpb.c- improve some help messages. +// mmwtex.c - added "OBSERVATION", "PROOF", AND "STATEMENT" keywords for +// WRITE BIBLIOGRAPHY. +// 0.161 2-Feb-2018 nm mmpars.c,h mmcmds.c mmwtex.c - fix wrong file name +// and line number in error messages. +// 0.160 24-Jan-2018 nm mmpars.c - fix bug introduced in version 0.158. +// 0.159 23-Jan-2018 nm mmpars.c - fix crash due to missing include file. +// 0.158 22-Jan-2018 nm mminou.c - strip CRs from Windows SUBMIT files +// run on Linux. +// 0.157 15-Jan-2018 nm Major rewrite of READ-related functions. +// Added HELP MARKUP. +// 9-Jan-2018 nm Track line numbers for error messages in included files. +// 1-Jan-2018 nm Changed HOME_DIRECTORY to ROOT_DIRECTORY. +// 31-Dec-2017 nm metamath.c mmcmdl.c,h mmpars.c,h mmcmds.c,h mminou.c,h. +// mmwtex.c mmhlpb.c mmdata.h - add virtual includes "$( Begin $[...$] $)", +// $( End $[...$] $)", "$( Skip $[...$] $)". +// 0.156 8-Dec-2017 nm mmwtex.c - fix bug that incorrectly gave "verify markup" +// errors when there was a mathbox statement without an "extended" section. +// 0.155 8-Oct-2017 nm mmcmdl.c - restore accidentally removed HELP HTML; +// mmhlpb.c mmwtex.c mmwtex.h,c mmcmds.c metamath.c - improve HELP and make +// other cosmetic changes per Benoit Jubin's suggestions. +// 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; +// metamath.c - enforce minimum screen width = 3 to prevent crash reported +// by Benoit Jubin. +// 0.151 20-Sep-2017 nm mmwtex.c - better matching to insert space between +// A and y in "E. x e. ran A y R x" to prevent spurious spaces in thms rncoeq, +// dfiun3g as reported by Benoit Jubin. +// 0.150 26-Aug-2017 nm mmcmds.c,mmwtex.h - fix hyperlink for Distinct variable +// etc. lists so that it will point to mmset.html on other Explorers like NF. +// Move the "Dummy variables..." to print after the "Proof of Theorem..." +// line. +// 0.149 21-Aug-2017 nm mmwtex.c,h mmcmds.c mmhlpb.c - add a subsubsection +// "tiny" header with separator "-.-." to table of contents and theorem list; +// see HELP WRITE THEOREM_LIST. +// 21-Aug-2017 nm mmcmds.c - remove bug check 255. +// 19-Aug-2017 nm mmcmds.c - change mmset.html links to +// ../mpeuni/mmset.html so they will work in NF Explorer etc. +// 0.148 14-Aug-2017 nm mmcmds.c - hyperlink "Dummy variable(s)". +// 0.147 13-Aug-2017 nm mmcmds.c,h - add "Dummy variable x is distinct from all +// other variables." to proof web page. +// 0.146 26-Jun-2017 nm mmwtex.c - fix handling of local labels in +// 'show proof.../tex' (bug 2341 reported by Eric Parfitt). +// 0.145 16-Jun-2017 nm metamath.c mmpars.c - fix bug 1741 during +// MINIMIZE_WITH; mmpfas.c - make duplicate bug numbers unique; mmhlpa.c +// mmhlpb.c - adjust to prevent lcc compiler "Function too big for the +// optimizer". +// 29-May-2017 nm mmwtex.c mmhlpa.c - take out extraneous ... +// markup tags in HTML output so w3c validator will pass. +// 0.144 15-May-2017 nm metamath.c mmcmds.c - add "(Revised by..." tag for +// conversion of legacy .mm's if there is a 2nd date under the proof. +// 0.143 14-May-2017 nm metamath.c mmdata.c,h mmcmdl.c mmcmds.c mmhlpb.c - +// added SET CONTRIBUTOR; for missing "(Contributed by..." use date +// below proof if it exists, otherwise use today's date, in order to update +// old .mm files. +// 14-May-2017 Ari Ferrera - mmcmds.c - fix memory leaks in ERASE. +// 0.142 12-May-2017 nm metamath.c mmdata.c,h mmcmds.c - added +// "#define DATE_BELOW_PROOF" in mmdata.h that if uncommented, will enable +// use of the (soon-to-be obsolete) date below the proof. +// 4-May-2017 Ari Ferrera - mmcmds.c metamath.c mmdata.c mmcmdl.c +// mminou.c mminou.h mmcmdl.h mmdata.h - fixed memory leaks and warnings +// found by valgrind. +// 3-May-2017 nm - metamath.c mmdata.c,h mmcmds.c,h mmpars.c,h mmhlpb.c +// mmcmdl.c mmwtex.c - added xxChanged flags to statement structure so +// that any part of the source can be changed; removed /CLEAN qualifier +// of WRITE SOURCE; automatically put "(Contributed by ?who?..." during +// SAVE NEW_PROOF or SAVE PROOF when it is missing; more VERIFY MARKUP +// checking. +// 0.141 2-May-2017 nm mmdata.c, metamath.c, mmcmds.c, mmhlpb.c - use +// getContrib() date for WRITE RECENT instead of date below proof. This lets +// us list recent $a's as well as $p's. Also, add caching to getContrib() for +// speedup. +// 0.140 1-May-2017 nm mmwtex.c, mmcmds.c, metamath.c - fix some LaTeX issues +// reported by Ari Ferrera. +// 0.139 2-Jan-2017 nm metamath.c - print only one line for +// 'save proof * /compressed/fast'. +// 0.138 26-Dec-2016 nm mmwtex.c - remove extraneous causing w3c +// validation failure; put space after 1st x in "F/ x x = x"; +// mmcmds.c - added checking for lines > 79 chars in VERIFY MARKUP; +// mmcmds.c, mmcmdl.c, metamath.c, mmhlpb.c, mmcmds.h - added /VERBOSE to +// VERIFY MARKUP. +// 0.137 20-Dec-2016 nm mmcmds.c - check ax-XXX $a vs axXXX $p label convention +// in 'verify markup'. +// 18-Dec-2016 nm mmwtex.c, mmpars.c, mmdata.h - use true "header area" +// between successive $a/$p for getSectionHeadings() mmcmds.c - add +// header comment checking. +// 13-Dec-2016 nm mmdata.c,h - enhanced compareDates() to treat empty string as +// older date. +// 13-Dec-2016 nm metamath.c, mmcmds.c - moved mm* and Microsoft illegal file +// name label check to verifyMarkup() (the VERIFY MARKUP command) instead of +// checking on READ; added check of set.mm Version date to verifyMarkup(). +// 13-Dec-2016 nm mmwtex.c,h - don't treat bracketed description text with +// space as a bib label; add labelMatch parameter to writeBibliography(). +// 0.136 10-Oct-2016 mminou.c - fix resource leak bug reported by David Binderman. +// 0.135 11-Sep-2016, 14-Sep-2016 metamath.c, mmpfas.c,h, mmdata.c,h, +// mmpars.c,h mmcmds.c, mmcmdl.c, mmhlpb.c - added EXPAND command. +// 0.134 16-Aug-2016 mmwtex.c - added breadcrumbs to theorem pages; +// metamath.c, mmcmdl.c, mmhlpb.c, mminou.c,.h - added /TIME to SAVE PROOF, +// SHOW STATEMENT.../[ALT}HTML, MINIMIZE_WITH. +// 0.133 13-Aug-2016 mmwtex.c - improve mobile display with tag +// mmpars.c - use updated Macintosh information. +// 0.132 10-Jul-2016 metamath.c, mmcmdl.c, mmcmds.c,.h, mmdata.c,.h, mmhlpb.c, +// mmpfas.c - change "restricted" to "discouraged" to match set.mm markup +// tags; add SET DISCOURAGEMENT OFF|ON (default ON) to turn off blocking for +// convenience of advanced users. +// 6-Jul-2016 metamath.c - add "(void)" in front of "system(...)" to +// suppress -Wunused-result warning. +// 0.131 10-Jun-2016 mminou.c - reverted change of 22-May-2016 because +// 'minimize_with' depends on error message in string to prevent DV violations. +// Todo: write a DV-checking routine for 'minimize_with', then revert +// the 22-May-2016 fix for bug 126 (which only occurs when writing web +// pages for .mm file with errors). +// 9-Jun-2016 mmcmdl.c, metamath.c - added _EXIT_PA for use with +// scripts that will give an error message outside of MM-PA> rather +// than exiting metamath. +// 0.130 25-May-2016 mmpars.c - workaround clang warning about j = j; +// mmvstr.c - workaround gcc -Wstrict-overflow warning. +// 0.129 24-May-2016 mmdata.c - fix bug 1393. +// 0.128 22-May-2016 mminou.c - fixed error message going to html page +// instead of to screen, triggering bug 126. +// 0.127 10-May-2016 metamath.c, mmcmdl.c, mmhlpb.c - added /OVERRIDE to PROVE. +// 0.126 3-May-2016 metamath.c, mmdata.h, mmdata.c, mmcmds.h, mmcmds.c, +// mmcmdl.c, mmhlpb.c, mmpars.c - added getMarkupFlag() in mmdata.c; +// Added /OVERRIDE added to ASSIGN, REPLACE, IMPROVE, MINIMIZE_WITH, +// SAVE NEW_PROOF; PROVE gives warning about SAVE NEW_PROOF for locked +// proof. Added SHOW RESTRICTED command. +// 3-May-2016 m*.c - fix numerous conversion warnings provided by gcc 5.3.0. +// 0.125 10-Mar-2016 mmpars.c - fixed bug parsing /EXPLICIT/PACKED format +// 8-Mar-2016 nm mmdata.c - added "#nnn" to SHOW STATEMENT etc. to reference +// statement number e.g. SHOW STATEMENT #58 shows a1i in set.mm. +// 7-Mar-2016 nm mmwtex.c - added space between } and { in HTML output. +// 6-Mar-2016 nm mmpars.c - disabled wrapping of formula lines in +// WRITE SOURCE.../REWRAP. +// 2-Mar-2016 nm metamath.c, mmcmdl.c, mmhlpb.c - added /FAST to +// SAVE PROOF, SHOW PROOF. +// 0.123 25-Jan-2016 nm mmpars.c, mmdata.h, mmdata.c, mmpfas.c, mmcmds., +// metamath.c, mmcmdl.c, mmwtex.c - unlocked SHOW PROOF.../PACKED, +// added SHOW PROOF.../EXPLICIT. +// 0.122 14-Jan-2016 nm metamath.c, mmcmds.c, mmwtex.c, mmwtex.h - surrounded +// math HTML output with "...; added htmlcss and +// htmlfont $t commands. +// 10-Jan-2016 nm mmwtex.c - delete duplicate -4px style; metamath.c - +// add   after char on mmascii.html. +// 3-Jan-2016 nm mmwtex.c - fix bug when doing SHOW STATEMENT * /ALT_HTML after +// VERIFY MARKUP. +// 0.121 17-Nov-2015 nm metamath.c, mmcmdl.h, mmcmdl.c, mmcmds.h, mmcmds.c, +// mmwtex.h, mmwtex.c, mmdata.h, mmdata.c - +// 1. Moved WRITE BIBLIOGRAPHY code from metamath.c to its own function in +// mmwtex.c; moved qsortStringCmp() from metamath.c to mmdata.c +// 2. Added $t, comment markup, and bibliography checking to VERIFY MARKUP. +// 3. Added options to bug() bug-check interception to select aborting, +// stepping to next bug, or ignoring subsequent bugs. +// 4. SHOW STATEMENT can now use both /HTML and /ALT_HTML in same session. +// 5. Added /HTML, /ALT_HTML to WRITE THEOREM_LIST and +// WRITE RECENT_ADDITIONS. +// 0.120 7-Nov-2015 nm metamath.c, mmcmdl.c, mmpars.c - add VERIFY MARKUP. +// 4-Nov-2015 nm metamath.c, mmcmds.c/h, mmdata.c/h - move getDescription, +// getSourceIndentation from mmcmds.c to mmdata.c. +// metamath.c, mmdata.c - add and call parseDate() instead of in-line +// code; add getContrib(), getProofDate(), buildDate(), compareDates(). +// 0.119 18-Oct-2015 nm mmwtex.c - add summary TOC to Theorem List; improve +// math symbol GIF image alignment. +// 2-Oct-2015 nm metamath.c, mmpfas.c, mmwtex.c - fix miscellaneous small +// bugs or quirks. +// 0.118 18-Jul-2015 nm metamath.c, mmcmds.h, mmcmds.c, mmcmdl.c, mmhlpb.h, +// mmhlpb.c - added /TO qualifier to SHOW TRACE_BACK. See +// HELP SHOW TRACE_BACK. +// 0.117 30-May-2015 +// 1. nm mmwtex.c - move of Theorem List pages. +// 0.115 8-May-2015 nm mmwtex.c - added section header comments to +// WRITE THEOREM_LIST and broke out Table of Contents page. +// 24-Apr-2015 nm metamath.c - add # bytes to end of "---Clip out the proof"; +// reverted to no blank lines there (see 0.113 item 3). +// 0.114 22-Apr-2015 nm mmcmds.c - put [-1], [-2],... offsets on 'show +// new_proof/unknown'. +// 0.113 19-Apr-2015 so, nm metamath.c, mmdata.c +// 1. SHOW LABEL % will show statements with changed proofs +// 2. SHOW LABEL = will show the statement being proved in MM-PA +// 3. Added blank lines before, after "---------Clip out the proof" proof +// 4. Generate date only if the proof is complete. +// 0.112 15-Apr-2015 nm metamath.c - fix bug 1121 (reported by S. O'Rear); +// mmwtex.c - add "img { margin-bottom: -4px }" to CSS to align symbol GIFs; +// mmwtex.c - remove some hard coding for set.mm, for use with new nf.mm; +// metamath.c - fix comment parsing in WRITE BIBLIOGRAPHY to ignore +// math symbols. +// 0.111 22-Nov-2014 nm metamath.c, mmcmds.c, mmcmdl.c, mmhlpb.c - added +// /NO_NEW_AXIOMS_FROM qualifier to MINIMIZE_WITH; see HELP MINIMIZE_WITH. +// 21-Nov-2014 Stefan O'Rear mmdata.c, mmhlpb.c - added ~ label range specifier +// to wildcards; see HELP SEARCH. +// 0.110 2-Nov-2014 nm mmcmds.c - fixed bug 1114 (reported by Stefan O'Rear); +// metamath.c, mmhlpb.c - added "SHOW STATEMENT =" to show the statement +// being proved in MM-PA (based on patch submitted by Stefan O'Rear). +// 0.109 20-Aug-2014 nm mmwtex.c - fix corrupted HTML caused by misinterpreting +// math symbols as comment markup (math symbols with _ [ ] or ~). Also, +// allow https:// as well as http:// in ~ label markup. +// 11-Jul-2014 wl mmdata.c - fix obscure crash in debugging mode db9. +// 0.108 25-Jun-2014 nm +// (1) metamath.c, mmcmdl.c, mmhlpb.c - MINIMIZE_WITH now checks the size +// of the compressed proof, prevents $d violations, and tries forward and +// reverse statement scanning order; /NO_DISTINCT, /BRIEF, /REVERSE +// qualifiers were removed. +// (2) mminou.c - prevent hard breaks (in the middle of a word) in too-long +// lines (e.g. long URLs) in WRITE SOURCE .../REWRAP; just overflow the +// screen width instead. +// (3) mmpfas.c - fixed memory leak in replaceStatement() +// (4) mmpfas.c - suppress inf. growth with MINIMIZE_WITH idi/ALLOW_GROWTH. +// 0.107 21-Jun-2014 nm metamath.c, mmcmdl.c, mmhlpb.c - added /SIZE qualifier +// to SHOW PROOF; added SHOW ELAPSED_TIME; mmwtex.c - reformatted WRITE +// THEOREM_LIST output; now "$(", newline, "######" starts a "part". +// 0.106 30-Mar-2014 nm mmwtex.c - fix bug introduced by 0.105 that disabled +// hyperlinks on literature refs in HTML comment. metamath.c - improve +// messages. +// 0.105 15-Feb-2014 nm mmwtex.c - prevented illegal LaTeX output for certain +// special characters in comments. +// 0.104 14-Feb-2014 nm mmwtex.c - fixed bug 2312, mmcmds.c - enhanced ASSIGN +// error message. +// 0.103 4-Jan-2014 nm mmcmds.c,h - added "Allowed substitution hints" below +// the "Distinct variable groups" list on generated web pages +// mmwtex.c - added "*" to indicate DV's occur in Statement List entries. +// 0.102 2-Jan-2014 nm mminou.c - made compressed proof line wrapping more +// uniform at start of compressed part of proof. +// 0.101 27-Dec-2013 nm mmdata.h,c, mminou.c, mmcmdl.c, mmhlpb.c, mmvstr.c - +// Improved storage efficiency of /COMPRESSED proofs (but with 20% slower run +// time); added /OLD_COMPRESSION to specify old algorithm; removed end-of-line +// space after label list in old algorithm; fixed linput() bug. +// 0.100 30-Nov-2013 nm mmpfas.c - reversed statement scan order in +// proveFloating(), to speed up SHOW STATEMENT df-* /HTML; metamath.c - remove +// the unknown date place holder in SAVE NEW_PROOF; Wolf Lammen mmvstr.c - +// some cleanup. +// 0.07.99 1-Nov-2013 nm metamath.c, mmpfas.h,c, mmcmdl.h,c, mmhlpa.c, +// mmhlpb.c - added UNDO, REDO, SET UNDO commands (see HELP UNDO). +// 0.07.98 30-Oct-2013 Wolf Lammen mmvstr.c,h, mminou.c, mmpars.c, +// mmdata.c - improve code style and program structure. +// 0.07.97 20-Oct-2013 Wolf Lammen mmvstr.c,h, metamath.c - improved linput(); +// nm mmcmds.c, mmdata.c - tolerate bad proofs in SHOW TRACE_BACK etc. +// 0.07.96 20-Sep-2013 Wolf Lammen mmvstr.c - revised cat(); +// nm mmwtex.c, mminou.c - change a print2 to printLongLine to fix bug 1150. +// 0.07.95 18-Sep-2013 Wolf Lammen mmvstr.c - optimized cat(); +// nm metamath.c, mmcmds.c, mmdata.c, mmpars.c, mmpfas.c, mmvstr.c, +// mmwtex.c - suppress some clang warnings. +// 0.07.94 28-Aug-2013 Alexey Merkulov mmcmds.c, mmpars.c - fixed several +// memory leaks found by valgrind --leak-check=full --show-possibly-lost=no. +// 0.07.93 8-Jul-2013 Wolf Lammen mmvstr.c - simplified let() function; +// also many minor changes in m*.c and m*.h to assist future refactoring. +// 0.07.92 28-Jun-2013 nm metamath.c mmcmds.c,h mmcmdl.c mmhlpb.c- added +// /NO_REPEATED_STEPS for /LEMMON mode of SHOW PROOF, SHOW NEW_PROOF. +// This reverts the /LEMMON mode default display change of 31-Jan-2010 +// and invokes it when desired via /NO_REPEATED_STEPS. +// 0.07.91 20-May-2013 nm metamath.c mmpfas.c,h mmcmds.c,h mmcmdl.c +// mmhlpb.c- added /FORBID qualifier to MINIMIZE_WITH. +// 0.07.90 19-May-2013 nm metamath.c mmcmds.c mmcmdl.c mmhlpb.c - added /MATCH +// qualifier to SHOW TRACE_BACK. +// 0.07.88 18-Nov-2012 nm mmcmds.c - fixed bug 243. +// 0.07.87 17-Nov-2012 nm mmwtex.c - fixed formatting problem when label +// markup ends a comment in SHOW PROOF ... /HTML. +// 0.07.86 27-Oct-2012 nm mmcmds.c, mmwtex.c, mmwtex.h - fixed ERASE bug +// caused by imperfect re-initialization; reported by Wolf Lammen. +// 0.07.85 10-Oct-2012 nm metamath.c, mmcmdl.c, mmwtex.c, mmwtex.h, mmhlpb.c - +// added /SHOW_LEMMAS to WRITE THEOREM_LIST to bypass lemma math suppression. +// 0.07.84 9-Oct-2012 nm mmcmds.c - fixed bug in getStatementNum(). +// 0.07.83 19-Sep-2012 nm mmwtex.c - fixed bug reported by Wolf Lammen. +// 0.07.82 16-Sep-2012 nm metamath.c, mmpfas.c - fixed REPLACE infinite loop; +// improved REPLACE message for shared dummy variables. +// 0.07.81 14-Sep-2012 nm metamath.c, mmcmds.c, mmcmds.h, mmcmdl.c, mmhlpb.c +// - added FIRST, LAST, +nn, -nn where missing from ASSIGN, REPLACE, +// IMPROVE, LET STEP. Wildcards are allowed for PROVE, ASSIGN, REPLACE +// labels provided there is a unique match. +// 0.07.80 4-Sep-2012 nm metamath.c, mmpfas.c, mmpfas.h, mmcmdl.c, mmhlpb.c +// - added / 1, / 2, / 3, / SUBPROOFS to IMPROVE to specify search level. +// 0.07.79 31-Aug-2012 nm m*.c - clean up some gcc warnings. +// 0.07.78 28-Aug-2012 nm mmpfas.c - fix bug in 0.07.77. +// 0.07.77 25-Aug-2012 nm metamath.c, mmpfas.c - Enhanced IMPROVE algorithm to +// allow non-shared dummy variables in unknown steps. +// 0.07.76 22-Aug-2012 nm metamath.c, mmpfas.c, mmcmdl.c, mmhlpb.c - +// Enhanced IMPROVE algorithm to also try REPLACE algorithm. +// 0.07.75 14-Aug-2012 nm metamath.c - MINIMIZE_WITH now checks current +// mathbox (but not other mathboxes) even if /INCLUDE_MATHBOXES is omitted. +// 0.07.74 18-Mar-2012 nm mmwtex.c, mmcmds.c, metamath.c - improved texToken() +// error message. +// 0.07.73 26-Dec-2011 nm mmwtex.c, mmpars.c - added ... in +// comments for passing through raw HTML code into HTML files generated with +// SHOw STATEMENT xxx / HTML. +// 0.07.72 25-Dec-2011 nm (obsolete). +// 0.07.71 10-Nov-2011 nm metamath.c, mmcmdl.c - added /REV to MINIMIZE_WITH. +// 0.07.70 6-Aug-2011 nm mmwtex.c - fix handling of double quotes inside +// of htmldef strings to match spec in Metamath book Appendix A p. 156. +// 0.07.69 9-Jul-2011 nm mmpars.c, mmvstr.c - Untab file in WRITE SOURCE ... /REWRAP. +// 0.07.68 3-Jul-2011 nm metamath.c, mminou.h, mminou.c - Nested SUBMIT calls +// (SUBMIT calls inside of a SUBMIT command file) are now allowed. +// Also, mmdata.c - fix memory leak. +// 0.07.67 2-Jul-2011 nm metamath.c, mmcmdl.c, mmhlpa.c - Added TAG command +// to TOOLS. See HELP TAG under TOOLS. (The old special-purpose TAG command +// was renamed to UPDATE.) +// 0.07.66 1-Jul-2011 nm metamath.c, mmcmds.c, mmpars.c, mmpars.h - Added code +// to strip spurious "$( [?] $)" in WRITE SOURCE ... /CLEAN output. +// 0.07.65 30-Jun-2011 nm mmwtex.c - Prevent processing [...] bibliography +// brackets inside of `...` math strings in comments. +// 0.07.64 28-Jun-2011 nm metamath.c, mmcmdl.c - Added /INCLUDE_MATHBOXES +// qualifier to MINIMIZE_WITH; without it, MINIMIZE_WITH * will skip +// checking user mathboxes. +// 0.07.63 26-Jun-2011 nm mmwtex.c - check that .gifs exist for htmldefs. +// 0.07.62 18-Jun-2011 nm mmpars.c - fixed bug where redeclaration of active +// $v was not detected. +// 0.07.61 12-Jun-2011 nm mmpfas.c, mmcmds.c, metamath.c, mmhlpb.c - added +// /FORMAT and /REWRAP qualifiers to WRITE SOURCE to format according to set.mm +// conventions - set HELP WRITE SOURCE. +// 0.07.60 7-Jun-2011 nm mmpfas.c - fixed bug 1805 which occurred when doing +// MINIMIZE_WITH weq/ALLOW_GROWTH after DELETE DELETE FLOATING_HYPOTHESES. +// 0.07.59 11-Dec-2010 nm mmpfas.c - increased default SET SEARCH_LIMIT from +// 10000 to 25000 to accommodate df-plig web page in set.mm. +// 0.07.58 9-Dec-2010 nm mmpars.c - detect if same symbol is used with both +// $c and $v, in order to conform with Metamath spec. +// 0.07.57 19-Oct-2010 nm mmpars.c - fix bug causing incorrect line count +// for error messages when non-ASCII character was found; mminou.h - +// increase SET WIDTH maximum from 999 to 9999. +// 0.07.56 27-Sep-2010 nm mmpars.c, mmpfas.c - check for $a's with +// one token e.g. "$a wff $."; if found, turn SET EMPTY_SUBSTITUTION ON +// automatically. (Suggested by Mel O'Cat; patent pending.) +// 0.07.55 26-Sep-2010 nm mmunif.c, mmcmds.c, mmunif.h - check for mismatched +// brackets in all $a's, so that if there are any, the bracket matching +// algorithm (for fewer ambiguous unifications) in mmunif.c will be turned +// off. +// 0.07.54 25-Sep-2010 nm mmpars.c - added $f checking to conform to the +// current Metamath spec, so footnote 2 on p. 92 of Metamath book is +// no longer applicable. +// 0.07.53 24-Sep-2010 nm mmveri.c - fixed bug(2106), reported by Michal Burger. +// 0.07.52 14-Sep-2010 nm metamath.c, mmwtex.h, mmwtex.c, mmcmds.c, +// mmcmdl.c, mmhlpb.c - rewrote the LaTeX output for easier hand-editing +// and embedding in LaTeX documents. The old LaTeX output is still +// available with /OLD_TEX on OPEN TEX, SHOW STATEMENT, and SHOW PROOF, +// but it is obsolete and will be deleted eventually if no one objects. The +// new /TEX output also replaces the old /SIMPLE_TEX, which was removed. +// 0.07.51 9-Sep-2010 Stefan Allen mmwtex.c - put hyperlinks on hypothesis +// label references in SHOW STATEMENT * /HTML, ALT_HTML output. +// 0.07.50 21-Feb-2010 nm mminou.c - "./metamath < empty", where "empty" is a +// 0-byte file, now exits metamath instead of producing an infinite loop. +// Also, ^D now exits metamath. Reported by Cai Yufei. +// 0.07.49 31-Jan-2010 nm mmcmds.c - Lemmon-style proofs (SHOW PROOF xxx +// /LEMON/RENUMBER) no longer have steps with dummy labels; instead, steps +// are now the same as in HTML page proofs. (There is a line to comment +// out if you want to revert to old behavior.) +// 0.07.48 11-Sep-2009 nm mmpars.c, mm, mmvstr.c, mmdata.c - Added detection of +// non-whitespace around keywords (mmpars.c); small changes to eliminate +// warnings in gcc 3.4.4 (mmvstr.c, mmdata.c). +// 0.07.47 2-Aug-2009 nm mmwtex.c, mmwtex.h - added user name to mathbox pages. +// 0.07.46 24-Jul-2009 nm metamath.c, mmwtex.c - changed name of sandbox +// to "mathbox". +// 0.07.45 15-Jun-2009 nm metamath.c, mmhlpb.c - put "!" before each line of +// SET ECHO ON output to make them easy to identity for creating scripts. +// 0.07.44 12-May-2009 Stefan Allan, nm metamath.c, mmcmdl.c, mmwtex.c - +// added SHOW STATEMENT / MNEMONICS - see HELP SHOW STATEMENT. +// 0.07.43 29-Aug-2008 nm mmwtex.c - workaround for Unicode huge font bug in +// FireFox 3. +// 0.07.42 8-Aug-2008 nm metamath.c - added sandbox, Hilbert Space colors to +// Definition List. +// 0.07.41 29-Jul-2008 nm metamath.c, mmwtex.h, mmwtex.c - Added handling of +// sandbox section of Metamath Proof Explorer web pages. +// 0.07.40 6-Jul-2008 nm metamath.c, mmcmdl.c, mmhlpa.c, mmhlpb.c - Added +// / NO_VERSIONING qualifier for SHOW STATEMENT, so website can be regenerated +// in place with less temporary space required. Also, the wildcard trigger +// for mmdefinitions.html, etc. is more flexible (see HELP HTML). +// 0.07.39 21-May-2008 nm metamath.c, mmhlpb.c - Added wildcard handling to +// statement label in SHOW TRACE_BACK. All wildcards now allow +// comma-separated lists [i.e. matchesList() instead of matches()]. +// 0.07.38 26-Apr-2008 nm metamath.c, mmdata.h, mmdata.c, mmvstr.c, mmhlpb.c - +// Enhanced / EXCEPT qualifier for MINIMIZE_WITH to handle comma-separated +// wildcard list. +// 0.07.37 14-Apr-2008 nm metamath.c, mmcmdl.c, mmhlpb.c - Added / JOIN +// qualifier to SEARCH. +// 0.07.36 7-Jan-2008 nm metamath.c, mmcmdl.c, mmhlpb.c - Added wildcard +// handling for labels in SHOW USAGE. +// 0.07.35 2-Jan-2008 nm mmcmdl.c, metamath.c, mmhlpb.c - Changed keywords +// COMPACT to PACKED and COLUMN to START_COLUMN so that SAVE/SHOW proof can use +// C to abbreviate COMPRESSED. (PACKED format is supported but "unofficial," +// used mainly for debugging purposes, and is not listed in HELP SAVE +// PROOF.) +// 0.07.34 19-Nov-2007 nm mmwtex.c, mminou.c - Added tooltips to proof step +// hyperlinks in SHOW STATEMENT.../HTML,ALT_HTML output (suggested by Reinder +// Verlinde). +// 0.07.33 19-Jul-2007 nm mminou.c, mmvstr.c, mmdata.c, mmword.c - added fflush +// after each printf() call for proper behavior inside emacs (suggested by +// Frederic Line). +// 0.07.32 29-Apr-2007 nm mminou.c - fSafeOpen now stops at gap; e.g. if ~2 +// doesn't exist, ~1 will be renamed to ~2, but any ~3, etc. are not touched. +// 0.07.31 5-Apr-2007 nm mmwtex.c - Don't make "_" in hyperlink a subscript. +// 0.07.30 8-Feb-2007 nm mmcmds.c, mmwtex.c Added HTML statement number info to +// SHOW STATEMENT.../FULL; friendlier "Contents+1" link in mmtheorems*.html. +// 0.07.29 6-Feb-2007 Jason Orendorff mmpfas.c - Patch to eliminate the +// duplicate "Exceeded trial limit at step n" messages. +// 0.07.28 22-Dec-2006 nm mmhlpb.c - Added info on quotes to HELP LET. +// 0.07.27 23-Oct-2006 nm metamath.c, mminou.c, mmhlpa.c, mmhlpb.c - Added +// / SILENT qualifier to SUBMIT command. +// 0.07.26 12-Oct-2006 nm mminou.c - Fixed bug when SUBMIT file was missing +// a new-line at end of file (reported by Marnix Klooster). +// 0.07.25 10-Oct-2006 nm metamath.c - Fixed bug invoking TOOLS as a ./metamath +// command-line argument. +// 0.07.24 25-Sep-2006 nm mmcmdl.c Fixed bug in +// SHOW NEW_PROOF/START_COLUMN nn/LEM. +// 0.07.23 31-Aug-2006 nm mmwtex.c - Added Home and Contents links to bottom of +// WRITE THEOREM_LIST pages. +// 0.07.22 26-Aug-2006 nm metamath.c, mmcmdl.c, mmhlpb.c - Changed 'IMPROVE +// STEP ' to 'IMPROVE ' for user convenience and to be consistent +// with ASSIGN . +// 0.07.21 20-Aug-2006 nm mmwtex.c - Revised small colored numbers so that all +// colors have the same grayscale brightness.. +// 0.07.20 19-Aug-2006 nm mmpars.c - Made the error "Required hypotheses may +// not be explicitly declared" in a compressed proof non-severe, so that we +// can still SAVE the proof to reformat and recover it. +// 0.07.19 11-Aug-06 nm mmcmds.c - "Distinct variable group(s)" is now +// "group" or "groups" as appropriate. +// 0.07.18 31-Jul-06 nm mmwtex.c - added table to contents to p.1 of output of +// WRITE THEOREM_LIST command. +// 0.07.17 4-Jun-06 nm mmpars.c - do not allow labels to match math symbols +// (new spec proposed by O'Cat). mmwtex.c - made theorem name 1st in title, +// for readability in Firefox tabs. +// 0.07.16 16-Apr-06 nm metamath.c, mmcmdl.c, mmpfas.c, mmhlpb.c - allow step +// to be negative (relative to end of proof) for ASSIGN, UNIFY, and LET STEP +// (see their HELPs). Added INITIALIZE USER to delete LET STEP assignments +// (see HELP INITIALIZE). Fixed bug in LET STEP (mmpfas.c). +// 0.07.15 10-Apr-06 nm metamath.c, mmvstr.c - change dates from 2-digit to +// 4-digit year; make compatible with older 2-digit year. +// 0.07.14 21-Mar-06 nm mmpars.c - fix bug 1722 when compressed proof has +// "Z" at beginning of proof instead of after a proof step. +// 0.07.13 3-Feb-06 nm mmpfas.c - minor improvement to MINIMIZE_WITH. +// 0.07.12 30-Jan-06 nm metamath.c, mmcmds.c, mmdata.c, mmdata.h, mmhlpa.c, +// mmhlpb.c - added "?" wildcard to match single character. See HELP SEARCH. +// 0.07.11 7-Jan-06 nm metamath.c, mmcmdl.c, mmhlpb.c - added EXCEPT qualifier +// to MINIMIZE_WITH. +// 0.07.10 28-Dec-05 nm metamath.c, mmcmds.c - cosmetic tweaks. +// 0.07.10 11-Dec-05 nm metamath.c, mmcmdl.c, mmhlpb.c - added ASSIGN FIRST +// and IMPROVE FIRST commands. Also enhanced READ error message. +// 0.07.9 1-Dec-05 nm mmvstr.c - added comment on how to make portable. +// 0.07.9 18-Nov-05 nm metamath.c, mminou.c, mminou.h, mmcmdl.c, mmhlpb.c - +// added SET HEIGHT command; changed SET SCREEN_WIDTH to SET WIDTH; changed +// SET HENTY_FILTER to SET JEREMY_HENTY_FILTER (to make H for HEIGHT +// unambiguous); added HELP for SET JEREMY_HENTY_FILTER. +// 0.07.8 15-Nov-05 nm mmunif.c - now detects wrong order in bracket matching +// heuristic to further reduce ambiguous unifications in Proof Assistant. +// 0.07.7 12-Nov-05 nm mmunif.c - add "[","]" and "[_","]_" bracket matching +// heuristic to reduce ambiguous unifications in Proof Assistant. +// mmwtex.c - added heuristic for HTML spacing after "sum_" token. +// 0.07.6 15-Oct-05 nm mmcmds.c,mmpars.c - fixed compressed proof algorithm +// to match spec in book (with new algorithm due to Marnix Klooster). +// Users are warned to convert proofs when the old compression is found. +// 0.07.5 6-Oct-05 nm mmpars.c - fixed bug that reset "severe error in +// proof" flag when a proof with severe error also had unknown steps. +// 0.07.4 1-Oct-05 nm mmcmds.c - ignored bug 235, which could happen for +// non-standard logics. +// 0.07.3 17-Sep-05 nm mmpars.c - reinstated duplicate local label checking to +// conform to strict spec. +// 0.07.2 19-Aug-05 nm mmwtex.c - suppressed math content for lemmas in +// WRITE THEOREMS output. +// 0.07.1 28-Jul-05 nm Added SIMPLE_TEX qualifier to SHOW STATEMENT. +// 0.07: Official 0.07 22-Jun-05 corresponding to Metamath book. +// 0.07x: Fixed to work with AMD64 with 64-bit longs by +// Waldek Hebisch; deleted unused stuff in mmdata.c. +// 0.07w: .mm date format like "$( [7-Sep-04] $)" is now +// generated and permitted (old one is tolerated too for compatibility). +// Metamath Proof Verifier - main program. +// See the book "Metamath" for description of Metamath and run instructions. + +// *************************************************************************** + +// --------------------------------------------------------------------------- #include #include @@ -738,42 +731,43 @@ void command(int argc, char *argv[]); */ int main(int argc, char *argv[]) { -/* argc is the number of arguments; argv points to an array containing them */ +// argc is the number of arguments; argv points to an array containing them #ifdef TEST_ENABLE // enable this in mmtest.h or via './build.sh -t' RUN_TESTS(); // you never get here #endif - /****** If g_listMode is set to 1 here, the startup will be Text Tools - utilities, and Metamath will be disabled ***************************/ - /* (Historically, this mode was used for the creation of a stand-alone - "TOOLS>" utility for people not interested in Metamath. This utility - was named "LIST.EXE", "tools.exe", and "tools" on VMS, DOS, and Unix - platforms respectively. The UPDATE command of TOOLS (mmword.c) was - custom-written in accordance with the version control requirements of a - company that used it; it documents the differences between two versions - of a program as C-style comments embedded in the newer version.) */ - g_listMode = 0; /* Force Metamath mode as startup */ + // ******** If g_listMode is set to 1 here, the startup will be Text + // Tools utilities, and Metamath will be disabled ********* + + // (Historically, this mode was used for the creation of a stand-alone + // "TOOLS>" utility for people not interested in Metamath. This utility + // was named "LIST.EXE", "tools.exe", and "tools" on VMS, DOS, and Unix + // platforms respectively. The UPDATE command of TOOLS (mmword.c) was + // custom-written in accordance with the version control requirements of a + // company that used it; it documents the differences between two versions + // of a program as C-style comments embedded in the newer version.) + g_listMode = 0; // Force Metamath mode as startup g_toolsMode = g_listMode; if (!g_listMode) { - /*print2("Metamath - Version %s\n", MVERSION);*/ + // print2("Metamath - Version %s\n", MVERSION); print2("Metamath - Version %s%s", MVERSION, space(27 - (long)strlen(MVERSION))); } print2("Type HELP for help, EXIT to exit.\n"); - /* Allocate big arrays */ + // Allocate big arrays initBigArrays(); - /* Set the default contributor */ + // Set the default contributor let(&g_contributorName, DEFAULT_CONTRIBUTOR); - /* Process a command line until EXIT */ + // Process a command line until EXIT command(argc, argv); - /* Close logging command file */ + // Close logging command file if (g_listMode && g_listFile_fp != NULL) { fclose(g_listFile_fp); } @@ -782,13 +776,13 @@ int main(int argc, char *argv[]) { } void command(int argc, char *argv[]) { - /* Command line user interface -- this is an infinite loop; it fetches and - processes a command; returns only if the command is 'EXIT' or 'QUIT' and - never returns otherwise. */ - long argsProcessed = 0; /* Number of argv initial command-line - arguments processed so far */ + // Command line user interface -- this is an infinite loop; it fetches and + // processes a command; returns only if the command is 'EXIT' or 'QUIT' and + // never returns otherwise. + // Number of argv initial command-line arguments processed so far. + long argsProcessed = 0; - long /*c,*/ i, j, k, m, l, n, p, q, r, s /*,tokenNum*/; + long /* c, */ i, j, k, m, l, n, p, q, r, s /*, tokenNum */; long stmt, step; int subType = 0; #define SYNTAX 4 @@ -797,116 +791,115 @@ void command(int argc, char *argv[]) { vstring_def(str3); vstring_def(str4); vstring_def(str5); - nmbrString *nmbrTmpPtr; /* Pointer only; not allocated directly */ + nmbrString *nmbrTmpPtr; // Pointer only; not allocated directly nmbrString_def(nmbrTmp); nmbrString_def(nmbrSaveProof); - /*pntrString *pntrTmpPtr;*/ /* Pointer only; not allocated directly */ + // pntrString *pntrTmpPtr; // Pointer only; not allocated directly pntrString_def(pntrTmp); pntrString_def(expandedProof); flag tmpFlag; - /* proofSavedFlag tells us there was at least one - SAVE NEW_PROOF during the MM-PA session while the UNDO stack wasn't - empty, meaning that "UNDO stack empty" is no longer a reliable indication - that the proof wasn't changed. It is cleared upon entering MM-PA, and - set by SAVE NEW_PROOF. */ + // proofSavedFlag tells us there was at least one + // SAVE NEW_PROOF during the MM-PA session while the UNDO stack wasn't + // empty, meaning that "UNDO stack empty" is no longer a reliable indication + // that the proof wasn't changed. It is cleared upon entering MM-PA, and + // set by SAVE NEW_PROOF. flag proofSavedFlag = 0; - /* Variables for SHOW PROOF */ - flag pipFlag; /* Proof-in-progress flag */ - long outStatement; /* Statement for SHOW PROOF or SHOW NEW_PROOF */ - flag explicitTargets; /* For SAVE PROOF /EXPLICIT */ + // Variables for SHOW PROOF + flag pipFlag; // Proof-in-progress flag + long outStatement; // Statement for SHOW PROOF or SHOW NEW_PROOF + flag explicitTargets; // For SAVE PROOF /EXPLICIT long startStep; long endStep; - /* long startIndent; */ - long endIndent; /* Also for SHOW TRACE_BACK */ - flag essentialFlag; /* Also for SHOW TRACE_BACK */ - flag renumberFlag; /* Flag to use essential step numbering */ + // long startIndent; + long endIndent; // Also for SHOW TRACE_BACK + flag essentialFlag; // Also for SHOW TRACE_BACK + flag renumberFlag; // Flag to use essential step numbering flag unknownFlag; flag notUnifiedFlag; flag reverseFlag; long detailStep; - flag noIndentFlag; /* Flag to use non-indented display */ - long splitColumn; /* Column at which formula starts in non-indented display */ - flag skipRepeatedSteps; /* NO_REPEATED_STEPS qualifier */ - flag texFlag; /* Flag for TeX */ - flag saveFlag; /* Flag to save in source */ - flag fastFlag; /* Flag for SAVE PROOF.../FAST */ - long indentation; /* Number of spaces to indent proof */ - vstring_def(labelMatch); /* SHOW PROOF ", g_Statement[stmt].labelName, "", - str4, "", NULL), /* Description */ - " ", /* Start continuation line with space */ - "\""); /* Don't break inside quotes e.g. "Arial Narrow" */ + str4, "", NULL), // Description + " ", // Start continuation line with space + "\""); // Don't break inside quotes e.g. "Arial Narrow" - g_showStatement = stmt; /* For printTexComment */ - g_outputToString = 0; /* For printTexComment */ + g_showStatement = stmt; // For printTexComment + g_outputToString = 0; // For printTexComment g_texFilePtr = list2_fp; - printTexComment(str3, /* Sends result to g_texFilePtr */ - 0, /* 1 = htmlCenterFlag */ - PROCESS_EVERYTHING, /* actionBits */ - 1 /* 1 = fileCheck */ ); + printTexComment(str3, // Sends result to g_texFilePtr + 0, // 1 = htmlCenterFlag + PROCESS_EVERYTHING, // actionBits + 1); // 1 = fileCheck g_texFilePtr = NULL; - g_outputToString = 1; /* Restore after printTexComment */ + g_outputToString = 1; // Restore after printTexComment - /* Get HTML hypotheses => assertion */ + // Get HTML hypotheses => assertion free_vstring(str4); str4 = getTexOrHtmlHypAndAssertion(stmt); printLongLine(cat("" : - cat(" BGCOLOR=", PURPLISH_BIBLIO_COLOR, ">", NULL), - */ - + // (s < g_extHtmlStmt) ? + // ">" : + // cat(" BGCOLOR=", PURPLISH_BIBLIO_COLOR, ">", NULL), (stmt < g_extHtmlStmt) ? ">" : (stmt < g_mathboxStmt) @@ -2350,30 +2336,30 @@ void command(int argc, char *argv[]) { "", str4, "", NULL), - " ", /* Start continuation line with space */ - "\""); /* Don't break inside quotes e.g. "Arial Narrow" */ + " ", // Start continuation line with space + "\""); // Don't break inside quotes e.g. "Arial Narrow" g_outputToString = 0; fprintf(list2_fp, "%s", g_printString); free_vstring(g_printString); - if (n >= i /*RECENT_COUNT*/) break; /* We're done */ + if (n >= i /* RECENT_COUNT */) break; // We're done - /* Put separator row if not last theorem */ + // Put separator row if not last theorem g_outputToString = 1; printLongLine(cat("", " ", NULL), - " ", /* Start continuation line with space */ - "\""); /* Don't break inside quotes e.g. "Arial Narrow" */ - - /* Put the previous, current, and next statement - labels in HTML comments so a script can use them to update - web site incrementally. This would be done by searching - for "For script" and gather label between = and --> then - regenerate just those statements. Previous and next labels - are included to prevent dead links if they don't exist yet. */ - /* This section can be deleted without side effects */ - /* Find the previous statement with a web page */ + " ", // Start continuation line with space + "\""); // Don't break inside quotes e.g. "Arial Narrow" + + // Put the previous, current, and next statement + // labels in HTML comments so a script can use them to update + // web site incrementally. This would be done by searching + // for "For script" and gather label between = and --> then + // regenerate just those statements. Previous and next labels + // are included to prevent dead links if they don't exist yet. + // This section can be deleted without side effects. + // Find the previous statement with a web page. j = 0; for (q = stmt - 1; q >= 1; q--) { if (g_Statement[q].type == (char)p_ || @@ -2382,14 +2368,14 @@ void command(int argc, char *argv[]) { break; } } - /* 13-Dec-2018 nm This isn't used anywhere yet. But fix error - in current label and also identify previous, current, next */ + // 13-Dec-2018 nm This isn't used anywhere yet. But fix error + // in current label and also identify previous, current, next. if (j) print2("\n", g_Statement[j].labelName); - /* Current statement */ + // Current statement print2("\n", g_Statement[stmt].labelName); - /* Find the next statement with a web page */ + // Find the next statement with a web page j = 0; for (q = stmt + 1; q <= g_statements; q++) { if (g_Statement[q].type == (char)p_ || @@ -2405,28 +2391,28 @@ void command(int argc, char *argv[]) { fprintf(list2_fp, "%s", g_printString); free_vstring(g_printString); } - } /* Next stmt - statement number */ - /* Decrement date */ + } // Next stmt - statement number + // Decrement date if (k > 1) { - k--; /* Decrement day */ + k--; // Decrement day } else { - k = 31; /* Non-existent day 31's will never match, which is OK */ + k = 31; // Non-existent day 31's will never match, which is OK if (l > 1) { - l--; /* Decrement month */ + l--; // Decrement month } else { - l = 12; /* Dec */ - m --; /* Decrement year */ + l = 12; // Dec + m --; // Decrement year } } - } /* next while - Scan next date */ + } // next while - Scan next date - /* Discard the input file up to the special "" comment */ + // Discard the input file up to the special "" comment while (1) { if (!linput(list1_fp, NULL, &str1)) { print2( "?Error: Could not find \"\" line in input file \"%s\".\n", g_fullArg[2]); - tmpFlag = 1; /* Error flag to recover input file */ + tmpFlag = 1; // Error flag to recover input file break; } if (!strcmp(str1, "")) { @@ -2436,14 +2422,14 @@ void command(int argc, char *argv[]) { } if (tmpFlag) goto wrrecent_error; - /* Transfer the rest of the input file */ + // Transfer the rest of the input file while (1) { if (!linput(list1_fp, NULL, &str1)) { break; } - /* Update the date stamp at the bottom of the HTML page. */ - /* This is just a nicety; no error check is done. */ + // Update the date stamp at the bottom of the HTML page. + // This is just a nicety; no error check is done. if (!strcmp("This page was last updated on ", left(str1, 30))) { let(&str1, cat(left(str1, 30), date(), ".", NULL)); } @@ -2457,36 +2443,36 @@ void command(int argc, char *argv[]) { fclose(list1_fp); fclose(list2_fp); if (tmpFlag) { - /* Recover input files in case of error */ - remove(g_fullArg[2]); /* Delete output file */ + // Recover input files in case of error + remove(g_fullArg[2]); // Delete output file + // Restore input file name rename(cat(g_fullArg[2], "~1", NULL), g_fullArg[2]); - /* Restore input file name */ print2("?The file \"%s\" was not modified.\n", g_fullArg[2]); } continue; - } /* End of "WRITE RECENT_ADDITIONS" */ + } // End of "WRITE RECENT_ADDITIONS" if (cmdMatches("SHOW LABELS")) { linearFlag = 0; if (switchPos("LINEAR")) linearFlag = 1; if (switchPos("ALL")) { - m = 1; /* Include $e, $f statements */ + m = 1; // Include $e, $f statements print2( "The labels that match are shown with statement number, label, and type.\n"); } else { - m = 0; /* Show $a, $p only */ + m = 0; // Show $a, $p only print2( "The assertions that match are shown with statement number, label, and type.\n"); } j = 0; k = 0; - let(&str2, ""); /* Line so far */ -#define COL 20 /* Column width */ -#define MIN_SPACE 2 /* At least this many spaces between columns */ + let(&str2, ""); // Line so far +#define COL 20 // Column width +#define MIN_SPACE 2 // At least this many spaces between columns for (i = 1; i <= g_statements; i++) { - if (!g_Statement[i].labelName[0]) continue; /* No label */ + if (!g_Statement[i].labelName[0]) continue; // No label if (!m && g_Statement[i].type != (char)p_ && - g_Statement[i].type != (char)a_) continue; /* No /ALL switch */ + g_Statement[i].type != (char)a_) continue; // No /ALL switch if (!matchesList(g_Statement[i].labelName, g_fullArg[2], '*', '?')) { continue; } @@ -2495,31 +2481,31 @@ void command(int argc, char *argv[]) { g_Statement[i].labelName, " $", chr(g_Statement[i].type), NULL)); if (!str2[0]) { - j = 0; /* # of fields on line so far */ + j = 0; // # of fields on line so far } k = ((long)strlen(str2) + MIN_SPACE > j * COL) + // Position before new str1 starts ? (long)strlen(str2) + MIN_SPACE : j * COL; - /* Position before new str1 starts */ if (k + (long)strlen(str1) > g_screenWidth || linearFlag) { if (j == 0) { - /* In case of huge label, force it out anyway */ + // In case of huge label, force it out anyway printLongLine(str1, "", " "); } else { - /* Line width exceeded, postpone adding str1 */ + // Line width exceeded, postpone adding str1 print2("%s\n", str2); let(&str2, str1); j = 1; } } else { - /* Add new field to line */ + // Add new field to line if (j == 0) { - let(&str2, str1); /* Don't put space before 1st label on line */ + let(&str2, str1); // Don't put space before 1st label on line } else { let(&str2, cat(str2, space(k - (long)strlen(str2)), str1, NULL)); } j++; } - } /* next i */ + } // next i if (str2[0]) { print2("%s\n", str2); free_vstring(str2); @@ -2534,46 +2520,46 @@ void command(int argc, char *argv[]) { } if (cmdMatches("SHOW SOURCE")) { - /* Currently, SHOW SOURCE only handles one statement at a time, - so use getStatementNum(). Eventually, SHOW SOURCE may become - obsolete; I don't think anyone uses it. */ + // Currently, SHOW SOURCE only handles one statement at a time, + // so use getStatementNum(). Eventually, SHOW SOURCE may become + // obsolete; I don't think anyone uses it. s = getStatementNum(g_fullArg[2], - 1/*startStmt*/, - g_statements + 1 /*maxStmt*/, - 1/*aAllowed*/, - 1/*pAllowed*/, - 1/*eAllowed*/, - 1/*fAllowed*/, - 0/*efOnlyForMaxStmt*/, - 1/*uniqueFlag*/); + 1, // startStmt + g_statements + 1, // maxStmt + 1, // aAllowed + 1, // pAllowed + 1, // eAllowed + 1, // fAllowed + 0, // efOnlyForMaxStmt + 1); // uniqueFlag if (s == -1) { - continue; /* Error msg was provided */ + continue; // Error msg was provided } - g_showStatement = s; /* Update for future defaults */ + g_showStatement = s; // Update for future defaults free_vstring(str1); - str1 = outputStatement(g_showStatement, /* cleanFlag */ - 0 /* reformatFlag */); - let(&str1,edit(str1,128)); /* Trim trailing spaces */ + str1 = outputStatement(g_showStatement, // cleanFlag + 0); // reformatFlag + let(&str1,edit(str1,128)); // Trim trailing spaces if (str1[strlen(str1)-1] == '\n') let(&str1, left(str1, (long)strlen(str1) - 1)); printLongLine(str1, "", ""); - free_vstring(str1); /* Deallocate vstring */ + free_vstring(str1); // Deallocate vstring continue; - } /* if (cmdMatches("SHOW SOURCE")) */ + } // if (cmdMatches("SHOW SOURCE")) if (cmdMatches("SHOW STATEMENT") && ( switchPos("HTML") || switchPos("BRIEF_HTML") || switchPos("ALT_HTML") || switchPos("BRIEF_ALT_HTML"))) { - /* Special processing for the / HTML qualifiers - for each matching - statement, a .html file is opened, the statement is output, - and depending on statement type a proof or other information - is output. */ + // Special processing for the / HTML qualifiers - for each matching + // statement, a .html file is opened, the statement is output, + // and depending on statement type a proof or other information + // is output. noVersioning = (switchPos("NO_VERSIONING") != 0); - i = 5; /* # arguments with only / HTML or / ALT_HTML */ + i = 5; // # arguments with only / HTML or / ALT_HTML if (noVersioning) i = i + 2; if (switchPos("TIME")) i = i + 2; if (g_rawArgs != i) { @@ -2608,57 +2594,55 @@ void command(int argc, char *argv[]) { q = 0; - /* Special feature: if the match statement starts with "*", we - will also output mmascii.html, mmtheoremsall.html, and - mmdefinitions.html. So, with - SHOW STATEMENT * / HTML - these will be output plus all statements; with - SHOW STATEMENT *! / HTML - these will be output with no statements (since ! is illegal in a - statement label); with - SHOW STATEMENT ?* / HTML - all statements will be output, but without mmascii.html etc. */ + // Special feature: if the match statement starts with "*", we + // will also output mmascii.html, mmtheoremsall.html, and + // mmdefinitions.html. So, with + // SHOW STATEMENT * / HTML + // these will be output plus all statements; with + // SHOW STATEMENT *! / HTML + // these will be output with no statements (since ! is illegal in a + // statement label); with + // SHOW STATEMENT ?* / HTML + // all statements will be output, but without mmascii.html etc. if (((char *)(g_fullArg[2]))[0] == '*' || g_briefHtmlFlag) { - s = -2; /* -2 is for ASCII table; -1 is for theorems; - 0 is for definitions */ + // -2 is for ASCII table; -1 is for theorems; 0 is for definitions + s = -2; } else { s = 1; } for (s = s + 0; s <= g_statements; s++) { - if (s > 0 && g_briefHtmlFlag) break; /* Only do summaries */ + if (s > 0 && g_briefHtmlFlag) break; // Only do summaries - /* - s = -2: mmascii.html - s = -1: mmtheoremsall.html (used to be mmtheorems.html) - s = 0: mmdefinitions.html - s > 0: normal statement - */ + // s = -2: mmascii.html + // s = -1: mmtheoremsall.html (used to be mmtheorems.html) + // s = 0: mmdefinitions.html + // s > 0: normal statement if (s > 0) { - if (!g_Statement[s].labelName[0]) continue; /* No label */ + if (!g_Statement[s].labelName[0]) continue; // No label if (!matchesList(g_Statement[s].labelName, g_fullArg[2], '*', '?')) continue; if (g_Statement[s].type != (char)a_ && g_Statement[s].type != (char)p_) continue; } - q = 1; /* Flag that at least one matching statement was found */ + q = 1; // Flag that at least one matching statement was found if (s > 0) { g_showStatement = s; } else { - /* We set it to 1 here so we will output the Metamath Proof - Explorer and not the Hilbert Space Explorer header for - definitions and theorems lists, when g_showStatement is - compared to g_extHtmlStmt in printTexHeader in mmwtex.c */ + // We set it to 1 here so we will output the Metamath Proof + // Explorer and not the Hilbert Space Explorer header for + // definitions and theorems lists, when g_showStatement is + // compared to g_extHtmlStmt in printTexHeader in mmwtex.c g_showStatement = 1; } - /*** Open the html file ***/ + // *** Open the html file *** g_htmlFlag = 1; - /* Open the html output file */ + // Open the html output file switch (s) { case -2: let(&g_texFileName, "mmascii.html"); @@ -2675,18 +2659,17 @@ void command(int argc, char *argv[]) { } print2("Creating HTML file \"%s\"...\n", g_texFileName); g_texFilePtr = fSafeOpen(g_texFileName, "w", noVersioning); - if (!g_texFilePtr) goto htmlDone; /* Couldn't open it (err msg was - provided) */ + if (!g_texFilePtr) goto htmlDone; // Couldn't open it (err msg was provided) g_texFileOpenFlag = 1; - printTexHeader((s > 0) ? 1 : 0 /*texHeaderFlag*/); + printTexHeader((s > 0) ? 1 : 0 /* texHeaderFlag */); if (!g_texDefsRead) { - /* If there was an error reading the $t xx.mm statement, - g_texDefsRead won't be set, and we should close out file and skip - further processing. Otherwise we will be attempting to process - uninitialized htmldef arrays and such. */ + // If there was an error reading the $t xx.mm statement, + // g_texDefsRead won't be set, and we should close out file and skip + // further processing. Otherwise we will be attempting to process + // uninitialized htmldef arrays and such. print2("?HTML generation was aborted due to the error above.\n"); - s = g_statements + 1; /* To force loop to exit */ - goto ABORT_S; /* Go to end of loop where file is closed out */ + s = g_statements + 1; // To force loop to exit + goto ABORT_S; // Go to end of loop where file is closed out } if (s <= 0) { @@ -2699,11 +2682,11 @@ void command(int argc, char *argv[]) { " in the database)", "

", NULL), "", "\""); } - /* 13-Oct-2006 nm todo - still appears - where is it? */ + // 13-Oct-2006 nm todo - still appears - where is it? if (!g_briefHtmlFlag) print2("

\n"); print2("\n"); @@ -2725,7 +2708,7 @@ void command(int argc, char *argv[]) { break; case 0: printLongLine(cat( - /* (in case |- suppressed) */ + // (in case |- suppressed) "", NULL), "", "\""); } - } /* next j */ - /* Close out the string now to prevent memory overflow */ + } // next j + // Close out the string now to prevent memory overflow fprintf(g_texFilePtr, "%s", g_printString); free_vstring(g_printString); break; - case -1: /* Falls through to next case */ + case -1: // Falls through to next case case 0: free_vstring(str1); if (s == 0 || g_briefHtmlFlag) { free_vstring(str1); - /* Get HTML hypotheses => assertion */ + // Get HTML hypotheses => assertion str1 = getTexOrHtmlHypAndAssertion(i); let(&str1, cat(str1, "", NULL)); } if (g_briefHtmlFlag) { - /* Get page number in mmtheorems*.html of WRITE THEOREMS */ + // Get page number in mmtheorems*.html of WRITE THEOREMS k = ((g_Statement[i].pinkNumber - 1) / - THEOREMS_PER_PAGE) + 1; /* Page # */ + THEOREMS_PER_PAGE) + 1; // Page # let(&str2, cat("", NULL)); printLongLine(str1, "", "\""); } - /* Close out the string now to prevent overflow */ + // Close out the string now to prevent overflow fprintf(g_texFilePtr, "%s", g_printString); free_vstring(g_printString); break; - } /* end switch */ - } /* next i (statement number) */ - g_outputToString = 0; /* closing will write out the string */ - free_vstring(bgcolor); /* Deallocate (to improve fragmentation) */ - } else { /* s > 0 */ + } // end switch + } // next i (statement number) + g_outputToString = 0; // closing will write out the string + free_vstring(bgcolor); // Deallocate (to improve fragmentation) + } else { // s > 0 if (printTime == 1) { - getRunTime(&timeIncr); /* This call just resets the time */ + getRunTime(&timeIncr); // This call just resets the time } - /*** Output the html statement body ***/ + // *** Output the html statement body *** typeStatement(g_showStatement, - 0 /*briefFlag*/, - 0 /*commentOnlyFlag*/, - 1 /*texFlag*/, /* means latex or html */ - 1 /*g_htmlFlag*/); + 0, // briefFlag + 0, // commentOnlyFlag + 1, // texFlag // means latex or html + 1); // g_htmlFlag if (printTime == 1) { getRunTime(&timeIncr); @@ -2911,44 +2894,45 @@ void command(int argc, char *argv[]) { timeIncr, g_texFileName); } - } /* if s <= 0 */ + } // if s <= 0 ABORT_S: - /*** Close the html file ***/ - printTexTrailer(1 /*texHeaderFlag*/); + // *** Close the html file *** + printTexTrailer(1); // texHeaderFlag fclose(g_texFilePtr); g_texFileOpenFlag = 0; free_vstring(g_texFileName); - } /* next s */ + } // next s if (!q) { - /* No matching statement was found */ + // No matching statement was found printLongLine(cat("?There is no statement whose label matches \"", g_fullArg[2], "\". ", "Use SHOW LABELS for a list of valid labels.", NULL), "", " "); continue; } - /* Complete the command processing to bypass normal SHOW STATEMENT - (non-html) below. */ + // Complete the command processing to bypass normal SHOW STATEMENT + // (non-html) below. htmlDone: continue; - } /* if (cmdMatches("SHOW STATEMENT") && switchPos("HTML")...) */ + } // if (cmdMatches("SHOW STATEMENT") && switchPos("HTML")...) - /* Write mnemosyne.txt */ + // Write mnemosyne.txt if (cmdMatches("SHOW STATEMENT") && switchPos("MNEMONICS")) { - g_htmlFlag = 1; /* Use HTML, not TeX section */ - g_altHtmlFlag = 1; /* Use Unicode, not GIF */ - /* readTexDefs() rereads based on changes to g_htmlFlag, g_altHtmlFlag */ - if (2/*error*/ == readTexDefs(0 /* 1 = check errors only */, - 1 /* 1 = GIF file existence check */ )) { - continue; /* An error occurred */ + g_htmlFlag = 1; // Use HTML, not TeX section + g_altHtmlFlag = 1; // Use Unicode, not GIF + // readTexDefs() rereads based on changes to g_htmlFlag, g_altHtmlFlag + if (2 /* error */ == readTexDefs(0, // 1 = check errors only + 1)) // 1 = GIF file existence check + { + continue; // An error occurred } let(&g_texFileName, "mnemosyne.txt"); - g_texFilePtr = fSafeOpen(g_texFileName, "w", 0/*noVersioningFlag*/); + g_texFilePtr = fSafeOpen(g_texFileName, "w", 0 /* noVersioningFlag */); if (!g_texFilePtr) { - /* Couldn't open file; error message was provided by fSafeOpen */ + // Couldn't open file; error message was provided by fSafeOpen continue; } print2("Creating Mnemosyne file \"%s\"...\n", g_texFileName); @@ -2956,7 +2940,7 @@ void command(int argc, char *argv[]) { for (s = 1; s <= g_statements; s++) { g_showStatement = s; - if (!g_Statement[s].labelName[0]) continue; /* No label */ + if (!g_Statement[s].labelName[0]) continue; // No label if (!matchesList(g_Statement[s].labelName, g_fullArg[2], '*', '?')) continue; if (g_Statement[s].type != (char)a_ @@ -2985,13 +2969,12 @@ void command(int argc, char *argv[]) { NULL)); fprintf(g_texFilePtr, "%s", str1); - /* Print hypothesis */ - free_vstring(str1); /* Free any previous allocation to str1 */ - /* getTexLongMath does not return a temporary allocation; must - assign str1 directly, not with let(). It will be deallocated - with the next let(&str1,...). */ - str1 = getTexLongMath(g_Statement[k].mathString, - k/*stmt# for err msgs*/); + // Print hypothesis + free_vstring(str1); // Free any previous allocation to str1. + // getTexLongMath does not return a temporary allocation; must + // assign str1 directly, not with let(). It will be deallocated + // with the next let(&str1,...). + str1 = getTexLongMath(g_Statement[k].mathString, k /* stmt# for err msgs */); fprintf(g_texFilePtr, "%s", str1); } @@ -3004,14 +2987,14 @@ void command(int argc, char *argv[]) { let(&str1, ""); fprintf(g_texFilePtr, "%s", str1); - free_vstring(str1); /* Free any previous allocation to str1 */ - /* getTexLongMath does not return a temporary allocation */ + free_vstring(str1); // Free any previous allocation to str1. + // getTexLongMath does not return a temporary allocation. str1 = getTexLongMath(g_Statement[s].mathString, s); fprintf(g_texFilePtr, "%s", str1); let(&str1, ""); fprintf(g_texFilePtr, "%s\n",str1); - } /* for(s=1;s j-3) { print2("At least %ld bytes of memory are free.\n",j); @@ -3220,19 +3203,19 @@ void command(int argc, char *argv[]) { "Time since last SHOW ELAPSED_TIME command = %6.2f s; total = %6.2f s\n", timeIncr, timeTotal); continue; - } /* if (cmdMatches("SHOW ELAPSED_TIME")) */ + } // if (cmdMatches("SHOW ELAPSED_TIME")) if (cmdMatches("SHOW TRACE_BACK")) { essentialFlag = 0; axiomFlag = 0; endIndent = 0; i = switchPos("ESSENTIAL"); - if (i) essentialFlag = 1; /* Limit trace to essential steps only */ + if (i) essentialFlag = 1; // Limit trace to essential steps only i = switchPos("ALL"); if (i) essentialFlag = 0; i = switchPos("AXIOMS"); - if (i) axiomFlag = 1; /* Limit trace printout to axioms */ - i = switchPos("DEPTH"); /* Limit depth of printout */ + if (i) axiomFlag = 1; // Limit trace printout to axioms + i = switchPos("DEPTH"); // Limit depth of printout if (i) endIndent = (long)val(g_fullArg[i + 1]); i = switchPos("COUNT_STEPS"); @@ -3281,8 +3264,8 @@ void command(int argc, char *argv[]) { g_showStatement = 0; for (i = 1; i <= g_statements; i++) { if (g_Statement[i].type != (char)p_) - continue; /* Not a $p statement; skip it */ - /* Wildcard matching */ + continue; // Not a $p statement; skip it + // Wildcard matching if (!matchesList(g_Statement[i].labelName, g_fullArg[2], '*', '?')) continue; @@ -3299,73 +3282,74 @@ void command(int argc, char *argv[]) { axiomFlag, matchList, traceToList, - 0 /* testOnlyFlag */, - 1 /* allow early exit */) == -1) - break; // the user aborted + 0, // testOnlyFlag + 1 // allow early exit + ) == -1) + break; // the user aborted } } - } /* next i */ + } // next i if (g_showStatement == 0) { printLongLine(cat("?There are no $p labels matching \"", g_fullArg[2], "\". ", "See HELP SHOW TRACE_BACK for matching rules.", NULL), "", " "); } - free_vstring(matchList); /* Deallocate memory */ - free_vstring(traceToList); /* Deallocate memory */ + free_vstring(matchList); // Deallocate memory + free_vstring(traceToList); // Deallocate memory continue; - } /* if (cmdMatches("SHOW TRACE_BACK")) */ + } // if (cmdMatches("SHOW TRACE_BACK")) if (cmdMatches("SHOW USAGE")) { if (switchPos("ALL")) { - m = 1; /* Always include $e, $f statements */ + m = 1; // Always include $e, $f statements } else { - m = 0; /* If wildcards are used, show $a, $p only */ + m = 0; // If wildcards are used, show $a, $p only } g_showStatement = 0; for (i = 1; i <= g_statements; i++) { - if (!g_Statement[i].labelName[0]) continue; /* No label */ + if (!g_Statement[i].labelName[0]) continue; // No label if (!m && g_Statement[i].type != (char)p_ && g_Statement[i].type != (char)a_ - /* A wildcard-free user-specified statement is always matched even - if it's a $e, i.e. it overrides omission of / ALL */ + // A wildcard-free user-specified statement is always matched even + // if it's a $e, i.e. it overrides omission of / ALL && (instr(1, g_fullArg[2], "*") || instr(1, g_fullArg[2], "?"))) - continue; /* No /ALL switch and wildcard and not $p, $a */ - /* Wildcard matching */ + continue; // No /ALL switch and wildcard and not $p, $a + // Wildcard matching if (!matchesList(g_Statement[i].labelName, g_fullArg[2], '*', '?')) continue; g_showStatement = i; recursiveFlag = 0; j = switchPos("RECURSIVE"); - if (j) recursiveFlag = 1; /* Recursive (indirect) usage */ + if (j) recursiveFlag = 1; // Recursive (indirect) usage j = switchPos("DIRECT"); - if (j) recursiveFlag = 0; /* Direct references only */ + if (j) recursiveFlag = 0; // Direct references only free_vstring(str1); str1 = traceUsage(g_showStatement, recursiveFlag, - 0 /* cutoffStmt */); + 0); // cutoffStmt - /* str1[0] will be 'Y' or 'N' depending on whether there are any - statements. str1[i] will be 'Y' or 'N' depending on whether - g_Statement[i] uses g_showStatement. */ - /* Count the number of statements k = # of 'Y' */ + // str1[0] will be 'Y' or 'N' depending on whether there are any + // statements. str1[i] will be 'Y' or 'N' depending on whether + // g_Statement[i] uses g_showStatement. + // Count the number of statements k = # of 'Y'. k = 0; if (str1[0] == 'Y') { - /* There is at least one statement using g_showStatement */ + // There is at least one statement using g_showStatement for (j = g_showStatement + 1; j <= g_statements; j++) { if (str1[j] == 'Y') { k++; } else { - if (str1[j] != 'N') bug(1124); /* Must be 'Y' or 'N' */ + if (str1[j] != 'N') bug(1124); // Must be 'Y' or 'N' } } } else { - if (str1[0] != 'N') bug(1125); /* Must be 'Y' or 'N' */ + if (str1[0] != 'N') bug(1125); // Must be 'Y' or 'N' } if (k == 0) { @@ -3393,14 +3377,14 @@ void command(int argc, char *argv[]) { } if (k != 0) { - let(&str3, " "); /* Line buffer */ + let(&str3, " "); // Line buffer for (j = g_showStatement + 1; j <= g_statements; j++) { if (str1[j] == 'Y') { - /* Since the output list could be huge, don't build giant - string (very slow) but output it line by line */ + // Since the output list could be huge, don't build giant + // string (very slow) but output it line by line. if ((long)strlen(str3) + 1 + (long)strlen(g_Statement[j].labelName) > g_screenWidth) { - /* Output and reset the line buffer */ + // Output and reset the line buffer print2("%s\n", str3); let(&str3, " "); } @@ -3411,8 +3395,8 @@ void command(int argc, char *argv[]) { free_vstring(str3); } else { print2(" (None)\n"); - } /* if (k != 0) */ - } /* next i (statement matching wildcard list) */ + } // if (k != 0) + } // next i (statement matching wildcard list) if (g_showStatement == 0) { printLongLine(cat("?There are no labels matching \"", @@ -3420,7 +3404,7 @@ void command(int argc, char *argv[]) { "See HELP SHOW USAGE for matching rules.", NULL), "", " "); } continue; - } /* if cmdMatches("SHOW USAGE") */ + } // if cmdMatches("SHOW USAGE") if (cmdMatches("SHOW PROOF") || cmdMatches("SHOW NEW_PROOF") @@ -3435,34 +3419,34 @@ void command(int argc, char *argv[]) { if (cmdMatches("SAVE NEW_PROOF") && getMarkupFlag(g_proveStatement, PROOF_DISCOURAGED)) { if (switchPos("OVERRIDE") == 0 && g_globalDiscouragement == 1) { - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis print2( ">>> ?Error: Attempt to overwrite a proof whose modification is discouraged.\n"); print2( ">>> Use SAVE NEW_PROOF ... / OVERRIDE if you really want to do this.\n"); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis continue; } else { - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis print2( ">>> ?Warning: You are overwriting a proof whose modification is discouraged.\n"); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis } } if (cmdMatches("SHOW PROOF") || cmdMatches("SAVE PROOF")) { pipFlag = 0; } else { - pipFlag = 1; /* Proof-in-progress (NEW_PROOF) flag */ + pipFlag = 1; // Proof-in-progress (NEW_PROOF) flag } if (cmdMatches("SHOW")) { saveFlag = 0; } else { - saveFlag = 1; /* The command is SAVE PROOF */ + saveFlag = 1; // The command is SAVE PROOF } printTime = 0; - if (switchPos("TIME") != 0) { /* / TIME legal in SAVE mode only */ + if (switchPos("TIME") != 0) { // / TIME legal in SAVE mode only printTime = 1; } @@ -3501,7 +3485,7 @@ void command(int argc, char *argv[]) { } } - /* Establish defaults for omitted qualifiers */ + // Establish defaults for omitted qualifiers startStep = 0; endStep = 0; endIndent = 0; @@ -3522,12 +3506,10 @@ void command(int argc, char *argv[]) { if (i) endStep = (long)val(g_fullArg[i + 1]); i = switchPos("DEPTH"); if (i) endIndent = (long)val(g_fullArg[i + 1]); - /* ESSENTIAL is retained for downwards compatibility, but is - now the default, so we ignore it. */ - /* - i = switchPos("ESSENTIAL"); - if (i) essentialFlag = 1; - */ + // ESSENTIAL is retained for downwards compatibility, but is + // now the default, so we ignore it. + // i = switchPos("ESSENTIAL"); + // if (i) essentialFlag = 1; i = switchPos("ALL"); if (i) essentialFlag = 0; if (i && switchPos("ESSENTIAL")) { @@ -3538,7 +3520,7 @@ void command(int argc, char *argv[]) { if (i) renumberFlag = 1; i = switchPos("UNKNOWN"); if (i) unknownFlag = 1; - i = switchPos("NOT_UNIFIED"); /* pip mode only */ + i = switchPos("NOT_UNIFIED"); // pip mode only if (i) notUnifiedFlag = 1; i = switchPos("REVERSE"); if (i) reverseFlag = 1; @@ -3549,9 +3531,9 @@ void command(int argc, char *argv[]) { i = switchPos("NO_REPEATED_STEPS"); if (i) skipRepeatedSteps = 1; - /* If NO_REPEATED_STEPS is specified, indentation (tree) mode will be - misleading because a hypothesis assignment will be suppressed if the - same assignment occurred earlier, i.e. it is no longer a "tree". */ + // If NO_REPEATED_STEPS is specified, indentation (tree) mode will be + // misleading because a hypothesis assignment will be suppressed if the + // same assignment occurred earlier, i.e. it is no longer a "tree". if (skipRepeatedSteps == 1 && noIndentFlag == 0) { print2("?You must specify / LEMMON with / NO_REPEATED_STEPS\n"); continue; @@ -3569,7 +3551,7 @@ void command(int argc, char *argv[]) { pipFlag = 0; saveFlag = 0; let(&labelMatch, g_fullArg[1]); - i = switchPos("PARAMETER"); /* MIDI only */ + i = switchPos("PARAMETER"); // MIDI only if (i) { let(&g_midiParam, g_fullArg[i + 1]); } else { @@ -3590,61 +3572,61 @@ void command(int argc, char *argv[]) { } } - i = switchPos("DETAILED_STEP"); /* non-pip mode only */ + i = switchPos("DETAILED_STEP"); // non-pip mode only if (i) { detailStep = (long)val(g_fullArg[i + 1]); - if (!detailStep) detailStep = -1; /* To use as flag; error message - will occur in showDetailStep() */ + // To use as flag; error message will occur in showDetailStep(). + if (!detailStep) detailStep = -1; } -/*??? Need better warnings for switch combinations that don't make sense */ +// ??? Need better warnings for switch combinations that don't make sense - /* Print a single message for "/compressed/fast" */ + // Print a single message for "/compressed/fast" if (switchPos("COMPRESSED") && fastFlag && !strcmp("*", labelMatch)) { print2( "Reformatting and saving (but not recompressing) all proofs...\n"); } - q = 0; /* Flag that at least one matching statement was found */ + q = 0; // Flag that at least one matching statement was found for (stmt = 1; stmt <= g_statements; stmt++) { - /* If pipFlag (NEW_PROOF), we will iterate exactly once. This - loop of course will be entered because there is a least one - statement, and at the end of the s loop we break out of it. */ - /* If !pipFlag, get the next statement: */ + // If pipFlag (NEW_PROOF), we will iterate exactly once. This + // loop of course will be entered because there is a least one + // statement, and at the end of the s loop we break out of it. + // If !pipFlag, get the next statement: if (!pipFlag) { - if (g_Statement[stmt].type != (char)p_) continue; /* Not $p */ + if (g_Statement[stmt].type != (char)p_) continue; // Not $p if (!matchesList(g_Statement[stmt].labelName, labelMatch, '*', '?')) continue; g_showStatement = stmt; } - q = 1; /* Flag that at least one matching statement was found */ + q = 1; // Flag that at least one matching statement was found if (detailStep) { - /* Show the details of just one step */ + // Show the details of just one step showDetailStep(g_showStatement, detailStep); continue; } - if (switchPos("STATEMENT_SUMMARY")) { /* non-pip mode only */ - /* Just summarize the statements used in the proof */ + if (switchPos("STATEMENT_SUMMARY")) { // non-pip mode only + // Just summarize the statements used in the proof proofStmtSumm(g_showStatement, essentialFlag, texFlag); continue; } - if (switchPos("SIZE")) { /* non-pip mode only */ - /* Just print the size of the stored proof and continue */ + if (switchPos("SIZE")) { // non-pip mode only + // Just print the size of the stored proof and continue let(&str1, space(g_Statement[g_showStatement].proofSectionLen)); memcpy(str1, g_Statement[g_showStatement].proofSectionPtr, (size_t)(g_Statement[g_showStatement].proofSectionLen)); n = instr(1, str1, "$."); if (n == 0) { - /* The original source truncates the proof before $. */ + // The original source truncates the proof before $. n = g_Statement[g_showStatement].proofSectionLen; } else { - /* If a proof is saved, it includes the $. (Should we - revisit or document better how/why this is done?) */ + // If a proof is saved, it includes the $. (Should we + // revisit or document better how/why this is done?) n = n - 1; } print2("The proof source for \"%s\" has %ld characters.\n", @@ -3654,11 +3636,11 @@ void command(int argc, char *argv[]) { if (switchPos("PACKED") || switchPos("NORMAL") || switchPos("COMPRESSED") || switchPos("EXPLICIT") || saveFlag) { - /*??? Add error msg if other switches were specified. (Ignore them.)*/ + // ??? Add error msg if other switches were specified. (Ignore them.) if (saveFlag) { if (printTime == 1) { - getRunTime(&timeIncr); /* This call just resets the time */ + getRunTime(&timeIncr); // This call just resets the time } } @@ -3670,23 +3652,23 @@ void command(int argc, char *argv[]) { explicitTargets = (switchPos("EXPLICIT") != 0) ? 1 : 0; - /* Get the amount to indent the proof by */ + // Get the amount to indent the proof by indentation = 2 + getSourceIndentation(outStatement); if (!pipFlag) { - parseProof(g_showStatement); /* Prints message if severe error */ + parseProof(g_showStatement); // Prints message if severe error if (g_WrkProof.errorSeverity > 1) { - /* Prevent bug trap in nmbrSquishProof -> nmbrGetSubProofLen - if proof corrupted */ + // Prevent bug trap in nmbrSquishProof -> nmbrGetSubProofLen + // if proof corrupted print2( "?The proof has a severe error and cannot be displayed or saved.\n"); continue; } if (fastFlag) { - /* Use the proof as is */ + // Use the proof as is nmbrLet(&nmbrSaveProof, g_WrkProof.proofString); } else { - /* Make sure the proof is uncompressed */ + // Make sure the proof is uncompressed nmbrLet(&nmbrSaveProof, nmbrUnsquishProof(g_WrkProof.proofString)); } } else { @@ -3700,150 +3682,150 @@ void command(int argc, char *argv[]) { if (switchPos("COMPRESSED")) { let(&str1, compressProof(nmbrSaveProof, - outStatement, /* g_showStatement or g_proveStatement based on pipFlag */ + outStatement, // g_showStatement or g_proveStatement based on pipFlag (switchPos("OLD_COMPRESSION")) ? 1 : 0)); } else { let(&str1, nmbrCvtRToVString(nmbrSaveProof, explicitTargets, - outStatement /*statemNum, used only if explicitTargets*/)); + outStatement)); // statemNum, used only if explicitTargets } if (saveFlag) { - /* ??? This is a problem when mixing html and save proof */ + // ??? This is a problem when mixing html and save proof if (g_printString[0]) bug(1114); let(&g_printString, ""); - /* Set flag for print2() to put output in g_printString instead - of displaying it on the screen */ + // Set flag for print2() to put output in g_printString instead + // of displaying it on the screen. g_outputToString = 1; } else { if (!print2("Proof of \"%s\":\n", g_Statement[outStatement].labelName)) - break; /* Break for speedup if user quit */ + break; // Break for speedup if user quit print2( "---------Clip out the proof below this line to put it in the source file:\n"); } if (switchPos("COMPRESSED")) { + // "&" is special flag to break compressed part of proof anywhere. printLongLine(cat(space(indentation), str1, " $.", NULL), - space(indentation), "& "); /* "&" is special flag to break - compressed part of proof anywhere */ + space(indentation), "& "); } else { printLongLine(cat(space(indentation), str1," $.", NULL), space(indentation), " "); } - l = (long)(strlen(str1)); /* Save length for printout below */ + l = (long)(strlen(str1)); // Save length for printout below - /* SOREAR Only generate date if the proof looks complete. - This is not intended as a grading mechanism, just trying - to avoid premature output */ + // SOREAR Only generate date if the proof looks complete. + // This is not intended as a grading mechanism, just trying + // to avoid premature output. if (!nmbrElementIn(1, nmbrSaveProof, -(long)'?')) { - /* Add a "(Contributed by...)" date if it isn't there */ + // Add a "(Contributed by...)" date if it isn't there free_vstring(str2); str2 = getContrib(outStatement, CONTRIBUTOR); - if (str2[0] == 0) { /* The is no contributor, so add one */ + if (str2[0] == 0) { // The is no contributor, so add one - /* See if there is a date below the proof (for converting old - .mm files). Someday this will be obsolete, with str3 and - str4 always returned as "". */ + // See if there is a date below the proof (for converting old + // .mm files). Someday this will be obsolete, with str3 and + // str4 always returned as "". getProofDate(outStatement, &str3, &str4); - /* If there are two dates below the proof, the first on is - the revision date and the second the "Contributed by" date. */ - if (str4[0] != 0) { /* There are 2 dates below the proof */ - let(&str5, str3); /* 1st date is Revised by... */ - let(&str3, str4); /* 2nd date is Contributed by... */ + // If there are two dates below the proof, the first on is + // the revision date and the second the "Contributed by" date. + if (str4[0] != 0) { // There are 2 dates below the proof + let(&str5, str3); // 1st date is Revised by... + let(&str3, str4); // 2nd date is Contributed by... } else { let(&str5, ""); } - /* If there is no date below proof, use today's date */ + // If there is no date below proof, use today's date if (str3[0] == 0) let(&str3, date()); let(&str4, cat("\n", space(indentation + 1), "(Contributed by ", g_contributorName, ", ", str3, ".) ", NULL)); - /* If there is a 2nd date below proof, add a "(Revised by..." - tag */ + // If there is a 2nd date below proof, add a "(Revised by... )" tag if (str5[0] != 0) { - /* Use the DEFAULT_CONTRIBUTOR ?who? because we don't - know the reviser name (using the contributor name may - be incorrect). Also, this will trigger a warning in - VERIFY MARKUP since it may be a proof shortener rather than - a reviser. */ + // Use the DEFAULT_CONTRIBUTOR ?who? because we don't + // know the reviser name (using the contributor name may + // be incorrect). Also, this will trigger a warning in + // VERIFY MARKUP since it may be a proof shortener rather than + // a reviser. let(&str4, cat(str4, "\n", space(indentation + 1), "(Revised by ", DEFAULT_CONTRIBUTOR, ", ", str5, ".) ", NULL)); } let(&str3, space(g_Statement[outStatement].labelSectionLen)); - /* str3 will have the statement's label section w/ comment */ + // str3 will have the statement's label section w/ comment memcpy(str3, g_Statement[outStatement].labelSectionPtr, (size_t)(g_Statement[outStatement].labelSectionLen)); - i = rinstr(str3, "$)"); /* The last "$)" occurrence */ - if (i != 0 /* A description comment exists */ - && saveFlag) { /* and we are saving the proof */ - /* This isn't a perfect wrapping but we assume - 'write source .../rewrap' will be done eventually. */ - /* str3 will have the updated comment */ + i = rinstr(str3, "$)"); // The last "$)" occurrence + if (i != 0 // A description comment exists + && saveFlag) { // and we are saving the proof + // This isn't a perfect wrapping but we assume + // 'write source .../rewrap' will be done eventually. + // str3 will have the updated comment let(&str3, cat(left(str3, i - 1), str4, right(str3, i), NULL)); if (g_Statement[outStatement].labelSectionChanged == 1) { - /* Deallocate old comment if not original source */ - free_vstring(str4); /* Deallocate any previous str4 content */ + // Deallocate old comment if not original source. + free_vstring(str4); // Deallocate any previous str4 content str4 = g_Statement[outStatement].labelSectionPtr; - free_vstring(str4); /* Deallocate the old content */ + free_vstring(str4); // Deallocate the old content } - /* Set flag that this is not the original source */ + // Set flag that this is not the original source g_Statement[outStatement].labelSectionChanged = 1; g_Statement[outStatement].labelSectionLen = (long)strlen(str3); - /* We do a direct assignment instead of let(&...) because - labelSectionPtr may point to the middle of the giant input - file buffer, which we don't want to deallocate */ + // We do a direct assignment instead of let(&...) because + // labelSectionPtr may point to the middle of the giant input + // file buffer, which we don't want to deallocate. g_Statement[outStatement].labelSectionPtr = str3; - /* Reset str3 without deallocating with let(), since it - was assigned to labelSectionPtr */ + // Reset str3 without deallocating with let(), since it + // was assigned to labelSectionPtr. str3 = ""; - /* Reset the cache for this statement in getContrib() */ + // Reset the cache for this statement in getContrib() str3 = getContrib(outStatement, GC_RESET_STMT); - } /* if i != 0 */ - } /* if str2[0] == 0 */ - } /* if (!nmbrElementIn(1, nmbrSaveProof, -(long)'?')) */ + } // if i != 0 + } // if str2[0] == 0 + } // if (!nmbrElementIn(1, nmbrSaveProof, -(long)'?')) if (saveFlag) { g_sourceChanged = 1; g_proofChanged = 0; if (processUndoStack(NULL, PUS_GET_STATUS, "", 0)) { - /* The UNDO stack may not be empty */ - proofSavedFlag = 1; /* UNDO stack empty no longer reliably - indicates that proof hasn't changed */ + // The UNDO stack may not be empty. + // UNDO stack empty no longer reliably indicates that + // proof hasn't changed. + proofSavedFlag = 1; } - /* Add an initial \n which will go after the "$=" and the - beginning of the proof */ + // Add an initial \n which will go after the "$=" and the + // beginning of the proof. let(&g_printString, cat("\n", g_printString, NULL)); if (g_Statement[outStatement].proofSectionChanged == 1) { - /* Deallocate old proof if not original source */ - free_vstring(str1); /* Deallocate any previous str1 content */ + // Deallocate old proof if not original source + free_vstring(str1); // Deallocate any previous str1 content str1 = g_Statement[outStatement].proofSectionPtr; - free_vstring(str1); /* Deallocate the proof section */ + free_vstring(str1); // Deallocate the proof section } - /* Set flag that this is not the original source */ + // Set flag that this is not the original source g_Statement[outStatement].proofSectionChanged = 1; if (strcmp(" $.\n", right(g_printString, (long)strlen(g_printString) - 3))) { bug(1128); } - /* Note that g_printString ends with "$.\n", but those 3 characters - should not be in the proofSection. (The "$." keyword is - added between proofSection and next labelSection when the - output is written by writeOutput.) Thus we subtract 3 - from the length. But there is no need to truncate the - string; later deallocation will take care of the whole - string. */ + // Note that g_printString ends with "$.\n", but those 3 characters + // should not be in the proofSection. (The "$." keyword is + // added between proofSection and next labelSection when the + // output is written by writeOutput.) Thus we subtract 3 + // from the length. But there is no need to truncate the + // string; later deallocation will take care of the whole + // string. g_Statement[outStatement].proofSectionLen = (long)strlen(g_printString) - 3; - /* We do a direct assignment instead of let(&...) because - proofSectionPtr may point to the middle of the giant input - file string, which we don't want to deallocate */ + // We do a direct assignment instead of let(&...) because + // proofSectionPtr may point to the middle of the giant input + // file string, which we don't want to deallocate. g_Statement[outStatement].proofSectionPtr = g_printString; - /* Reset g_printString without deallocating with let(), since it - was assigned to proofSectionPtr */ + // Reset g_printString without deallocating with let(), since it + // was assigned to proofSectionPtr g_printString = ""; g_outputToString = 0; @@ -3866,19 +3848,19 @@ void command(int argc, char *argv[]) { g_Statement[outStatement].labelName); } } else { - /*print2("\n");*/ /* Add a blank line to make clipping easier */ + // print2("\n"); // Add a blank line to make clipping easier print2(cat( "---------The proof of \"", g_Statement[outStatement].labelName, - /* "\" to clip out ends above this line.\n",NULL)); */ + // "\" to clip out ends above this line.\n",NULL)); "\" (", str((double)l), " bytes) ends above this line.\n", NULL)); - } /* End if saveFlag */ + } // End if saveFlag free_nmbrString(nmbrSaveProof); - if (pipFlag) break; /* Only one iteration for NEW_PROOF stuff */ - continue; /* to next s iteration */ - } /* end if (switchPos("PACKED") || switchPos("NORMAL") || - switchPos("COMPRESSED") || switchPos("EXPLICIT") || saveFlag) */ + if (pipFlag) break; // Only one iteration for NEW_PROOF stuff + continue; // to next s iteration + } // end if (switchPos("PACKED") || switchPos("NORMAL") || + // switchPos("COMPRESSED") || switchPos("EXPLICIT") || saveFlag) - if (saveFlag) bug(1112); /* Shouldn't get here */ + if (saveFlag) bug(1112); // Shouldn't get here if (!pipFlag) { outStatement = g_showStatement; @@ -3886,7 +3868,7 @@ void command(int argc, char *argv[]) { outStatement = g_proveStatement; } if (texFlag) { - g_outputToString = 1; /* Flag for print2 to add to g_printString */ + g_outputToString = 1; // Flag for print2 to add to g_printString if (!g_htmlFlag) { if (!g_oldTexFlag) { print2("\\begin{proof}\n"); @@ -3901,21 +3883,21 @@ void command(int argc, char *argv[]) { print2("\n"); print2("\n"); } - } else { /* g_htmlFlag */ + } else { // g_htmlFlag bug(1118); } g_outputToString = 0; - /* printTeXLongMath clears g_printString in LaTeX - mode before starting its output, so we must put out the - g_printString ourselves here */ + // printTeXLongMath clears g_printString in LaTeX + // mode before starting its output, so we must put out the + // g_printString ourselves here. fprintf(g_texFilePtr, "%s", g_printString); - free_vstring(g_printString); /* We'll clear it anyway */ - } else { /* !texFlag */ - /* Terminal output - display the statement if wildcard is used */ + free_vstring(g_printString); // We'll clear it anyway + } else { // !texFlag + // Terminal output - display the statement if wildcard is used if (!pipFlag) { if (instr(1, labelMatch, "*") || instr(1, labelMatch, "?")) { if (!print2("Proof of \"%s\":\n", g_Statement[outStatement].labelName)) - break; /* Break for speedup if user quit */ + break; // Break for speedup if user quit } } } @@ -3930,22 +3912,22 @@ void command(int argc, char *argv[]) { endIndent, essentialFlag, - /* In SHOW PROOF xxx /TEX, we use renumber steps mode so that - the first step is step 1. The step number is checked for - step 1 in mmwtex.c to prevent a spurious \\ (newline) at the - start of the proof. Note that - SHOW PROOF is not available in HTML mode, so texFlag will - always mean LaTeX mode here. */ + // In SHOW PROOF xxx /TEX, we use renumber steps mode so that + // the first step is step 1. The step number is checked for + // step 1 in mmwtex.c to prevent a spurious \\ (newline) at the + // start of the proof. Note that + // SHOW PROOF is not available in HTML mode, so texFlag will + // always mean LaTeX mode here. (texFlag ? 1 : renumberFlag), unknownFlag, notUnifiedFlag, reverseFlag, - /* In SHOW PROOF xxx /TEX, we use Lemmon mode so that the - hypothesis reference list will be available. Note that - SHOW PROOF is not available in HTML mode, so texFlag will - always mean LaTeX mode here. */ + // In SHOW PROOF xxx /TEX, we use Lemmon mode so that the + // hypothesis reference list will be available. Note that + // SHOW PROOF is not available in HTML mode, so texFlag will + // always mean LaTeX mode here. (texFlag ? 1 : noIndentFlag), splitColumn, @@ -3964,31 +3946,31 @@ void command(int argc, char *argv[]) { free_vstring(g_printString); } else { } - } else { /* g_htmlFlag */ + } else { // g_htmlFlag g_outputToString = 1; print2("
List of Syntax, ", "Axioms (ax-) and", " Definitions (\n"); - m = 0; /* Statement number map */ - let(&str3, ""); /* For storing ASCII token list in s=-2 mode */ + m = 0; // Statement number map + let(&str3, ""); // For storing ASCII token list in s=-2 mode let(&bgcolor, MINT_BACKGROUND_COLOR); for (i = 1; i <= g_statements; i++) { if (s != -2 && (i == g_extHtmlStmt || i == g_mathboxStmt)) { - /* Print a row that identifies the start of the extended - database (e.g. Hilbert Space Explorer) or the user - sandboxes */ + // Print a row that identifies the start of the extended + // database (e.g. Hilbert Space Explorer) or the user + // sandboxes. if (i == g_extHtmlStmt) { let(&bgcolor, PURPLISH_BIBLIO_COLOR); } else { @@ -2781,20 +2764,19 @@ void command(int argc, char *argv[]) { ) continue; switch (s) { case -2: - /* Print symbol to ASCII table entry */ - /* It's a $c or $v statement, so each token generates a - table row */ + // Print symbol to ASCII table entry. + // It's a $c or $v statement, so each token generates a table row. for (j = 0; j < g_Statement[i].mathStringLen; j++) { let(&str1, g_MathToken[(g_Statement[i].mathString)[j]].tokenName); - /* Output each token only once in case of multiple decl. */ + // Output each token only once in case of multiple decl. if (!instr(1, str3, cat(" ", str1, " ", NULL))) { let(&str3, cat(str3, " ", str1, " ", NULL)); free_vstring(str2); str2 = tokenToTex(g_MathToken[(g_Statement[i].mathString)[j] - ].tokenName, i/*stmt# for error msgs*/); - /* Skip any tokens (such as |- in QL Explorer) that may be suppressed */ + ].tokenName, i); // stmt# for error msgs + // Skip any tokens (such as |- in QL Explorer) that may be suppressed if (!str2[0]) continue; - /* Convert special characters to HTML entities */ + // Convert special characters to HTML entities for (k = 0; k < (signed)(strlen(str1)); k++) { if (str1[k] == '&') { let(&str1, cat(left(str1, k), "&", @@ -2811,39 +2793,40 @@ void command(int argc, char *argv[]) { right(str1, k + 2), NULL)); k = k + 3; } - } /* next k */ + } // next k printLongLine(cat("
", (g_altHtmlFlag ? cat("", NULL) : ""), str2, (g_altHtmlFlag ? "" : ""), - " ", /* This will prevent a - -4px shifted image from overlapping the - lower border of the table cell */ + // This will prevent a + // -4px shifted image from overlapping the + // lower border of the table cell. + " ", "", str1, "
", - /*"",*/ + // "", "", str((double)(g_Statement[i].pinkNumber)), " ", "", NULL)); let(&str1, cat(str2, " ", str1, NULL)); } else { - /* Get little pink (or rainbow-colored) number */ + // Get little pink (or rainbow-colored) number free_vstring(str4); str4 = pinkHTML(i); let(&str2, cat("
", str1, NULL)); } - print2("\n"); /* New line for HTML source readability */ + print2("\n"); // New line for HTML source readability printLongLine(str1, "", "\""); - + // Set s == 0 here for Web site version, + // s == s for symbol version of theorem list. if (s == 0 || g_briefHtmlFlag) { - /* Set s == 0 here for Web site version, - s == s for symbol version of theorem list */ - /* The below has been replaced by - getTexOrHtmlHypAndAssertion(i) above. */ - /*printTexLongMath(g_Statement[i].mathString, "", "", 0, 0);*/ - /*g_outputToString = 1;*/ /* Is reset by printTexLongMath */ + // The below has been replaced by + // getTexOrHtmlHypAndAssertion(i) above. + // printTexLongMath(g_Statement[i].mathString, "", "", 0, 0); + + // g_outputToString = 1; // Is reset by printTexLongMath } else { - /* Theorems are listed w/ description; otherwise file is too - big for convenience */ + // Theorems are listed w/ description; otherwise file is too + // big for convenience. free_vstring(str1); str1 = getDescription(i); if (strlen(str1) > 29) @@ -2884,26 +2867,26 @@ void command(int argc, char *argv[]) { let(&str1, cat(str1, "
\n"); print2("
\n"); - /* print trailer will close out string later */ + // print trailer will close out string later g_outputToString = 0; } } - /*E*/ if (0) { /* for debugging: */ + /*E*/ if (0) { // for debugging: printLongLine(nmbrCvtRToVString(g_WrkProof.proofString, - 0, /*explicitTargets*/ - 0 /*statemNum, used only if explicitTargets*/)," "," "); + 0, // explicitTargets + 0 /* statemNum, used only if explicitTargets */)," "," "); print2("\n"); nmbrLet(&nmbrSaveProof, nmbrSquishProof(g_WrkProof.proofString)); printLongLine(nmbrCvtRToVString(nmbrSaveProof, - 0, /*explicitTargets*/ - 0 /*statemNum, used only if explicitTargets*/)," "," "); + 0, // explicitTargets + 0 /* statemNum, used only if explicitTargets */)," "," "); print2("\n"); nmbrLet(&nmbrTmp, nmbrUnsquishProof(nmbrSaveProof)); printLongLine(nmbrCvtRToVString(nmbrTmp, - 0, /*explicitTargets*/ - 0 /*statemNum, used only if explicitTargets*/)," "," "); + 0, // explicitTargets + 0 /* statemNum, used only if explicitTargets */)," "," "); nmbrLet(&nmbrTmp, nmbrGetTargetHyp(nmbrSaveProof,g_showStatement)); printLongLine(nmbrCvtAnyToVString(nmbrTmp)," "," "); print2("\n"); @@ -3996,13 +3978,13 @@ void command(int argc, char *argv[]) { nmbrLet(&nmbrTmp, nmbrGetEssential(nmbrSaveProof)); printLongLine(nmbrCvtAnyToVString(nmbrTmp)," "," "); print2("\n"); - cleanWrkProof(); /* Deallocate verifyProof storage */ - } /* end debugging */ + cleanWrkProof(); // Deallocate verifyProof storage + } // end debugging - if (pipFlag) break; /* Only one iteration for NEW_PROOF stuff */ - } /* Next stmt */ + if (pipFlag) break; // Only one iteration for NEW_PROOF stuff + } // Next stmt if (!q) { - /* No matching statement was found */ + // No matching statement was found printLongLine(cat("?There is no $p statement whose label matches \"", (cmdMatches("MIDI")) ? g_fullArg[1] : g_fullArg[2], "\". ", @@ -4018,9 +4000,9 @@ void command(int argc, char *argv[]) { } continue; - } /* if (cmdMatches("SHOW/SAVE [NEW_]PROOF" or" MIDI") */ + } // if (cmdMatches("SHOW/SAVE [NEW_]PROOF" or" MIDI") -/*E*/ /*???????? DEBUG command for debugging only */ +/*E*/ // ???????? DEBUG command for debugging only if (cmdMatches("DBG")) { print2("DEBUGGING MODE IS FOR DEVELOPER'S USE ONLY!\n"); print2("Argument: %s\n", g_fullArg[1]); @@ -4028,46 +4010,47 @@ void command(int argc, char *argv[]) { for (j = 0; j < 3; j++) { print2("Trying depth %ld\n", j); nmbrTmpPtr = proveFloating(nmbrTmp, g_proveStatement, j, 0, 0, - 1/*overrideFlag*/, 1/*mathboxFlag*/); + 1, // overrideFlag + 1); // mathboxFlag if (nmbrLen(nmbrTmpPtr)) break; } print2("Result: %s\n", nmbrCvtRToVString(nmbrTmpPtr, - 0, /*explicitTargets*/ - 0 /*statemNum, used only if explicitTargets*/)); + 0, // explicitTargets + 0)); // statemNum, used only if explicitTargets free_nmbrString(nmbrTmpPtr); continue; } -/*E*/ /*???????? DEBUG command for debugging only */ +/*E*/ // ???????? DEBUG command for debugging only if (cmdMatches("PROVE")) { - /* Get the unique statement matching the g_fullArg[1] pattern */ + // Get the unique statement matching the g_fullArg[1] pattern i = getStatementNum(g_fullArg[1], - 1/*startStmt*/, - g_statements + 1 /*maxStmt*/, - 0/*aAllowed*/, - 1/*pAllowed*/, - 0/*eAllowed*/, - 0/*fAllowed*/, - 0/*efOnlyForMaxStmt*/, - 1/*uniqueFlag*/); + 1, // startStmt + g_statements + 1, // maxStmt + 0, // aAllowed + 1, // pAllowed + 0, // eAllowed + 0, // fAllowed + 0, // efOnlyForMaxStmt + 1); // uniqueFlag if (i == -1) { - continue; /* Error msg was provided if not unique */ + continue; // Error msg was provided if not unique } g_proveStatement = i; - /* 1 means to override usage locks */ + // 1 means to override usage locks overrideFlag = ( (switchPos("OVERRIDE")) ? 1 : 0) || g_globalDiscouragement == 0; if (getMarkupFlag(g_proveStatement, PROOF_DISCOURAGED)) { if (overrideFlag == 0) { - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis print2(">>> ?Error: " "Modification of this statement's proof is discouraged.\n"); print2(">>> You must use PROVE ... / OVERRIDE to work on it.\n"); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis continue; } } @@ -4075,13 +4058,13 @@ void command(int argc, char *argv[]) { print2("Entering the Proof Assistant. " "HELP PROOF_ASSISTANT for help, EXIT to exit.\n"); - g_PFASmode = 1; /* Set mode for commands here and in mmcmdl.c */ - /* Note: Proof Assistant mode can equivalently be determined by: - nmbrLen(g_ProofInProgress.proof) != 0 */ + g_PFASmode = 1; // Set mode for commands here and in mmcmdl.c + // Note: Proof Assistant mode can equivalently be determined by: + // nmbrLen(g_ProofInProgress.proof) != 0 parseProof(g_proveStatement); - verifyProof(g_proveStatement); /* Necessary to set RPN stack ptrs - before calling cleanWrkProof() */ + // Necessary to set RPN stack ptrs before calling cleanWrkProof(). + verifyProof(g_proveStatement); if (g_WrkProof.errorSeverity > 1) { print2( "The starting proof has a severe error. It will not be used.\n"); @@ -4089,19 +4072,19 @@ void command(int argc, char *argv[]) { } else { nmbrLet(&nmbrSaveProof, g_WrkProof.proofString); } - cleanWrkProof(); /* Deallocate verifyProof storage */ + cleanWrkProof(); // Deallocate verifyProof storage - /* Initialize the structure needed for the Proof Assistant */ + // Initialize the structure needed for the Proof Assistant initProofStruct(&g_ProofInProgress, nmbrSaveProof, g_proveStatement); - /* Show the user the statement to be proved */ + // Show the user the statement to be proved print2("You will be working on statement (from \"SHOW STATEMENT %s\"):\n", g_Statement[g_proveStatement].labelName); - typeStatement(g_proveStatement /*g_showStatement*/, - 1 /*briefFlag*/, - 0 /*commentOnlyFlag*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); + typeStatement(g_proveStatement, // g_showStatement + 1, // briefFlag + 0, // commentOnlyFlag + 0, // texFlag + 0); // g_htmlFlag if (!nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { print2( @@ -4110,112 +4093,111 @@ void command(int argc, char *argv[]) { print2( "Unknown step summary (from \"SHOW NEW_PROOF / UNKNOWN\"):\n"); - /* Automatically display new unknown steps - ???Future - add switch to enable/defeat this */ + // Automatically display new unknown steps + // ???Future - add switch to enable/defeat this typeProof(g_proveStatement, - 1 /*pipFlag*/, - 0 /*startStep*/, - 0 /*endStep*/, - 0 /*endIndent*/, - 1 /*essentialFlag*/, - 0 /*renumberFlag*/, - 1 /*unknownFlag*/, - 0 /*notUnifiedFlag*/, - 0 /*reverseFlag*/, - 0 /*noIndentFlag*/, - 0 /*splitColumn*/, - 0 /*skipRepeatedSteps*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); + 1, // pipFlag + 0, // startStep + 0, // endStep + 0, // endIndent + 1, // essentialFlag + 0, // renumberFlag + 1, // unknownFlag + 0, // notUnifiedFlag + 0, // reverseFlag + 0, // noIndentFlag + 0, // splitColumn + 0, // skipRepeatedSteps + 0, // texFlag + 0); // g_htmlFlag } if (getMarkupFlag(g_proveStatement, PROOF_DISCOURAGED)) { - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis print2( ">>> ?Warning: Modification of this statement's proof is discouraged.\n" ); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis } - processUndoStack(NULL, PUS_INIT, "", 0); /* Optional? */ - /* Put the initial proof into the UNDO stack; we don't need - the info string since it won't be undone */ + processUndoStack(NULL, PUS_INIT, "", 0); // Optional? + // Put the initial proof into the UNDO stack; we don't need + // the info string since it won't be undone. processUndoStack(&g_ProofInProgress, PUS_PUSH, "", 0); continue; } if (cmdMatches("UNDO")) { processUndoStack(&g_ProofInProgress, PUS_UNDO, "", 0); - g_proofChanged = 1; /* Maybe make this more intelligent some day */ - /* Automatically display new unknown steps - ???Future - add switch to enable/defeat this */ + g_proofChanged = 1; // Maybe make this more intelligent some day + // Automatically display new unknown steps + // ???Future - add switch to enable/defeat this typeProof(g_proveStatement, - 1 /*pipFlag*/, - 0 /*startStep*/, - 0 /*endStep*/, - 0 /*endIndent*/, - 1 /*essentialFlag*/, - 0 /*renumberFlag*/, - 1 /*unknownFlag*/, - 0 /*notUnifiedFlag*/, - 0 /*reverseFlag*/, - 0 /*noIndentFlag*/, - 0 /*splitColumn*/, - 0 /*skipRepeatedSteps*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); + 1, // pipFlag + 0, // startStep + 0, // endStep + 0, // endIndent + 1, // essentialFlag + 0, // renumberFlag + 1, // unknownFlag + 0, // notUnifiedFlag + 0, // reverseFlag + 0, // noIndentFlag + 0, // splitColumn + 0, // skipRepeatedSteps + 0, // texFlag + 0); // g_htmlFlag continue; } if (cmdMatches("REDO")) { processUndoStack(&g_ProofInProgress, PUS_REDO, "", 0); - g_proofChanged = 1; /* Maybe make this more intelligent some day */ - /* Automatically display new unknown steps - ???Future - add switch to enable/defeat this */ + g_proofChanged = 1; // Maybe make this more intelligent some day + // Automatically display new unknown steps + // ???Future - add switch to enable/defeat this typeProof(g_proveStatement, - 1 /*pipFlag*/, - 0 /*startStep*/, - 0 /*endStep*/, - 0 /*endIndent*/, - 1 /*essentialFlag*/, - 0 /*renumberFlag*/, - 1 /*unknownFlag*/, - 0 /*notUnifiedFlag*/, - 0 /*reverseFlag*/, - 0 /*noIndentFlag*/, - 0 /*splitColumn*/, - 0 /*skipRepeatedSteps*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); + 1, // pipFlag + 0, // startStep + 0, // endStep + 0, // endIndent + 1, // essentialFlag + 0, // renumberFlag + 1, // unknownFlag + 0, // notUnifiedFlag + 0, // reverseFlag + 0, // noIndentFlag + 0, // splitColumn + 0, // skipRepeatedSteps + 0, // texFlag + 0); // g_htmlFlag continue; } if (cmdMatches("UNIFY")) { - m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ + m = nmbrLen(g_ProofInProgress.proof); // Original proof length g_proofChangedFlag = 0; if (cmdMatches("UNIFY STEP")) { - s = (long)val(g_fullArg[2]); /* Step number */ + s = (long)val(g_fullArg[2]); // Step number if (s > m || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", m); continue; } + // 2nd arg. means print msg if already unified + interactiveUnifyStep(s - 1, 1); - interactiveUnifyStep(s - 1, 1); /* 2nd arg. means print msg if - already unified */ - - /* (The interactiveUnifyStep handles all messages.) */ - /* print2("... */ + // (The interactiveUnifyStep handles all messages.) + // print2("... autoUnify(1); if (g_proofChangedFlag) { - g_proofChanged = 1; /* Cumulative flag */ + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } continue; } - /* "UNIFY ALL" */ + // "UNIFY ALL" if (!switchPos("INTERACTIVE")) { autoUnify(1); if (!g_proofChangedFlag) { @@ -4223,70 +4205,71 @@ void command(int argc, char *argv[]) { } else { print2( "Steps were unified. SHOW NEW_PROOF / NOT_UNIFIED to see any remaining.\n"); - g_proofChanged = 1; /* Cumulative flag */ + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } } else { q = 0; while (1) { - /* Repeat the unifications over and over until done, since - a later unification may improve the ability of an aborted earlier - one to be done without timeout */ - g_proofChangedFlag = 0; /* This flag is set by autoUnify() and - interactiveUnifyStep() */ + // Repeat the unifications over and over until done, since + // a later unification may improve the ability of an aborted earlier + // one to be done without timeout. + + // This flag is set by autoUnify() and interactiveUnifyStep() + g_proofChangedFlag = 0; autoUnify(0); for (s = m - 1; s >= 0; s--) { - interactiveUnifyStep(s, 0); /* 2nd arg. means no msg if already - unified */ + // 2nd arg. means no msg if already unified. + interactiveUnifyStep(s, 0); } - autoUnify(1); /* 1 means print congratulations if complete */ + autoUnify(1); // 1 means print congratulations if complete if (!g_proofChangedFlag) { if (!q) { print2("No new unifications were made.\n"); } else { - /* If q=1, then we are in the 2nd or later pass, which means - there was a change in the 1st pass. */ + // If q=1, then we are in the 2nd or later pass, which means + // there was a change in the 1st pass. print2( "Steps were unified. SHOW NEW_PROOF / NOT_UNIFIED to see any remaining.\n"); - g_proofChanged = 1; /* Cumulative flag */ + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } - break; /* while (1) */ + break; // while (1) } else { - q = 1; /* Flag that we're starting a 2nd or later pass */ + q = 1; // Flag that we're starting a 2nd or later pass } - } /* End while (1) */ + } // End while (1) } - /* Automatically display new unknown steps - ???Future - add switch to enable/defeat this */ + // Automatically display new unknown steps + // ???Future - add switch to enable/defeat this typeProof(g_proveStatement, - 1 /*pipFlag*/, - 0 /*startStep*/, - 0 /*endStep*/, - 0 /*endIndent*/, - 1 /*essentialFlag*/, - 0 /*renumberFlag*/, - 1 /*unknownFlag*/, - 0 /*notUnifiedFlag*/, - 0 /*reverseFlag*/, - 0 /*noIndentFlag*/, - 0 /*splitColumn*/, - 0 /*skipRepeatedSteps*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); + 1, // pipFlag + 0, // startStep + 0, // endStep + 0, // endIndent + 1, // essentialFlag + 0, // renumberFlag + 1, // unknownFlag + 0, // notUnifiedFlag + 0, // reverseFlag + 0, // noIndentFlag + 0, // splitColumn + 0, // skipRepeatedSteps + 0, // texFlag + 0); // g_htmlFlag continue; } if (cmdMatches("MATCH")) { - maxEssential = -1; /* Default: no maximum */ + maxEssential = -1; // Default: no maximum i = switchPos("MAX_ESSENTIAL_HYP"); if (i) maxEssential = (long)val(g_fullArg[i + 1]); if (cmdMatches("MATCH STEP")) { - s = (long)val(g_fullArg[2]); /* Step number */ - m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ + s = (long)val(g_fullArg[2]); // Step number + m = nmbrLen(g_ProofInProgress.proof); // Original proof length if (s > m || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", m); continue; @@ -4298,7 +4281,7 @@ void command(int argc, char *argv[]) { } interactiveMatch(s - 1, maxEssential); - n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ + n = nmbrLen(g_ProofInProgress.proof); // New proof length if (n != m) { if (s != m) { printLongLine(cat("Steps ", str((double)s), ":", @@ -4314,17 +4297,17 @@ void command(int argc, char *argv[]) { } autoUnify(1); - g_proofChanged = 1; /* Cumulative flag */ - /* 1-Nov-2013 nm Why is g_proofChanged set unconditionally above? - Do we need the processUndoStack() call? */ + g_proofChanged = 1; // Cumulative flag + // 1-Nov-2013 nm Why is g_proofChanged set unconditionally above? + // Do we need the processUndoStack() call? processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; - } /* End if MATCH STEP */ + } // End if MATCH STEP if (cmdMatches("MATCH ALL")) { - m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ + m = nmbrLen(g_ProofInProgress.proof); // Original proof length k = 0; g_proofChangedFlag = 0; @@ -4334,30 +4317,30 @@ void command(int argc, char *argv[]) { } for (s = m; s > 0; s--) { - /* Match only unknown steps */ + // Match only unknown steps if ((g_ProofInProgress.proof)[s - 1] != -(long)'?') continue; - /* Match only essential steps if specified */ + // Match only essential steps if specified if (switchPos("ESSENTIAL")) { if (!nmbrTmp[s - 1]) continue; } interactiveMatch(s - 1, maxEssential); if (g_proofChangedFlag) { - k = s; /* Save earliest step changed */ + k = s; // Save earliest step changed g_proofChangedFlag = 0; } print2("\n"); } if (k) { - g_proofChangedFlag = 1; /* Restore it */ - g_proofChanged = 1; /* Cumulative flag */ + g_proofChangedFlag = 1; // Restore it + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); print2("Steps %ld and above have been renumbered.\n", k); } autoUnify(1); continue; - } /* End if MATCH ALL */ + } // End if MATCH ALL } if (cmdMatches("LET")) { @@ -4365,7 +4348,7 @@ void command(int argc, char *argv[]) { g_errorCount = 0; nmbrLet(&nmbrTmp, parseMathTokens(g_fullArg[4], g_proveStatement)); if (g_errorCount) { - /* Parsing issued error message(s) */ + // Parsing issued error message(s) g_errorCount = 0; continue; } @@ -4387,95 +4370,95 @@ void command(int argc, char *argv[]) { autoUnify(1); - g_proofChangedFlag = 1; /* Flag to push 'undo' stack */ - g_proofChanged = 1; /* Cumulative flag */ + g_proofChangedFlag = 1; // Flag to push 'undo' stack + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } if (cmdMatches("LET STEP")) { s = getStepNum(g_fullArg[2], g_ProofInProgress.proof, - 0 /* ALL not allowed */); - if (s == -1) continue; /* Error; message was provided already */ + 0); // ALL not allowed + if (s == -1) continue; // Error; message was provided already - /* Check to see if the statement selected is allowed */ + // Check to see if the statement selected is allowed if (!checkMStringMatch(nmbrTmp, s - 1)) { printLongLine(cat("?Step ", str((double)s), " cannot be unified with \"", nmbrCvtMToVString(nmbrTmp),"\".", NULL), " ", " "); continue; } - /* Assign the user string */ + // Assign the user string nmbrLet((nmbrString **)(&((g_ProofInProgress.user)[s - 1])), nmbrTmp); autoUnify(1); - g_proofChangedFlag = 1; /* Flag to push 'undo' stack */ - g_proofChanged = 1; /* Cumulative flag */ + g_proofChangedFlag = 1; // Flag to push 'undo' stack + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } - /* Automatically display new unknown steps - ???Future - add switch to enable/defeat this */ + // Automatically display new unknown steps + // ???Future - add switch to enable/defeat this typeProof(g_proveStatement, - 1 /*pipFlag*/, - 0 /*startStep*/, - 0 /*endStep*/, - 0 /*endIndent*/, - 1 /*essentialFlag*/, - 0 /*renumberFlag*/, - 1 /*unknownFlag*/, - 0 /*notUnifiedFlag*/, - 0 /*reverseFlag*/, - 0 /*noIndentFlag*/, - 0 /*splitColumn*/, - 0 /*skipRepeatedSteps*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); + 1, // pipFlag + 0, // startStep + 0, // endStep + 0, // endIndent + 1, // essentialFlag + 0, // renumberFlag + 1, // unknownFlag + 0, // notUnifiedFlag + 0, // reverseFlag + 0, // noIndentFlag + 0, // splitColumn + 0, // skipRepeatedSteps + 0, // texFlag + 0); // g_htmlFlag continue; } if (cmdMatches("ASSIGN")) { s = getStepNum(g_fullArg[1], g_ProofInProgress.proof, - 0 /* ALL not allowed */); - if (s == -1) continue; /* Error; message was provided already */ + 0); // ALL not allowed + if (s == -1) continue; // Error; message was provided already - /* 1 means to override usage locks */ + // 1 means to override usage locks overrideFlag = ( (switchPos("OVERRIDE")) ? 1 : 0) || g_globalDiscouragement == 0; - /* Get the unique statement matching the g_fullArg[2] pattern */ + // Get the unique statement matching the g_fullArg[2] pattern k = getStatementNum(g_fullArg[2], - 1/*startStmt*/, - g_proveStatement /*maxStmt*/, - 1/*aAllowed*/, - 1/*pAllowed*/, - 1/*eAllowed*/, - 1/*fAllowed*/, - 1/*efOnlyForMaxStmt*/, - 1/*uniqueFlag*/); + 1, // startStmt + g_proveStatement, // maxStmt + 1, // aAllowed + 1, // pAllowed + 1, // eAllowed + 1, // fAllowed + 1, // efOnlyForMaxStmt + 1); // uniqueFlag if (k == -1) { - continue; /* Error msg was provided if not unique */ + continue; // Error msg was provided if not unique } if (getMarkupFlag(k, USAGE_DISCOURAGED)) { if (overrideFlag == 0) { - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis print2( ">>> ?Error: Attempt to assign a statement whose usage is discouraged.\n"); print2( ">>> Use ASSIGN ... / OVERRIDE if you really want to do this.\n"); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis continue; } else { - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis print2( ">>> ?Warning: You are assigning a statement whose usage is discouraged.\n"); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis } } - m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ + m = nmbrLen(g_ProofInProgress.proof); // Original proof length - /* Check to see that the step is an unknown step */ + // Check to see that the step is an unknown step if ((g_ProofInProgress.proof)[s - 1] != -(long)'?') { print2( "?Step %ld is already assigned. You can only assign unknown steps.\n" @@ -4483,29 +4466,28 @@ void command(int argc, char *argv[]) { continue; } - /* Check to see if the statement selected is allowed */ + // Check to see if the statement selected is allowed if (!checkStmtMatch(k, s - 1)) { print2("?Statement \"%s\" cannot be unified with step %ld.\n", g_Statement[k].labelName, s); continue; } - assignStatement(k /*statement#*/, s - 1 /*step*/); + assignStatement(k /* statement# */, s - 1 /* step */); - n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ + n = nmbrLen(g_ProofInProgress.proof); // New proof length autoUnify(1); - /* Automatically interact with user if step not unified */ - /* ???We might want to add a setting to defeat this if user doesn't - like it */ - /* Since ASSIGN LAST is often run from a command file, don't - interact if / NO_UNIFY is specified, so response is predictable */ + // Automatically interact with user if step not unified. + // ???We might want to add a setting to defeat this if user doesn't like it. + // Since ASSIGN LAST is often run from a command file, don't + // interact if / NO_UNIFY is specified, so response is predictable. if (switchPos("NO_UNIFY") == 0) { - interactiveUnifyStep(s - m + n - 1, 2); /* 2nd arg. means print msg if - already unified */ - } /* if NO_UNIFY flag not set */ + // 2nd arg. means print msg if already unified. + interactiveUnifyStep(s - m + n - 1, 2); + } // if NO_UNIFY flag not set - /* See if it's in another mathbox; if so, let user know */ + // See if it's in another mathbox; if so, let user know assignMathboxInfo(); if (k > g_mathboxStmt && g_proveStatement > g_mathboxStmt) { if (k < g_mathboxStart[getMathboxNum(g_proveStatement) - 1]) { @@ -4517,103 +4499,103 @@ void command(int argc, char *argv[]) { } } - /* Automatically display new unknown steps - ???Future - add switch to enable/defeat this */ + // Automatically display new unknown steps + // ???Future - add switch to enable/defeat this. typeProof(g_proveStatement, - 1 /*pipFlag*/, - 0 /*startStep*/, - 0 /*endStep*/, - 0 /*endIndent*/, - 1 /*essentialFlag*/, - 0 /*renumberFlag*/, - 1 /*unknownFlag*/, - 0 /*notUnifiedFlag*/, - 0 /*reverseFlag*/, - 0 /*noIndentFlag*/, - 0 /*splitColumn*/, - 0 /*skipRepeatedSteps*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); - - g_proofChangedFlag = 1; /* Flag to push 'undo' stack (future) */ - g_proofChanged = 1; /* Cumulative flag */ + 1, // pipFlag + 0, // startStep + 0, // endStep + 0, // endIndent + 1, // essentialFlag + 0, // renumberFlag + 1, // unknownFlag + 0, // notUnifiedFlag + 0, // reverseFlag + 0, // noIndentFlag + 0, // splitColumn + 0, // skipRepeatedSteps + 0, // texFlag + 0); // g_htmlFlag + + g_proofChangedFlag = 1; // Flag to push 'undo' stack (future) + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; - } /* cmdMatches("ASSIGN") */ + } // cmdMatches("ASSIGN") if (cmdMatches("REPLACE")) { - /* 1 means to override usage locks */ + // 1 means to override usage locks overrideFlag = ( (switchPos("OVERRIDE")) ? 1 : 0) || g_globalDiscouragement == 0; step = getStepNum(g_fullArg[1], g_ProofInProgress.proof, - 0 /* ALL not allowed */); - if (step == -1) continue; /* Error; message was provided already */ + 0); // ALL not allowed + if (step == -1) continue; // Error; message was provided already - /* Get the unique statement matching the g_fullArg[2] pattern */ + // Get the unique statement matching the g_fullArg[2] pattern stmt = getStatementNum(g_fullArg[2], - 1/*startStmt*/, - g_proveStatement /*maxStmt*/, - 1/*aAllowed*/, - 1/*pAllowed*/, - 0/*eAllowed*/, /* Not implemented (yet?) */ - 0/*fAllowed*/, /* Not implemented (yet?) */ - 1/*efOnlyForMaxStmt*/, - 1/*uniqueFlag*/); + 1, // startStmt + g_proveStatement, // maxStmt + 1, // aAllowed + 1, // pAllowed + 0, // eAllowed // Not implemented (yet?) + 0, // fAllowed // Not implemented (yet?) + 1, // efOnlyForMaxStmt + 1); // uniqueFlag if (stmt == -1) { - continue; /* Error msg was provided if not unique */ + continue; // Error msg was provided if not unique } if (getMarkupFlag(stmt, USAGE_DISCOURAGED)) { if (overrideFlag == 0) { - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis print2( ">>> ?Error: Attempt to assign a statement whose usage is discouraged.\n"); print2( ">>> Use REPLACE ... / OVERRIDE if you really want to do this.\n"); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis continue; } else { - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis print2( ">>> ?Warning: You are assigning a statement whose usage is discouraged.\n"); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis } } - m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ + m = nmbrLen(g_ProofInProgress.proof); // Original proof length - /* Set a flag that proof has unknown steps (for autoUnify() call below) */ + // Set a flag that proof has unknown steps (for autoUnify() call below) if (nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { p = 1; } else { p = 0; } - /* Check to see if the statement selected is allowed */ + // Check to see if the statement selected is allowed if (!checkStmtMatch(stmt, step - 1)) { print2("?Statement \"%s\" cannot be unified with step %ld.\n", g_Statement[stmt].labelName, step); continue; } - /* Check dummy variable status of step */ - /* For use in message later */ + // Check dummy variable status of step. + // For use in message later. + // 0 = no dummy vars, 1 = isolated dummy vars, 2 = not isolated. dummyVarIsoFlag = checkDummyVarIsolation(step - 1); - /* 0=no dummy vars, 1=isolated dummy vars, 2=not isolated*/ - /* Do the replacement */ - nmbrTmpPtr = replaceStatement(stmt /*statement#*/, - step - 1 /*step*/, + // Do the replacement + nmbrTmpPtr = replaceStatement(stmt, // statement# + step - 1, // step g_proveStatement, - 0,/*scan whole proof to maximize chance of a match*/ - 0/*noDistinct*/, - 1/* try to prove $e's */, - 1/*improveDepth*/, + 0, // scan whole proof to maximize chance of a match + 0, // noDistinct + 1, // try to prove $e's + 1, // improveDepth overrideFlag, - /* Currently REPLACE (not often used) allows other mathboxes - silently; TODO: we may want to notify user like for ASSIGN */ - 1/*mathboxFlag*/); + // Currently REPLACE (not often used) allows other mathboxes + // silently; TODO: we may want to notify user like for ASSIGN. + 1); // mathboxFlag if (!nmbrLen(nmbrTmpPtr)) { print2( "?Hypotheses of statement \"%s\" do not match known proof steps.\n", @@ -4621,30 +4603,29 @@ void command(int argc, char *argv[]) { continue; } - /* Get the subproof at step s */ + // Get the subproof at step s q = subproofLen(g_ProofInProgress.proof, step - 1); deleteSubProof(step - 1); addSubProof(nmbrTmpPtr, step - q); - /* Assign known subproofs */ + // Assign known subproofs assignKnownSubProofs(); - /* Initialize remaining steps */ + // Initialize remaining steps i = nmbrLen(g_ProofInProgress.proof); for (j = 0; j < i; j++) { if (!nmbrLen((g_ProofInProgress.source)[j])) { initStep(j); } } - /* Unify whatever can be unified */ - /* If proof wasn't complete before (p = 1), but is now, print congrats - for user */ - autoUnify((char)p); /* 0 means no "congrats" message */ + // Unify whatever can be unified. + // If proof wasn't complete before (p = 1), but is now, print congrats for user + autoUnify((char)p); // 0 means no "congrats" message - free_nmbrString(nmbrTmpPtr); /* Deallocate memory */ + free_nmbrString(nmbrTmpPtr); // Deallocate memory - n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ + n = nmbrLen(g_ProofInProgress.proof); // New proof length if (nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { - /* The proof is not complete, so print step numbers that changed */ + // The proof is not complete, so print step numbers that changed if (m == n) { print2("Step %ld was replaced with statement %s.\n", step, g_Statement[stmt].labelName); @@ -4667,8 +4648,8 @@ void command(int argc, char *argv[]) { } } - g_proofChangedFlag = 1; /* Flag to push 'undo' stack */ - g_proofChanged = 1; /* Cumulative flag */ + g_proofChangedFlag = 1; // Flag to push 'undo' stack + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); if (dummyVarIsoFlag == 2 && g_proofChangedFlag) { @@ -4680,36 +4661,36 @@ void command(int argc, char *argv[]) { "", " "); } - /* Automatically display new unknown steps - ???Future - add switch to enable/defeat this */ + // Automatically display new unknown steps + // ???Future - add switch to enable/defeat this. if (g_proofChangedFlag) typeProof(g_proveStatement, - 1 /*pipFlag*/, - 0 /*startStep*/, - 0 /*endStep*/, - 0 /*endIndent*/, - 1 /*essentialFlag*/, - 0 /*renumberFlag*/, - 1 /*unknownFlag*/, - 0 /*notUnifiedFlag*/, - 0 /*reverseFlag*/, - 0 /*noIndentFlag*/, - 0 /*splitColumn*/, - 0 /*skipRepeatedSteps*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); + 1, // pipFlag + 0, // startStep + 0, // endStep + 0, // endIndent + 1, // essentialFlag + 0, // renumberFlag + 1, // unknownFlag + 0, // notUnifiedFlag + 0, // reverseFlag + 0, // noIndentFlag + 0, // splitColumn + 0, // skipRepeatedSteps + 0, // texFlag + 0); // g_htmlFlag continue; - } /* REPLACE */ + } // REPLACE if (cmdMatches("IMPROVE")) { - improveDepth = 0; /* Depth */ + improveDepth = 0; // Depth i = switchPos("DEPTH"); if (i) improveDepth = (long)val(g_fullArg[i + 1]); + // p = 1 means don't try to use statements with $d's if (switchPos("NO_DISTINCT")) p = 1; else p = 0; - /* p = 1 means don't try to use statements with $d's */ - searchAlg = 1; /* Default */ + searchAlg = 1; // Default if (switchPos("1")) searchAlg = 1; if (switchPos("2")) searchAlg = 2; if (switchPos("3")) searchAlg = 3; @@ -4717,9 +4698,9 @@ void command(int argc, char *argv[]) { if (switchPos("SUBPROOFS")) searchUnkSubproofs = 1; mathboxFlag = (switchPos("INCLUDE_MATHBOXES") != 0); - assignMathboxInfo(); /* In case it hasn't been assigned yet */ + assignMathboxInfo(); // In case it hasn't been assigned yet if (g_proveStatement > g_mathboxStmt) { - /* We're in a mathbox */ + // We're in a mathbox i = getMathboxNum(g_proveStatement); if (i <= 0) bug(1130); thisMathboxStartStmt = g_mathboxStart[i - 1]; @@ -4727,23 +4708,23 @@ void command(int argc, char *argv[]) { thisMathboxStartStmt = g_mathboxStmt; } - /* 1 means to override usage locks */ + // 1 means to override usage locks overrideFlag = ( (switchPos("OVERRIDE")) ? 1 : 0) || g_globalDiscouragement == 0; s = getStepNum(g_fullArg[1], g_ProofInProgress.proof, - 1 /* 1 = "ALL" is permissible; returns 0 */); - if (s == -1) continue; /* Error; message was provided already */ + 1); // 1 = "ALL" is permissible; returns 0 + if (s == -1) continue; // Error; message was provided already - if (s != 0) { /* s=0 means ALL */ - m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ + if (s != 0) { // s=0 means ALL + m = nmbrLen(g_ProofInProgress.proof); // Original proof length - /* Get the subproof at step s */ + // Get the subproof at step s q = subproofLen(g_ProofInProgress.proof, s - 1); nmbrLet(&nmbrTmp, nmbrSeg(g_ProofInProgress.proof, s - q + 1, s)); - /*???Shouldn't this be just known?*/ - /* Check to see that the subproof has an unknown step. */ + // ???Shouldn't this be just known? + // Check to see that the subproof has an unknown step. if (!nmbrElementIn(1, nmbrTmp, -(long)'?')) { print2( "?Step %ld already has a proof and cannot be improved.\n", @@ -4751,55 +4732,53 @@ void command(int argc, char *argv[]) { continue; } - /* Check dummy variable status of step */ + // Check dummy variable status of step + // 0 = no dummy vars, 1 = isolated dummy vars, 2 = not isolated dummyVarIsoFlag = checkDummyVarIsolation(s - 1); - /* 0=no dummy vars, 1=isolated dummy vars, 2=not isolated*/ if (dummyVarIsoFlag == 2) { print2( "?Step %ld target has shared dummy variables and cannot be improved.\n", s); - continue; /* Don't try to improve - dummy variables that aren't isolated */ + continue; // Don't try to improve dummy variables that aren't isolated. } - if (dummyVarIsoFlag == 0) { /* No dummy vars */ - /* Only use proveFloating if no dummy vars */ + if (dummyVarIsoFlag == 0) { // No dummy vars + // Only use proveFloating if no dummy vars nmbrTmpPtr = proveFloating((g_ProofInProgress.target)[s - 1], - g_proveStatement, improveDepth, s - 1, (char)p/*NO_DISTINCT*/, + g_proveStatement, improveDepth, s - 1, (char)p /* NO_DISTINCT */, overrideFlag, mathboxFlag); } else { - nmbrTmpPtr = NULL_NMBRSTRING; /* Initialize */ + nmbrTmpPtr = NULL_NMBRSTRING; // Initialize } if (!nmbrLen(nmbrTmpPtr)) { - /* A proof for the step was not found with proveFloating(). */ + // A proof for the step was not found with proveFloating(). - /* Next, try REPLACE algorithm */ + // Next, try REPLACE algorithm if (searchAlg == 2 || searchAlg == 3) { nmbrTmpPtr = proveByReplacement(g_proveStatement, - s - 1/*prfStep*/, /* 0 means step 1 */ - (char)p/*NO_DISTINCT*/, /* 1 means don't try stmts with $d's */ + s - 1, // prfStep // 0 means step 1 + (char)p, // NO_DISTINCT // 1 means don't try stmts with $d's dummyVarIsoFlag, - (char)(searchAlg - 2), /*0=proveFloat for $fs, 1=$e's also */ + (char)(searchAlg - 2), // 0 = proveFloat for $fs, 1 = $e's also improveDepth, overrideFlag, mathboxFlag); } if (!nmbrLen(nmbrTmpPtr)) { print2("A proof for step %ld was not found.\n", s); - /* REPLACE algorithm also failed */ + // REPLACE algorithm also failed continue; } } - /* If q=1, subproof must be an unknown step, so don't bother to - delete it */ - /*???Won't q always be 1 here?*/ + // If q=1, subproof must be an unknown step, so don't bother to delete it + // ???Won't q always be 1 here? if (q > 1) deleteSubProof(s - 1); addSubProof(nmbrTmpPtr, s - q); assignKnownSteps(s - q, nmbrLen(nmbrTmpPtr)); free_nmbrString(nmbrTmpPtr); - n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ + n = nmbrLen(g_ProofInProgress.proof); // New proof length if (m == n) { print2("A 1-step proof was found for step %ld.\n", s); } else { @@ -4820,20 +4799,20 @@ void command(int argc, char *argv[]) { } } - autoUnify(1); /* To get 'congrats' message if proof complete */ - g_proofChanged = 1; /* Cumulative flag */ + autoUnify(1); // To get 'congrats' message if proof complete + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); - /* End if s != 0 i.e. not IMPROVE ALL */ + // End if s != 0 i.e. not IMPROVE ALL } else { - /* Here, getStepNum() returned 0, meaning ALL */ + // Here, getStepNum() returned 0, meaning ALL if (!nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { print2("The proof is already complete.\n"); continue; } - n = 0; /* Earliest step that changed */ + n = 0; // Earliest step that changed g_proofChangedFlag = 0; @@ -4858,100 +4837,98 @@ void command(int argc, char *argv[]) { print2("Pass 3: Repeating pass 1...\n"); } } - /* improveAllIter = 1: run proveFloating only */ - /* improveAllIter = 2: run proveByReplacement on unknown steps */ - /* improveAllIter = 3: run proveByReplacement on steps with - incomplete subproofs */ - /* improveAllIter = 4: if something changed, run everything again */ + // improveAllIter = 1: run proveFloating only. + // improveAllIter = 2: run proveByReplacement on unknown steps. + // improveAllIter = 3: run proveByReplacement on steps with incomplete subproofs. + // improveAllIter = 4: if something changed, run everything again. if (improveAllIter == 3 && !searchUnkSubproofs) continue; - m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ + m = nmbrLen(g_ProofInProgress.proof); // Original proof length for (s = m; s > 0; s--) { proofStepUnk = ((g_ProofInProgress.proof)[s - 1] == -(long)'?') ? 1 : 0; - /* I think this is really too conservative, even - with the old algorithm, but keep it to imitate the old one */ + // I think this is really too conservative, even + // with the old algorithm, but keep it to imitate the old one. if (improveAllIter == 1 || searchAlg == 1) { - /* If the step is known and unified, don't do it, since nothing - would be accomplished. */ + // If the step is known and unified, don't do it, since nothing + // would be accomplished. if (!proofStepUnk) { if (nmbrEq((g_ProofInProgress.target)[s - 1], (g_ProofInProgress.source)[s - 1])) continue; } } - /* Get the subproof at step s */ + // Get the subproof at step s q = subproofLen(g_ProofInProgress.proof, s - 1); - if (proofStepUnk && q != 1) bug(1120); /* Consistency check */ + if (proofStepUnk && q != 1) bug(1120); // Consistency check nmbrLet(&nmbrTmp, nmbrSeg(g_ProofInProgress.proof, s - q + 1, s)); - /* Improve only subproofs with unknown steps */ + // Improve only subproofs with unknown steps if (!nmbrElementIn(1, nmbrTmp, -(long)'?')) continue; - free_nmbrString(nmbrTmp); /* No longer needed - dealloc */ + free_nmbrString(nmbrTmp); // No longer needed - dealloc - /* Check dummy variable status of step */ + // Check dummy variable status of step + // 0 = no dummy vars, 1 = isolated dummy vars, 2 = not isolated dummyVarIsoFlag = checkDummyVarIsolation(s - 1); - /* 0=no dummy vars, 1=isolated dummy vars, 2=not isolated*/ - if (dummyVarIsoFlag == 2) continue; /* Don't try to improve - dummy variables that aren't isolated */ + // Don't try to improve dummy variables that aren't isolated. + if (dummyVarIsoFlag == 2) continue; if (dummyVarIsoFlag == 0 && (improveAllIter == 1 || improveAllIter == 4)) { - /* No dummy vars */ - /* Only use proveFloating if no dummy vars */ + // No dummy vars + // Only use proveFloating if no dummy vars nmbrTmpPtr = proveFloating((g_ProofInProgress.target)[s - 1], g_proveStatement, improveDepth, s - 1, - (char)p/*NO_DISTINCT*/, + (char)p, // NO_DISTINCT overrideFlag, mathboxFlag); } else { - nmbrTmpPtr = NULL_NMBRSTRING; /* Init */ + nmbrTmpPtr = NULL_NMBRSTRING; // Init } if (!nmbrLen(nmbrTmpPtr)) { - /* A proof for the step was not found with proveFloating(). */ + // A proof for the step was not found with proveFloating(). - /* Next, try REPLACE algorithm */ + // Next, try REPLACE algorithm. if ((searchAlg == 2 || searchAlg == 3) && ((improveAllIter == 2 && proofStepUnk) || (improveAllIter == 3 && !proofStepUnk) - /*|| improveAllIter == 4*/)) { + /* || improveAllIter == 4 */)) { nmbrTmpPtr = proveByReplacement(g_proveStatement, - s - 1/*prfStep*/, /* 0 means step 1 */ - (char)p/*NO_DISTINCT*/, /* 1 means don't try stmts w/ $d's */ + s - 1, // prfStep // 0 means step 1 + (char)p, // NO_DISTINCT // 1 means don't try stmts w/ $d's dummyVarIsoFlag, - (char)(searchAlg - 2),/*searchMethod: 0 or 1*/ + (char)(searchAlg - 2), // searchMethod: 0 or 1 improveDepth, overrideFlag, mathboxFlag); } if (!nmbrLen(nmbrTmpPtr)) { - /* REPLACE algorithm also failed */ + // REPLACE algorithm also failed continue; } } - /* If q=1, subproof must be an unknown step, so don't bother to - delete it */ + // If q=1, subproof must be an unknown step, so don't bother to delete it if (q > 1) deleteSubProof(s - 1); addSubProof(nmbrTmpPtr, s - q); assignKnownSteps(s - q, nmbrLen(nmbrTmpPtr)); print2("A proof of length %ld was found for step %ld.\n", nmbrLen(nmbrTmpPtr), s); - if (nmbrLen(nmbrTmpPtr) || q != 1) n = s - q + 1; - /* Save earliest step changed */ + // Save earliest step changed + if (nmbrLen(nmbrTmpPtr) || q != 1) n = s - q + 1; free_nmbrString(nmbrTmpPtr); g_proofChangedFlag = 1; - s = s - q + 1; /* Adjust step position to account for deleted subpr */ - } /* Next step s */ + s = s - q + 1; // Adjust step position to account for deleted subpr + } // Next step s if (g_proofChangedFlag) { - autoUnify(0); /* 0 = No 'Congrats' if done */ + autoUnify(0); // 0 = No 'Congrats' if done } if (!g_proofChangedFlag @@ -4959,56 +4936,56 @@ void command(int argc, char *argv[]) { || improveAllIter == 3 || searchAlg == 1)) { print2("No new subproofs were found.\n"); - break; /* out of improveAllIter loop */ + break; // out of improveAllIter loop } if (g_proofChangedFlag) { - g_proofChanged = 1; /* Cumulative flag */ + g_proofChanged = 1; // Cumulative flag } if (!nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { - break; /* Proof is complete */ + break; // Proof is complete } - if (searchAlg == 1) break; /* Old algorithm does just 1st pass */ - } /* Next improveAllIter */ + if (searchAlg == 1) break; // Old algorithm does just 1st pass + } // Next improveAllIter if (g_proofChangedFlag) { if (n > 0) { - /* n is the first step number changed. It will be 0 if - the numbering didn't change e.g. a $e was assigned to - an unknown step. */ + // n is the first step number changed. It will be 0 if + // the numbering didn't change e.g. a $e was assigned to + // an unknown step. print2("Steps %ld and above have been renumbered.\n", n); } processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } if (!nmbrElementIn(1, g_ProofInProgress.proof, -(long)'?')) { - /* This is a redundant call; its purpose is just to give - the message if the proof is complete */ - autoUnify(1); /* 1 = 'Congrats' if done */ + // This is a redundant call; its purpose is just to give + // the message if the proof is complete. + autoUnify(1); // 1 = 'Congrats' if done } - } /* End if IMPROVE ALL */ + } // End if IMPROVE ALL - /* Automatically display new unknown steps - ???Future - add switch to enable/defeat this */ + // Automatically display new unknown steps. + // ???Future - add switch to enable/defeat this. if (g_proofChangedFlag) typeProof(g_proveStatement, - 1 /*pipFlag*/, - 0 /*startStep*/, - 0 /*endStep*/, - 0 /*endIndent*/, - 1 /*essentialFlag*/, - 0 /*renumberFlag*/, - 1 /*unknownFlag*/, - 0 /*notUnifiedFlag*/, - 0 /*reverseFlag*/, - 0 /*noIndentFlag*/, - 0 /*splitColumn*/, - 0 /*skipRepeatedSteps*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); + 1, // pipFlag + 0, // startStep + 0, // endStep + 0, // endIndent + 1, // essentialFlag + 0, // renumberFlag + 1, // unknownFlag + 0, // notUnifiedFlag + 0, // reverseFlag + 0, // noIndentFlag + 0, // splitColumn + 0, // skipRepeatedSteps + 0, // texFlag + 0); // g_htmlFlag continue; - } /* cmdMatches("IMPROVE") */ + } // cmdMatches("IMPROVE") if (cmdMatches("MINIMIZE_WITH")) { @@ -5017,24 +4994,23 @@ void command(int argc, char *argv[]) { printTime = 1; } if (printTime == 1) { - getRunTime(&timeIncr); /* This call just resets the time */ - } - - prntStatus = 0; /* Status flag to help determine messages - 0 = no statement was matched during scan (mainly for - error message if user typo in label field) - 1 = a statement was matched but no shorter proof - 2 = shorter proof found */ - verboseMode = (switchPos("VERBOSE") != 0); /* Verbose mode */ - - /* If no wildcard was used, switch to non-verbose mode - since there is no point to it and an annoying extra blank line - results */ + getRunTime(&timeIncr); // This call just resets the time + } + // Status flag to help determine messages: + // 0 = no statement was matched during scan (mainly for + // error message if user typo in label field). + // 1 = a statement was matched but no shorter proof. + // 2 = shorter proof found. + prntStatus = 0; + verboseMode = (switchPos("VERBOSE") != 0); // Verbose mode + + // If no wildcard was used, switch to non-verbose mode + // since there is no point to it and an annoying extra blank line + // results. if (!(instr(1, g_fullArg[1], "*") || instr(1, g_fullArg[1], "?"))) i = 1; - + // Mode to replace even if it doesn't reduce proof length mayGrowFlag = (switchPos("MAY_GROW") != 0); - /* Mode to replace even if it doesn't reduce proof length */ - exceptPos = switchPos("EXCEPT"); /* Statement match to skip */ + exceptPos = switchPos("EXCEPT"); // Statement match to skip allowNewAxiomsMatchPos = switchPos("ALLOW_NEW_AXIOMS"); if (allowNewAxiomsMatchPos != 0) { @@ -5059,35 +5035,35 @@ void command(int argc, char *argv[]) { mathboxFlag = (switchPos("INCLUDE_MATHBOXES") != 0); - /* Flag to override any "usage locks" placed in the comment markup */ + // Flag to override any "usage locks" placed in the comment markup overrideFlag = (switchPos("OVERRIDE") != 0) || g_globalDiscouragement == 0; - /* If a single statement is specified, don't bother to do certain - actions or print some of the messages */ + // If a single statement is specified, don't bother to do certain + // actions or print some of the messages. hasWildCard = 0; - /* Set hasWildCard only when there are potentially > 1 matches */ + // Set hasWildCard only when there are potentially > 1 matches if (strpbrk(g_fullArg[1], "*?~%,") != NULL) { - /* (See matches() function for processing of these) - "*" 0 or more char match - "?" 1 char match - "=" Most recent PROVE command statement = one statement match - "~" Statement range - "%" List of modified statements - "#" Internal statement number = one statement match - "@" Web page statement number = one statement match - "," Comma-separated fields */ + // (See matches() function for processing of these) + // "*" 0 or more char match + // "?" 1 char match + // "=" Most recent PROVE command statement = one statement match + // "~" Statement range + // "%" List of modified statements + // "#" Internal statement number = one statement match + // "@" Web page statement number = one statement match + // "," Comma-separated fields hasWildCard = 1; } g_proofChangedFlag = 0; - /* Always scan statements in current mathbox, even if - "/ INCLUDE_MATHBOXES" is omitted */ + // Always scan statements in current mathbox, even if + // "/ INCLUDE_MATHBOXES" is omitted. - assignMathboxInfo(); /* In case it hasn't been assigned yet */ + assignMathboxInfo(); // In case it hasn't been assigned yet if (g_proveStatement > g_mathboxStmt) { - /* We're in a mathbox */ + // We're in a mathbox i = getMathboxNum(g_proveStatement); if (i <= 0) bug(1130); thisMathboxStartStmt = g_mathboxStart[i - 1]; @@ -5097,41 +5073,41 @@ void command(int argc, char *argv[]) { copyProofStruct(&saveOrigProof, g_ProofInProgress); - /* 12-Sep-2016 nm TODO replace this w/ compressedProofSize */ - /* Get the current (original) compressed proof length - to compare it when a shorter non-compressed proof is found, to see - if the compressed proof also decreased in size */ - nmbrLet(&nmbrSaveProof, g_ProofInProgress.proof); /* Redundant? */ + // 12-Sep-2016 nm TODO replace this w/ compressedProofSize. + // Get the current (original) compressed proof length + // to compare it when a shorter non-compressed proof is found, to see + // if the compressed proof also decreased in size. + nmbrLet(&nmbrSaveProof, g_ProofInProgress.proof); // Redundant? nmbrLet(&nmbrSaveProof, nmbrSquishProof(g_ProofInProgress.proof)); - /* We only care about length; str1 will be discarded */ + // We only care about length; str1 will be discarded let(&str1, compressProof(nmbrSaveProof, - g_proveStatement, /* statement being proved */ - 0 /* Normal (not "fast") compression */ + g_proveStatement, // statement being proved + 0 // Normal (not "fast") compression )); origCompressedLength = (long)strlen(str1); print2("Bytes refer to compressed proof size, " "steps to uncompressed length.\n"); - /* Scan forward, then reverse, then pick best result */ + // Scan forward, then reverse, then pick best result for (forwRevPass = 1; forwRevPass <= 2; forwRevPass++) { if (forwRevPass == 1) { if (hasWildCard) print2("Scanning forward through statements...\n"); forwFlag = 1; } else { - /* If growth allowed, don't bother with reverse pass */ + // If growth allowed, don't bother with reverse pass if (mayGrowFlag) break; - /* If nothing was found on forward pass, don't bother with rev pass */ + // If nothing was found on forward pass, don't bother with rev pass if (!g_proofChangedFlag) break; - /* If only one statement was specified, don't bother with rev pass */ + // If only one statement was specified, don't bother with rev pass if (!hasWildCard) break; print2("Scanning backward through statements...\n"); forwFlag = 0; - /* Save proof and length from 1st pass; re-initialize */ + // Save proof and length from 1st pass; re-initialize copyProofStruct(&save1stPassProof, g_ProofInProgress); forwardLength = nmbrLen(g_ProofInProgress.proof); forwardCompressedLength = oldCompressedLength; - /* Start over from original proof */ + // Start over from original proof copyProofStruct(&g_ProofInProgress, saveOrigProof); } @@ -5139,8 +5115,8 @@ void command(int argc, char *argv[]) { oldCompressedLength = origCompressedLength; - /* If forwFlag is 0, scan from g_proveStatement-1 to 1 - If forwFlag is 1, scan from 1 to g_proveStatement-1 */ + // If forwFlag is 0, scan from g_proveStatement-1 to 1 + // If forwFlag is 1, scan from 1 to g_proveStatement-1 for (k = forwFlag ? 1 : (g_proveStatement - 1); k * (forwFlag ? 1 : -1) < (forwFlag ? g_proveStatement : 0); k = k + (forwFlag ? 1 : -1)) { @@ -5154,89 +5130,87 @@ void command(int argc, char *argv[]) { continue; if (exceptPos != 0) { - /* Skip any match to the EXCEPT argument */ + // Skip any match to the EXCEPT argument if (matchesList(g_Statement[k].labelName, g_fullArg[exceptPos + 1], '*', '?')) continue; } - if (forbidMatchList[0]) { /* User provided a /FORBID list */ - /* First, we check to make sure we're not trying a statement - in the forbidMatchList directly (traceProof() won't find - this) */ + if (forbidMatchList[0]) { // User provided a /FORBID list. + // First, we check to make sure we're not trying a statement + // in the forbidMatchList directly (traceProof() won't find this). if (matchesList(g_Statement[k].labelName, forbidMatchList, '*', '?')) continue; } - /* Check to see if statement comment specified a usage - restriction */ + // Check to see if statement comment specified a usage restriction. if (!overrideFlag) { if (getMarkupFlag(k, USAGE_DISCOURAGED)) { continue; } } - /* Print individual labels */ - if (prntStatus == 0) prntStatus = 1; /* Matched at least one */ + // Print individual labels + if (prntStatus == 0) prntStatus = 1; // Matched at least one - m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ + m = nmbrLen(g_ProofInProgress.proof); // Original proof length nmbrLet(&nmbrTmp, g_ProofInProgress.proof); - minimizeProof(k /* trial statement */, - g_proveStatement /* statement being proved in MM-PA */, - (char)mayGrowFlag /* mayGrowFlag */); + minimizeProof(k, // trial statement + g_proveStatement, // statement being proved in MM-PA + (char)mayGrowFlag); // mayGrowFlag - n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ + n = nmbrLen(g_ProofInProgress.proof); // New proof length if (!nmbrEq(nmbrTmp, g_ProofInProgress.proof)) { - /* The proof got shorter (or it changed if MAY_GROW) */ - - /* Because of the slow speed of traceBack(), - we only want to check the /FORBID list in the relatively - rare case where a minimization occurred. If the FORBID - list is matched, we then need to revert back to the - original proof. */ - if (forbidMatchList[0]) { /* User provided a /FORBID list */ + // The proof got shorter (or it changed if MAY_GROW) + + // Because of the slow speed of traceBack(), + // we only want to check the /FORBID list in the relatively + // rare case where a minimization occurred. If the FORBID + // list is matched, we then need to revert back to the + // original proof. + if (forbidMatchList[0]) { // User provided a /FORBID list if (g_Statement[k].type == (char)p_) { - /* We only care about tracing $p statements */ - /* See if the TRACE_BACK list includes a match to the - /FORBID argument */ + // We only care about tracing $p statements. + // See if the TRACE_BACK list includes a match to the + // /FORBID argument. if (traceProof(k, - 0, /*essentialFlag*/ - 0, /*axiomFlag*/ + 0, // essentialFlag + 0, // axiomFlag forbidMatchList, - "", /*traceToList*/ - 1 /* testOnlyFlag */, - 0 /* no early exit */)) { - /* Yes, a forbidden statement occurred in traceProof() */ - /* Revert the proof to before minimization */ + "", // traceToList + 1, // testOnlyFlag + 0)) // no early exit + { + // Yes, a forbidden statement occurred in traceProof() + // Revert the proof to before minimization copyProofStruct(&g_ProofInProgress, saveProofForReverting); - /* Skip further printout and flag setting */ - continue; /* Continue at 'Next k' loop end below */ + // Skip further printout and flag setting + continue; // Continue at 'Next k' loop end below } } } - /* Because of the slow speed of traceBack(), - we only want to check the /NO_NEW_AXIOMS_FROM list in the - relatively rare case where a minimization occurred. If the - NO_NEW_AXIOMS_FROM condition applies, we then need to revert - back to the original proof. */ - if (n == n + 0) { /* By default, no new axioms are permitted */ - /*if (noNewAxiomsMatchList[0]) {*/ /* User provided /NO_NEW_AXIOMS_FROM */ - /* If we haven't called trace yet for the theorem being proved, - do it now. */ + // Because of the slow speed of traceBack(), + // we only want to check the /NO_NEW_AXIOMS_FROM list in the + // relatively rare case where a minimization occurred. If the + // NO_NEW_AXIOMS_FROM condition applies, we then need to revert + // back to the original proof. + if (n == n + 0) { // By default, no new axioms are permitted + // if (noNewAxiomsMatchList[0]) { // User provided /NO_NEW_AXIOMS_FROM + // If we haven't called trace yet for the theorem being proved, do it now. if (traceProofFlags[0] == 0) { - /* traceProofWork() was written to use the SAVEd proof and - not the proof in progress. In order to use the proof in - progress, we temporarily put the proof in progress into the - (SAVEd) statement structure to trick traceProofWork() into using - the proof in progress instead of the SAVEd proof */ - /* Use the version of the proof in progress that existed *before* the - MINIMIZE_WITH command was invoked */ + // traceProofWork() was written to use the SAVEd proof and + // not the proof in progress. In order to use the proof in + // progress, we temporarily put the proof in progress into the + // (SAVEd) statement structure to trick traceProofWork() into using + // the proof in progress instead of the SAVEd proof. + // Use the version of the proof in progress that existed *before* the + // MINIMIZE_WITH command was invoked. nmbrLet(&nmbrSaveProof, nmbrSquishProof(saveProofForReverting.proof)); let(&str1, compressProof(nmbrSaveProof, - g_proveStatement, /* statement being proved in MM-PA */ - 0 /* Normal (not "fast") compression */ + g_proveStatement, // statement being proved in MM-PA + 0 // Normal (not "fast") compression )); saveZappedProofSectionPtr = g_Statement[g_proveStatement].proofSectionPtr; @@ -5244,28 +5218,28 @@ void command(int argc, char *argv[]) { = g_Statement[g_proveStatement].proofSectionLen; saveZappedProofSectionChanged = g_Statement[g_proveStatement].proofSectionChanged; - /* Set flag that this is not the original source */ + // Set flag that this is not the original source g_Statement[g_proveStatement].proofSectionChanged = 1; - /* str1 has the new compressed trial proof after minimization */ - /* Put space before and after to satisfy "space around token" - requirement, to prevent possible error messages, and also - add "$." since parseCompressedProof() expects it */ + // str1 has the new compressed trial proof after minimization. + // Put space before and after to satisfy "space around token" + // requirement, to prevent possible error messages, and also + // add "$." since parseCompressedProof() expects it. let(&str1, cat(" ", str1, " $.", NULL)); - /* Don't include the "$." in the length */ + // Don't include the "$." in the length g_Statement[g_proveStatement].proofSectionLen = (long)strlen(str1) - 2; - /* We don't deallocate previous proofSectionPtr content because - we will recover it after the verifyProof() */ + // We don't deallocate previous proofSectionPtr content because + // we will recover it after the verifyProof() g_Statement[g_proveStatement].proofSectionPtr = str1; traceProofWork(g_proveStatement, - 1 /*essentialFlag*/, - "", /*traceToList*/ - &traceProofFlags, /* y/n list of flags */ - &nmbrTmp /* unproved list - ignored */); - free_nmbrString(nmbrTmp); /* Discard */ + 1, // essentialFlag + "", // traceToList + &traceProofFlags, // y/n list of flags + &nmbrTmp); // unproved list - ignored + free_nmbrString(nmbrTmp); // Discard - /* Restore the SAVEd proof */ + // Restore the SAVEd proof g_Statement[g_proveStatement].proofSectionPtr = saveZappedProofSectionPtr; g_Statement[g_proveStatement].proofSectionLen @@ -5274,60 +5248,60 @@ void command(int argc, char *argv[]) { = saveZappedProofSectionChanged; } free_vstring(traceTrialFlags); - traceProofWork(k, /* The trial statement */ - 1 /*essentialFlag*/, - "", /*traceToList*/ - &traceTrialFlags, /* Y/N list of flags */ - &nmbrTmp /* unproved list - ignored */); - free_nmbrString(nmbrTmp); /* Discard */ - j = 1; /* 1 = ok to use trial statement */ + traceProofWork(k, // The trial statement + 1, // essentialFlag + "", // traceToList + &traceTrialFlags, // Y/N list of flags + &nmbrTmp); // unproved list - ignored + free_nmbrString(nmbrTmp); // Discard + j = 1; // 1 = ok to use trial statement for (i = 1; i < g_proveStatement; i++) { - if (g_Statement[i].type != (char)a_) continue; /* Not $a */ + if (g_Statement[i].type != (char)a_) continue; // Not $a + // If the axiom is already used by the proof, we + // don't care if the trial statement depends on it. if (traceProofFlags[i] == 'Y') continue; - /* If the axiom is already used by the proof, we - don't care if the trial statement depends on it */ if (matchesList(g_Statement[i].labelName, allowNewAxiomsMatchList, '*', '?') == 1 && matchesList(g_Statement[i].labelName, noNewAxiomsMatchList, '*', '?') != 1) { - /* If the axiom is in the list to allow and not in the list - to disallow, we don't care if the trial statement depends - on it */ + // If the axiom is in the list to allow and not in the list + // to disallow, we don't care if the trial statement depends + // on it. continue; } if (traceTrialFlags[i] == 'Y') { - /* The trial statement uses an axiom that the current - proof should avoid, so we abort it */ - j = 0; /* 0 = don't use trial statement */ + // The trial statement uses an axiom that the current + // proof should avoid, so we abort it. + j = 0; // 0 = don't use trial statement break; } - } /* next i */ + } // next i if (j == 0) { - /* A forbidden axiom is used by the trial proof */ - /* Revert the proof to before minimization */ + // A forbidden axiom is used by the trial proof. + // Revert the proof to before minimization. copyProofStruct(&g_ProofInProgress, saveProofForReverting); - /* Skip further printout and flag setting */ - continue; /* Continue at 'Next k' loop end below */ + // Skip further printout and flag setting + continue; // Continue at 'Next k' loop end below } - } /* end if (true) */ + } // end if (true) - /* Make sure the compressed proof length - decreased, otherwise revert. Also, we will use the - compressed proof for the $d check next */ + // Make sure the compressed proof length + // decreased, otherwise revert. Also, we will use the + // compressed proof for the $d check next. if (nmbrLen(g_Statement[k].reqDisjVarsA) || !mayGrowFlag) { nmbrLet(&nmbrSaveProof, g_ProofInProgress.proof); nmbrLet(&nmbrSaveProof, nmbrSquishProof(g_ProofInProgress.proof)); let(&str1, compressProof(nmbrSaveProof, - g_proveStatement, /* statement being proved in MM-PA */ - 0 /* Normal (not "fast") compression */ + g_proveStatement, // statement being proved in MM-PA + 0 // Normal (not "fast") compression )); newCompressedLength = (long)strlen(str1); if (!mayGrowFlag && newCompressedLength > oldCompressedLength) { - /* The compressed proof length increased, so don't use it. - (If it stayed the same, we will use it because the uncompressed - length did decrease.) */ - /* Revert the proof to before minimization */ + // The compressed proof length increased, so don't use it. + // (If it stayed the same, we will use it because the uncompressed + // length did decrease.) + // Revert the proof to before minimization. if (verboseMode) { print2( "Reverting \"%s\": Uncompressed steps: old = %ld, new = %ld\n", @@ -5338,20 +5312,20 @@ void command(int argc, char *argv[]) { oldCompressedLength, newCompressedLength); } copyProofStruct(&g_ProofInProgress, saveProofForReverting); - /* Skip further printout and flag setting */ - continue; /* Continue at 'Next k' loop end below */ + // Skip further printout and flag setting + continue; // Continue at 'Next k' loop end below } - } /* if (nmbrLen(g_Statement[k].reqDisjVarsA) || !mayGrowFlag) */ + } // if (nmbrLen(g_Statement[k].reqDisjVarsA) || !mayGrowFlag) - /* Make sure there are no $d violations, otherwise revert */ - /* This requires the str1 from above */ + // Make sure there are no $d violations, otherwise revert. + // This requires the str1 from above. if (nmbrLen(g_Statement[k].reqDisjVarsA)) { - /* There is currently no way to verify a proof that doesn't - read and parse the source directly. This should be - changed in the future to make the program more modular. But - for now, we temporarily zap the source with new compressed - proof and see if there are any $d violations by looking at - the error message output */ + // There is currently no way to verify a proof that doesn't + // read and parse the source directly. This should be + // changed in the future to make the program more modular. But + // for now, we temporarily zap the source with new compressed + // proof and see if there are any $d violations by looking at + // the error message output. saveZappedProofSectionPtr = g_Statement[g_proveStatement].proofSectionPtr; saveZappedProofSectionLen @@ -5359,39 +5333,39 @@ void command(int argc, char *argv[]) { saveZappedProofSectionChanged = g_Statement[g_proveStatement].proofSectionChanged; - /* Set flag that this is not the original source */ + // Set flag that this is not the original source g_Statement[g_proveStatement].proofSectionChanged = 1; - /* str1 has the new compressed trial proof after minimization */ - /* Put space before and after to satisfy "space around token" - requirement, to prevent possible error messages, and also - add "$." since parseCompressedProof() expects it */ + // str1 has the new compressed trial proof after minimization. + // Put space before and after to satisfy "space around token" + // requirement, to prevent possible error messages, and also + // add "$." since parseCompressedProof() expects it. let(&str1, cat(" ", str1, " $.", NULL)); - /* Don't include the "$." in the length */ + // Don't include the "$." in the length g_Statement[g_proveStatement].proofSectionLen = (long)strlen(str1) - 2; - /* We don't deallocate previous proofSectionPtr content because - we will recover it after the verifyProof() */ + // We don't deallocate previous proofSectionPtr content because + // we will recover it after the verifyProof(). g_Statement[g_proveStatement].proofSectionPtr = str1; - g_outputToString = 1; /* Suppress error messages */ - /* parseProof, verifyProof, cleanWrkProof must be - called in sequence to assign the g_WrkProof structure, verify - the proof, and deallocate the g_WrkProof structure. Either none - of them or all of them must be called. */ + g_outputToString = 1; // Suppress error messages + // parseProof, verifyProof, cleanWrkProof must be + // called in sequence to assign the g_WrkProof structure, verify + // the proof, and deallocate the g_WrkProof structure. Either none + // of them or all of them must be called. parseProof(g_proveStatement); - verifyProof(g_proveStatement); /* Must be called even if error - occurred in parseProof, to init RPN stack - for cleanWrkProof() */ - /* don't change proof if there is an error - (which could be pre-existing). */ + // Must be called even if error occurred in parseProof, + // to init RPN stack for cleanWrkProof(). + verifyProof(g_proveStatement); + // don't change proof if there is an error + // (which could be pre-existing). i = (g_WrkProof.errorSeverity > 1); - /**** Here we look at the screen output sent to a string. - This is rather crude, and someday the ability to - check proofs and $d violations should be modularized *****/ + // **** Here we look at the screen output sent to a string. + // This is rather crude, and someday the ability to + // check proofs and $d violations should be modularized ***** j = instr(1, g_printString, "There is a disjoint variable ($d) violation"); - g_outputToString = 0; /* Restore to normal output */ - free_vstring(g_printString); /* Clear out the stored error messages */ - cleanWrkProof(); /* Deallocate verifyProof storage */ + g_outputToString = 0; // Restore to normal output + free_vstring(g_printString); // Clear out the stored error messages + cleanWrkProof(); // Deallocate verifyProof storage g_Statement[g_proveStatement].proofSectionPtr = saveZappedProofSectionPtr; g_Statement[g_proveStatement].proofSectionLen @@ -5399,28 +5373,28 @@ void command(int argc, char *argv[]) { g_Statement[g_proveStatement].proofSectionChanged = saveZappedProofSectionChanged; if (i != 0 || j != 0) { - /* There was a verify proof error (j!=0) or $d violation (i!=0) - so don't used minimized proof */ - /* Revert the proof to before minimization */ + // There was a verify proof error (j!=0) or $d violation (i!=0) + // so don't used minimized proof. + // Revert the proof to before minimization. copyProofStruct(&g_ProofInProgress, saveProofForReverting); - /* Skip further printout and flag setting */ - continue; /* Continue at 'Next k' loop end below */ + // Skip further printout and flag setting. + continue; // Continue at 'Next k' loop end below. } - } /* if (nmbrLen(g_Statement[k].reqDisjVarsA)) */ + } // if (nmbrLen(g_Statement[k].reqDisjVarsA)) - /* Warn user if a discouraged statement is overridden */ + // Warn user if a discouraged statement is overridden if (getMarkupFlag(k, USAGE_DISCOURAGED)) { if (!overrideFlag) bug(1126); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis print2( ">>> ?Warning: Overriding discouraged usage of \"%s\".\n", g_Statement[k].labelName); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis } if (!mayGrowFlag) { - /* Note: this is the length BEFORE indentation and wrapping, - so it is less than SHOW PROOF ... /SIZE */ + // Note: this is the length BEFORE indentation and wrapping, + // so it is less than SHOW PROOF ... /SIZE if (newCompressedLength < oldCompressedLength) { print2( "Proof of \"%s\" decreased from %ld to %ld bytes using \"%s\".\n", @@ -5438,7 +5412,7 @@ void command(int argc, char *argv[]) { " (Uncompressed steps decreased from %ld to %ld).\n", m, n ); } - /* (We don't care about compressed length if MAY_GROW) */ + // (We don't care about compressed length if MAY_GROW) oldCompressedLength = newCompressedLength; } @@ -5449,18 +5423,18 @@ void command(int argc, char *argv[]) { g_Statement[g_proveStatement].labelName, m, n, g_Statement[k].labelName); } - /* MAY_GROW possibility */ + // MAY_GROW possibility if (m < n) print2( "Proof of \"%s\" increased from %ld to %ld steps using \"%s\".\n", g_Statement[g_proveStatement].labelName, m, n, g_Statement[k].labelName); - /* MAY_GROW possibility */ + // MAY_GROW possibility if (m == n) print2( "Proof of \"%s\" remained at %ld steps using \"%s\".\n", g_Statement[g_proveStatement].labelName, m, g_Statement[k].labelName); - /* See if it's in another mathbox; if so, let user know */ + // See if it's in another mathbox; if so, let user know assignMathboxInfo(); if (k > g_mathboxStmt && g_proveStatement > g_mathboxStmt) { if (k < g_mathboxStart[getMathboxNum(g_proveStatement) - 1]) { @@ -5472,18 +5446,17 @@ void command(int argc, char *argv[]) { } } - prntStatus = 2; /* Found one */ + prntStatus = 2; // Found one g_proofChangedFlag = 1; - /* Save the changed proof in case we have to restore - it later */ + // Save the changed proof in case we have to restore it later. copyProofStruct(&saveProofForReverting, g_ProofInProgress); } - } /* Next k (statement) */ + } // Next k (statement) if (g_proofChangedFlag && forwRevPass == 2) { - /* Check whether the reverse pass found a better proof than the - forward pass */ + // Check whether the reverse pass found a better proof than the + // forward pass. if (verboseMode) { print2( "Forward vs. backward: %ld vs. %ld bytes; %ld vs. %ld steps\n", @@ -5495,14 +5468,14 @@ void command(int argc, char *argv[]) { if (oldCompressedLength < forwardCompressedLength || (oldCompressedLength == forwardCompressedLength && nmbrLen(g_ProofInProgress.proof) < forwardLength)) { - /* The reverse pass was better */ + // The reverse pass was better print2("The backward scan results were used.\n"); } else { copyProofStruct(&g_ProofInProgress, save1stPassProof); print2("The forward scan results were used.\n"); } } - } /* next forwRevPass */ + } // next forwRevPass if (prntStatus == 1 && !mayGrowFlag) print2("No shorter proof was found.\n"); @@ -5523,37 +5496,37 @@ void command(int argc, char *argv[]) { g_Statement[g_proveStatement].labelName); } - free_vstring(str1); /* Deallocate memory */ - free_nmbrString(nmbrSaveProof); /* Deallocate memory */ + free_vstring(str1); // Deallocate memory + free_nmbrString(nmbrSaveProof); // Deallocate memory - /* Clear these Y/N trace strings unconditionally since new axioms are no - longer allowed by default, so they may become set regardless of - qualifiers */ - free_vstring(traceProofFlags); /* Deallocate memory */ - free_vstring(traceTrialFlags); /* Deallocate memory */ + // Clear these Y/N trace strings unconditionally since new axioms are no + // longer allowed by default, so they may become set regardless of + // qualifiers. + free_vstring(traceProofFlags); // Deallocate memory + free_vstring(traceTrialFlags); // Deallocate memory - if (allowNewAxiomsMatchList[0]) { /* User provided /NO_NEW_AXIOMS_FROM list */ - free_vstring(allowNewAxiomsMatchList); /* Deallocate memory */ + if (allowNewAxiomsMatchList[0]) { // User provided /NO_NEW_AXIOMS_FROM list + free_vstring(allowNewAxiomsMatchList); // Deallocate memory } - if (noNewAxiomsMatchList[0]) { /* User provided /ALLOW_NEW_AXIOMS list */ - free_vstring(noNewAxiomsMatchList); /* Deallocate memory */ + if (noNewAxiomsMatchList[0]) { // User provided /ALLOW_NEW_AXIOMS list + free_vstring(noNewAxiomsMatchList); // Deallocate memory } - if (forbidMatchList[0]) { /* User provided a /FORBID list */ - free_vstring(forbidMatchList); /* Deallocate memory */ + if (forbidMatchList[0]) { // User provided a /FORBID list + free_vstring(forbidMatchList); // Deallocate memory } - deallocProofStruct(&saveProofForReverting); /* Deallocate memory */ - deallocProofStruct(&saveOrigProof); /* Deallocate memory */ - deallocProofStruct(&save1stPassProof); /* Deallocate memory */ + deallocProofStruct(&saveProofForReverting); // Deallocate memory + deallocProofStruct(&saveOrigProof); // Deallocate memory + deallocProofStruct(&save1stPassProof); // Deallocate memory if (g_proofChangedFlag) { - g_proofChanged = 1; /* Cumulative flag */ + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } continue; - } /* End if MINIMIZE_WITH */ + } // End if MINIMIZE_WITH if (cmdMatches("EXPAND")) { @@ -5562,7 +5535,7 @@ void command(int argc, char *argv[]) { s = compressedProofSize(nmbrSaveProof, g_proveStatement); for (i = g_proveStatement - 1; i >= 1; i--) { - if (g_Statement[i].type != (char)p_) continue; /* Not a $p */ + if (g_Statement[i].type != (char)p_) continue; // Not a $p if (!matchesList(g_Statement[i].labelName, g_fullArg[1], '*', '?')) { continue; } @@ -5586,12 +5559,12 @@ void command(int argc, char *argv[]) { } if (g_proofChangedFlag) { - g_proofChanged = 1; /* Cumulative flag */ - /* Clear the existing proof structure */ + g_proofChanged = 1; // Cumulative flag + // Clear the existing proof structure deallocProofStruct(&g_ProofInProgress); - /* Then rebuild proof structure from new proof nmbrTmp */ + // Then rebuild proof structure from new proof nmbrTmp initProofStruct(&g_ProofInProgress, nmbrTmp, g_proveStatement); - /* Save the new proof structure on the undo stack */ + // Save the new proof structure on the undo stack processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } else { print2("No expansion occurred. The proof was not changed.\n"); @@ -5599,12 +5572,12 @@ void command(int argc, char *argv[]) { free_nmbrString(nmbrSaveProof); free_nmbrString(nmbrTmp); continue; - } /* EXPAND */ + } // EXPAND if (cmdMatches("DELETE STEP") || (cmdMatches("DELETE ALL"))) { if (cmdMatches("DELETE STEP")) { - s = (long)val(g_fullArg[2]); /* Step number */ + s = (long)val(g_fullArg[2]); // Step number } else { s = nmbrLen(g_ProofInProgress.proof); } @@ -5612,14 +5585,14 @@ void command(int argc, char *argv[]) { print2("?Step %ld is unknown and cannot be deleted.\n", s); continue; } - m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ + m = nmbrLen(g_ProofInProgress.proof); // Original proof length if (s > m || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", m); continue; } deleteSubProof(s - 1); - n = nmbrLen(g_ProofInProgress.proof); /* New proof length */ + n = nmbrLen(g_ProofInProgress.proof); // New proof length if (m == n) { print2("Step %ld was deleted.\n", s); } else { @@ -5636,25 +5609,25 @@ void command(int argc, char *argv[]) { } } - /* Automatically display new unknown steps - ???Future - add switch to enable/defeat this */ + // Automatically display new unknown steps + // ???Future - add switch to enable/defeat this typeProof(g_proveStatement, - 1 /*pipFlag*/, - 0 /*startStep*/, - 0 /*endStep*/, - 0 /*endIndent*/, - 1 /*essentialFlag*/, - 0 /*renumberFlag*/, - 1 /*unknownFlag*/, - 0 /*notUnifiedFlag*/, - 0 /*reverseFlag*/, - 0 /*noIndentFlag*/, - 0 /*splitColumn*/, - 0 /*skipRepeatedSteps*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); - - g_proofChanged = 1; /* Cumulative flag */ + 1, // pipFlag + 0, // startStep + 0, // endStep + 0, // endIndent + 1, // essentialFlag + 0, // renumberFlag + 1, // unknownFlag + 0, // notUnifiedFlag + 0, // reverseFlag + 0, // noIndentFlag + 0, // splitColumn + 0, // skipRepeatedSteps + 0, // texFlag + 0); // g_htmlFlag + + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; @@ -5662,29 +5635,29 @@ void command(int argc, char *argv[]) { if (cmdMatches("DELETE FLOATING_HYPOTHESES")) { - /* Get the essential step flags */ + // Get the essential step flags nmbrLet(&nmbrTmp, nmbrGetEssential(g_ProofInProgress.proof)); - m = nmbrLen(g_ProofInProgress.proof); /* Original proof length */ + m = nmbrLen(g_ProofInProgress.proof); // Original proof length - n = 0; /* Earliest step that changed */ + n = 0; // Earliest step that changed g_proofChangedFlag = 0; for (s = m; s > 0; s--) { - /* Skip essential steps and unknown steps */ - if (nmbrTmp[s - 1] == 1) continue; /* Not floating */ - if ((g_ProofInProgress.proof)[s - 1] == -(long)'?') continue; /* Unknown */ + // Skip essential steps and unknown steps + if (nmbrTmp[s - 1] == 1) continue; // Not floating + if ((g_ProofInProgress.proof)[s - 1] == -(long)'?') continue; // Unknown - /* Get the subproof length at step s */ + // Get the subproof length at step s q = subproofLen(g_ProofInProgress.proof, s - 1); deleteSubProof(s - 1); - n = s - q + 1; /* Save earliest step changed */ + n = s - q + 1; // Save earliest step changed g_proofChangedFlag = 1; - s = s - q + 1; /* Adjust step position to account for deleted subpr */ - } /* Next step s */ + s = s - q + 1; // Adjust step position to account for deleted subpr + } // Next step s if (g_proofChangedFlag) { print2("All floating-hypothesis steps were deleted.\n"); @@ -5693,70 +5666,70 @@ void command(int argc, char *argv[]) { print2("Steps %ld and above have been renumbered.\n", n); } - /* Automatically display new unknown steps - ???Future - add switch to enable/defeat this */ + // Automatically display new unknown steps + // ???Future - add switch to enable/defeat this typeProof(g_proveStatement, - 1 /*pipFlag*/, - 0 /*startStep*/, - 0 /*endStep*/, - 0 /*endIndent*/, - 1 /*essentialFlag*/, - 0 /*renumberFlag*/, - 1 /*unknownFlag*/, - 0 /*notUnifiedFlag*/, - 0 /*reverseFlag*/, - 0 /*noIndentFlag*/, - 0 /*splitColumn*/, - 0 /*skipRepeatedSteps*/, - 0 /*texFlag*/, - 0 /*g_htmlFlag*/); - - g_proofChanged = 1; /* Cumulative flag */ + 1, // pipFlag + 0, // startStep + 0, // endStep + 0, // endIndent + 1, // essentialFlag + 0, // renumberFlag + 1, // unknownFlag + 0, // notUnifiedFlag + 0, // reverseFlag + 0, // noIndentFlag + 0, // splitColumn + 0, // skipRepeatedSteps + 0, // texFlag + 0); // g_htmlFlag + + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); } else { print2("?There are no floating-hypothesis steps to delete.\n"); } continue; - } /* End if DELETE FLOATING_HYPOTHESES */ + } // End if DELETE FLOATING_HYPOTHESES if (cmdMatches("INITIALIZE")) { if (cmdMatches("INITIALIZE ALL")) { i = nmbrLen(g_ProofInProgress.proof); - /* Reset the dummy variable counter (all will be refreshed) */ + // Reset the dummy variable counter (all will be refreshed) g_pipDummyVars = 0; - /* Initialize all steps */ + // Initialize all steps for (j = 0; j < i; j++) { initStep(j); } - /* Assign known subproofs */ + // Assign known subproofs assignKnownSubProofs(); print2("All steps have been initialized.\n"); - g_proofChanged = 1; /* Cumulative flag */ + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; } if (cmdMatches("INITIALIZE USER")) { i = nmbrLen(g_ProofInProgress.proof); - /* Delete all LET STEP assignments */ + // Delete all LET STEP assignments for (j = 0; j < i; j++) { nmbrLet((nmbrString **)(&((g_ProofInProgress.user)[j])), NULL_NMBRSTRING); } print2( "All LET STEP user assignments have been initialized (i.e. deleted).\n"); - g_proofChanged = 1; /* Cumulative flag */ + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; } - s = (long)val(g_fullArg[2]); /* Step number */ + s = (long)val(g_fullArg[2]); // Step number if (s > nmbrLen(g_ProofInProgress.proof) || s < 1) { print2("?The step must be in the range from 1 to %ld.\n", nmbrLen(g_ProofInProgress.proof)); @@ -5765,47 +5738,47 @@ void command(int argc, char *argv[]) { initStep(s - 1); - /* Also delete LET STEPs, per HELP INITIALIZE */ + // Also delete LET STEPs, per HELP INITIALIZE nmbrLet((nmbrString **)(&((g_ProofInProgress.user)[s - 1])), NULL_NMBRSTRING); print2("Step %ld and its hypotheses have been initialized.\n", s); - g_proofChanged = 1; /* Cumulative flag */ + g_proofChanged = 1; // Cumulative flag processUndoStack(&g_ProofInProgress, PUS_PUSH, g_fullArgString, 0); continue; } if (cmdMatches("SEARCH")) { if (switchPos("ALL")) { - m = 1; /* Include $e, $f statements */ + m = 1; // Include $e, $f statements } else { - m = 0; /* Show $a, $p only */ + m = 0; // Show $a, $p only } if (switchPos("JOIN")) { - joinFlag = 1; /* Join $e's to $a,$p for matching */ + joinFlag = 1; // Join $e's to $a,$p for matching } else { - joinFlag = 0; /* Search $a,$p by themselves */ + joinFlag = 0; // Search $a,$p by themselves } if (switchPos("COMMENTS")) { - n = 1; /* Search comments */ + n = 1; // Search comments } else { - n = 0; /* Search statement math symbols */ + n = 0; // Search statement math symbols } - let(&str1, g_fullArg[2]); /* String to match */ + let(&str1, g_fullArg[2]); // String to match - if (n) { /* COMMENTS switch */ - /* Trim leading, trailing spaces; reduce white space to space; - convert to upper case */ + if (n) { // COMMENTS switch + // Trim leading, trailing spaces; reduce white space to space; + // convert to upper case. let(&str1, edit(str1, 8 + 16 + 128 + 32)); - } else { /* No COMMENTS switch */ - /* Trim leading, trailing spaces; reduce white space to space */ + } else { // No COMMENTS switch + // Trim leading, trailing spaces; reduce white space to space let(&str1, edit(str1, 8 + 16 + 128)); - /* Change all spaces to double spaces */ + // Change all spaces to double spaces q = (long)strlen(str1); let(&str3, space(q + q)); s = 0; @@ -5818,93 +5791,93 @@ void command(int argc, char *argv[]) { } let(&str1, left(str3, q + s)); - /* Find single-character-match wildcard argument "$?" - (or "?" for convenience). Use ASCII 3 for the exactly-1-char - wildcard character. This is a single-character - match, not a single-token match: we need "??" to match "ph". */ + // Find single-character-match wildcard argument "$?" + // (or "?" for convenience). Use ASCII 3 for the exactly-1-char + // wildcard character. This is a single-character + // match, not a single-token match: we need "??" to match "ph". while (1) { p = instr(1, str1, "$?"); if (!p) break; let(&str1, cat(left(str1, p - 1), chr(3), right(str1, p + 2), NULL)); } - /* Allow just "?" for convenience. */ + // Allow just "?" for convenience. while (1) { p = instr(1, str1, "?"); if (!p) break; let(&str1, cat(left(str1, p - 1), chr(3), right(str1, p + 1), NULL)); } - /* Change wildcard to ASCII 2 (to be different from printable chars) */ - /* 1-Mar-02 nm - (Why are we matching with and without space? I'm not sure.) */ - /* 30-Jan-06 nm Answer: We need the double-spacing, and the removal - of space in the "with spaces" case, so that "ph $ ph" will match - "ph ph" (0-token case) - "ph $ ph" won't match this in the - (character-based, not token-based) matches(). The "with spaces" - case is for matching whole tokens, whereas the "without spaces" - case is for matching part of a token. */ + // Change wildcard to ASCII 2 (to be different from printable chars). + // 1-Mar-02 nm - (Why are we matching with and without space? I'm not sure.). + // 30-Jan-06 nm Answer: We need the double-spacing, and the removal + // of space in the "with spaces" case, so that "ph $ ph" will match + // "ph ph" (0-token case) - "ph $ ph" won't match this in the + // (character-based, not token-based) matches(). The "with spaces" + // case is for matching whole tokens, whereas the "without spaces" + // case is for matching part of a token. while (1) { p = instr(1, str1, " $* "); if (!p) break; - /* This removes the space before and after the $* */ + // This removes the space before and after the $* let(&str1, cat(left(str1, p - 1), chr(2), right(str1, p + 4), NULL)); } while (1) { p = instr(1, str1, "$*"); if (!p) break; - /* This simply replaces $* with chr(2) */ + // This simply replaces $* with chr(2) let(&str1, cat(left(str1, p - 1), chr(2), right(str1, p + 2), NULL)); } - /* Also allow a plain $ as a wildcard, for convenience. */ + // Also allow a plain $ as a wildcard, for convenience. while (1) { p = instr(1, str1, " $ "); if (!p) break; let(&str1, cat(left(str1, p - 1), chr(2), right(str1, p + 3), NULL)); } while (1) { - /* Note: the "$" shortcut must be done last to avoid picking up - "$*" and "$?". */ + // Note: the "$" shortcut must be done last to avoid picking up + // "$*" and "$?". p = instr(1, str1, "$"); if (!p) break; let(&str1, cat(left(str1, p - 1), chr(2), right(str1, p + 1), NULL)); } - /* Add wildcards to beginning and end to match middle of any string */ + // Add wildcards to beginning and end to match middle of any string let(&str1, cat(chr(2), " ", str1, " ", chr(2), NULL)); - } /* End no COMMENTS switch */ + } // End no COMMENTS switch for (i = 1; i <= g_statements; i++) { - if (!g_Statement[i].labelName[0]) continue; /* No label */ + if (!g_Statement[i].labelName[0]) continue; // No label if (!m && g_Statement[i].type != (char)p_ && g_Statement[i].type != (char)a_) { - continue; /* No /ALL switch */ + continue; // No /ALL switch } if (!matchesList(g_Statement[i].labelName, g_fullArg[1], '*', '?')) continue; - if (n) { /* COMMENTS switch */ + if (n) { // COMMENTS switch free_vstring(str2); - str2 = getDescription(i); /* str2 must be deallocated here */ - /* Strip linefeeds and reduce spaces; cvt to uppercase */ + str2 = getDescription(i); // str2 must be deallocated here + // Strip linefeeds and reduce spaces; cvt to uppercase j = instr(1, edit(str2, 4 + 8 + 16 + 128 + 32), str1); - if (!j) { /* No match */ + if (!j) { // No match free_vstring(str2); continue; } - /* Strip linefeeds and reduce spaces */ + // Strip linefeeds and reduce spaces let(&str2, edit(str2, 4 + 8 + 16 + 128)); - j = j + ((long)strlen(str1) / 2); /* Center of match location */ + j = j + ((long)strlen(str1) / 2); // Center of match location p = g_screenWidth - 7 - (long)strlen(str((double)i)) - + // Longest comment portion that will fit in one line (long)strlen(g_Statement[i].labelName); - /* Longest comment portion that will fit in one line */ - q = (long)strlen(str2); /* Length of comment */ - if (q <= p) { /* Use entire comment */ + q = (long)strlen(str2); // Length of comment + if (q <= p) { // Use entire comment let(&str3, str2); } else { - if (q - j <= p / 2) { /* Use right part of comment */ + if (q - j <= p / 2) { // Use right part of comment let(&str3, cat("...", right(str2, q - p + 4), NULL)); } else { - if (j <= p / 2) { /* Use left part of comment */ + if (j <= p / 2) { // Use left part of comment let(&str3, cat(left(str2, p - 3), "...", NULL)); - } else { /* Use middle part of comment */ + } else { // Use middle part of comment let(&str3, cat("...", mid(str2, j - p / 2, p - 6), "...", NULL)); } @@ -5913,13 +5886,13 @@ void command(int argc, char *argv[]) { print2("%s\n", cat(str((double)i), " ", g_Statement[i].labelName, " $", chr(g_Statement[i].type), " \"", str3, "\"", NULL)); free_vstring(str2); - } else { /* No COMMENTS switch */ + } else { // No COMMENTS switch let(&str2,nmbrCvtMToVString(g_Statement[i].mathString)); - tmpFlag = 0; /* Flag that $p or $a is already in string */ + tmpFlag = 0; // Flag that $p or $a is already in string if (joinFlag && (g_Statement[i].type == (char)p_ || g_Statement[i].type == (char)a_)) { - /* If $a or $p, prepend $e's to string to match */ + // If $a or $p, prepend $e's to string to match k = nmbrLen(g_Statement[i].reqHypList); for (j = k - 1; j >= 0; j--) { p = g_Statement[i].reqHypList[j]; @@ -5928,12 +5901,12 @@ void command(int argc, char *argv[]) { nmbrCvtMToVString(g_Statement[p].mathString), tmpFlag ? "" : cat(" $", chr(g_Statement[i].type), NULL), " ", str2, NULL)); - tmpFlag = 1; /* Flag that a $p or $a was added */ + tmpFlag = 1; // Flag that a $p or $a was added } } } - /* Change all spaces to double spaces */ + // Change all spaces to double spaces q = (long)strlen(str2); let(&str3, space(q + q)); s = 0; @@ -5947,20 +5920,20 @@ void command(int argc, char *argv[]) { let(&str2, left(str3, q + s)); let(&str2, cat(" ", str2, " ", NULL)); - /* We should use matches() and not matchesList() here, because - commas can be legal token characters in math symbols */ - if (!matches(str2, str1, 2/* ascii 2 0-or-more-token match char*/, - 3/* ascii 3 single-token-match char*/)) + // We should use matches() and not matchesList() here, because + // commas can be legal token characters in math symbols. + if (!matches(str2, str1, 2, // ascii 2 0-or-more-token match char + 3)) // ascii 3 single-token-match char continue; - let(&str2, edit(str2, 8 + 16 + 128)); /* Trim leading, trailing - spaces; reduce white space to space */ + // Trim leading, trailing spaces; reduce white space to space. + let(&str2, edit(str2, 8 + 16 + 128)); printLongLine(cat(str((double)i)," ", g_Statement[i].labelName, tmpFlag ? "" : cat(" $", chr(g_Statement[i].type), NULL), " ", str2, NULL), " ", " "); - } /* End no COMMENTS switch */ - } /* Next i */ + } // End no COMMENTS switch + } // Next i continue; } @@ -6019,7 +5992,7 @@ void command(int argc, char *argv[]) { } if (cmdMatches("SET SEARCH_LIMIT")) { - s = (long)val(g_fullArg[2]); /* Timeout value */ + s = (long)val(g_fullArg[2]); // Timeout value print2("IMPROVE search limit has been changed from %ld to %ld\n", g_userMaxProveFloat, s); g_userMaxProveFloat = s; @@ -6027,10 +6000,10 @@ void command(int argc, char *argv[]) { } if (cmdMatches("SET WIDTH")) { - s = (long)val(g_fullArg[2]); /* Screen width value */ + s = (long)val(g_fullArg[2]); // Screen width value - /* TODO: figure out why s=2 crashes program! */ - if (s < 3) s = 3; /* Less than 3 may cause a segmentation fault */ + // TODO: figure out why s=2 crashes program! + if (s < 3) s = 3; // Less than 3 may cause a segmentation fault i = g_screenWidth; g_screenWidth = s; print2("Screen width has been changed from %ld to %ld.\n", @@ -6039,14 +6012,14 @@ void command(int argc, char *argv[]) { } if (cmdMatches("SET HEIGHT")) { - s = (long)val(g_fullArg[2]); /* Screen height value */ - if (s < 2) s = 2; /* Less than 2 makes no sense */ + s = (long)val(g_fullArg[2]); // Screen height value + if (s < 2) s = 2; // Less than 2 makes no sense i = g_screenHeight; g_screenHeight = s - 1; print2("Screen height has been changed from %ld to %ld.\n", i + 1, s); - /* g_screenHeight is one less than the physical screen to account for the - prompt line after pausing. */ + // g_screenHeight is one less than the physical screen to account for the + // prompt line after pausing. continue; } @@ -6057,12 +6030,12 @@ void command(int argc, char *argv[]) { } else if (!strcmp(g_fullArg[2], "OFF")) { print2( "\"(...is discouraged.)\" markup tags are no longer honored.\n"); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis print2( ">>> ?Warning: This setting is intended for advanced users only. Please turn\n"); print2( ">>> it back ON if you are not intimately familiar with this database.\n"); - /* print2("\n"); */ /* Enable for more emphasis */ + // print2("\n"); // Enable for more emphasis g_globalDiscouragement = 0; } else { bug(1129); @@ -6078,15 +6051,15 @@ void command(int argc, char *argv[]) { } if (cmdMatches("SET ROOT_DIRECTORY")) { - let(&str1, g_rootDirectory); /* Save previous one */ - let(&g_rootDirectory, edit(g_fullArg[2], 2/*discard spaces,tabs*/)); - if (g_rootDirectory[0] != 0) { /* Not an empty directory path */ - /* Add trailing "/" to g_rootDirectory if missing */ + let(&str1, g_rootDirectory); // Save previous one + let(&g_rootDirectory, edit(g_fullArg[2], 2 /* discard spaces, tabs */)); + if (g_rootDirectory[0] != 0) { // Not an empty directory path + // Add trailing "/" to g_rootDirectory if missing if (instr(1, g_rootDirectory, "\\") != 0 || instr(1, g_input_fn, "\\") != 0 || instr(1, g_output_fn, "\\") != 0 ) { - /* Using Windows-style path (not really supported, but at least - make full path consistent) */ + // Using Windows-style path (not really supported, but at least + // make full path consistent). if (g_rootDirectory[strlen(g_rootDirectory) - 1] != '\\') { let(&g_rootDirectory, cat(g_rootDirectory, "\\", NULL)); } @@ -6105,17 +6078,17 @@ void command(int argc, char *argv[]) { } if (cmdMatches("SET UNDO")) { - s = (long)val(g_fullArg[2]); /* Maximum UNDOs */ - if (s < 0) s = 0; /* Less than 0 UNDOs makes no sense */ - /* Reset the stack size if it changed */ + s = (long)val(g_fullArg[2]); // Maximum UNDOs + if (s < 0) s = 0; // Less than 0 UNDOs makes no sense + // Reset the stack size if it changed if (processUndoStack(NULL, PUS_GET_SIZE, "", 0) != s) { print2( "The maximum number of UNDOs was changed from %ld to %ld\n", processUndoStack(NULL, PUS_GET_SIZE, "", 0), s); processUndoStack(NULL, PUS_NEW_SIZE, "", s); if (g_PFASmode == 1) { - /* If we're in the Proof Assistant, assign the first stack - entry with the current proof (the stack was erased) */ + // If we're in the Proof Assistant, assign the first stack + // entry with the current proof (the stack was erased). processUndoStack(&g_ProofInProgress, PUS_PUSH, "", 0); } } else { @@ -6125,7 +6098,7 @@ void command(int argc, char *argv[]) { } if (cmdMatches("SET UNIFICATION_TIMEOUT")) { - s = (long)val(g_fullArg[2]); /* Timeout value */ + s = (long)val(g_fullArg[2]); // Timeout value print2("Unification timeout has been changed from %ld to %ld\n", g_userMaxUnifTrials,s); g_userMaxUnifTrials = s; @@ -6133,10 +6106,10 @@ void command(int argc, char *argv[]) { } if (cmdMatches("OPEN LOG")) { - /* Open a log file */ + // Open a log file let(&g_logFileName, g_fullArg[2]); - g_logFilePtr = fSafeOpen(g_logFileName, "w", 0/*noVersioningFlag*/); - if (!g_logFilePtr) continue; /* Couldn't open it (err msg was provided) */ + g_logFilePtr = fSafeOpen(g_logFileName, "w", 0 /* noVersioningFlag */); + if (!g_logFilePtr) continue; // Couldn't open it (err msg was provided) g_logFileOpenFlag = 1; print2("The log file \"%s\" was opened %s %s.\n",g_logFileName, date(),time_()); @@ -6144,7 +6117,7 @@ void command(int argc, char *argv[]) { } if (cmdMatches("CLOSE LOG")) { - /* Close the log file */ + // Close the log file if (!g_logFileOpenFlag) { print2("?Sorry, there is no log file currently open.\n"); } else { @@ -6160,8 +6133,8 @@ void command(int argc, char *argv[]) { if (cmdMatches("OPEN TEX")) { if (g_texDefsRead) { if (g_htmlFlag) { - /* Actually it isn't clear to me this is still the case, but - to be safe I left it in */ + // 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"); @@ -6169,7 +6142,7 @@ void command(int argc, char *argv[]) { } } - /* Open a TeX file */ + // Open a TeX file let(&g_texFileName,g_fullArg[2]); if (switchPos("NO_HEADER")) { texHeaderFlag = 0; @@ -6182,8 +6155,8 @@ void command(int argc, char *argv[]) { } else { g_oldTexFlag = 0; } - g_texFilePtr = fSafeOpen(g_texFileName, "w", 0/*noVersioningFlag*/); - if (!g_texFilePtr) continue; /* Couldn't open it (err msg was provided) */ + g_texFilePtr = fSafeOpen(g_texFileName, "w", 0 /* noVersioningFlag */); + if (!g_texFilePtr) continue; // Couldn't open it (err msg was provided) g_texFileOpenFlag = 1; print2("Created %s output file \"%s\".\n", g_htmlFlag ? "HTML" : "LaTeX", g_texFileName); @@ -6193,7 +6166,7 @@ void command(int argc, char *argv[]) { } if (cmdMatches("CLOSE TEX")) { - /* Close the TeX file */ + // Close the TeX file if (!g_texFileOpenFlag) { print2("?Sorry, there is no LaTeX file currently open.\n"); } else { @@ -6207,24 +6180,24 @@ void command(int argc, char *argv[]) { continue; } - /* Similar to Unix 'more' */ + // Similar to Unix 'more' if (cmdMatches("MORE")) { - list1_fp = fSafeOpen(g_fullArg[1], "r", 0/*noVersioningFlag*/); - if (!list1_fp) continue; /* Couldn't open it (error msg was provided) */ + list1_fp = fSafeOpen(g_fullArg[1], "r", 0 /* noVersioningFlag */); + if (!list1_fp) continue; // Couldn't open it (error msg was provided) while (1) { - if (!linput(list1_fp, NULL, &str1)) break; /* End of file */ - /* Print a line on the screen */ - if (!print2("%s\n", str1)) break; /* User typed Q */ + if (!linput(list1_fp, NULL, &str1)) break; // End of file + // Print a line on the screen + if (!print2("%s\n", str1)) break; // User typed Q } fclose(list1_fp); continue; - } /* end MORE */ + } // end MORE if (cmdMatches("FILE SEARCH")) { - /* Search the contents of a file and type on the screen */ + // Search the contents of a file and type on the screen - type_fp = fSafeOpen(g_fullArg[2], "r", 0/*noVersioningFlag*/); - if (!type_fp) continue; /* Couldn't open it (error msg was provided) */ + type_fp = fSafeOpen(g_fullArg[2], "r", 0 /* noVersioningFlag */); + if (!type_fp) continue; // Couldn't open it (error msg was provided) fromLine = 0; toLine = 0; searchWindow = 0; @@ -6234,25 +6207,25 @@ void command(int argc, char *argv[]) { if (i) toLine = (long)val(g_fullArg[i + 1]); i = switchPos("WINDOW"); if (i) searchWindow = (long)val(g_fullArg[i + 1]); - /*??? Implement SEARCH /WINDOW */ + // ??? Implement SEARCH /WINDOW if (i) print2("Sorry, WINDOW has not been implemented yet.\n"); - let(&str2, g_fullArg[3]); /* Search string */ - let(&str2, edit(str2, 32)); /* Convert to upper case */ + let(&str2, g_fullArg[3]); // Search string + let(&str2, edit(str2, 32)); // Convert to upper case tmpFlag = 0; - /* Search window buffer */ + // Search window buffer pntrLet(&pntrTmp, pntrSpace(searchWindow)); - j = 0; /* Line # */ - m = 0; /* # matches */ + j = 0; // Line # + m = 0; // # matches while (linput(type_fp, NULL, &str1)) { j++; if (j > toLine && toLine != 0) break; if (j >= fromLine || fromLine == 0) { - let(&str3, edit(str1, 32)); /* Convert to upper case */ - if (instr(1, str3, str2)) { /* Match occurred */ + let(&str3, edit(str1, 32)); // Convert to upper case + if (instr(1, str3, str2)) { // Match occurred if (!tmpFlag) { tmpFlag = 1; print2( @@ -6283,7 +6256,7 @@ void command(int argc, char *argv[]) { fclose(type_fp); - /* Deallocate search window buffer */ + // Deallocate search window buffer for (i = 0; i < searchWindow; i++) { let((vstring *)(&pntrTmp[i]), ""); } @@ -6295,19 +6268,19 @@ void command(int argc, char *argv[]) { if (cmdMatches("SET UNIVERSE") || cmdMatches("ADD UNIVERSE") || cmdMatches("DELETE UNIVERSE")) { - /*continue;*/ /* ???Not implemented */ - } /* end if xxx UNIVERSE */ + // continue; // ???Not implemented + } // end if xxx UNIVERSE if (cmdMatches("SET DEBUG FLAG")) { print2("Notice: The DEBUG mode is intended for development use only.\n"); print2("The printout will not be meaningful to the user.\n"); i = (long)val(g_fullArg[3]); - if (i == 4) db4 = 1; /* Not used */ - if (i == 5) db5 = 1; /* mmpars.c statistics; mmunif.c overview */ - if (i == 6) db6 = 1; /* mmunif.c details */ - if (i == 7) db7 = 1; /* mmunif.c more details; mmveri.c */ - if (i == 8) db8 = 1; /* mmpfas.c unification calls */ - if (i == 9) db9 = 1; /* memory */ /* use SET MEMORY_STATUS ON instead */ + if (i == 4) db4 = 1; // Not used + if (i == 5) db5 = 1; // mmpars.c statistics; mmunif.c overview + if (i == 6) db6 = 1; // mmunif.c details + if (i == 7) db7 = 1; // mmunif.c more details; mmveri.c + if (i == 8) db8 = 1; // mmpfas.c unification calls + if (i == 9) db9 = 1; // memory // use SET MEMORY_STATUS ON instead continue; } if (cmdMatches("SET DEBUG OFF")) { @@ -6332,7 +6305,7 @@ void command(int argc, char *argv[]) { g_sourceChanged = 0; } eraseSource(); - g_sourceHasBeenRead = 0; /* Global variable */ + g_sourceHasBeenRead = 0; // Global variable g_showStatement = 0; g_proveStatement = 0; print2("Metamath has been reset to the starting state.\n"); @@ -6341,9 +6314,9 @@ void command(int argc, char *argv[]) { if (cmdMatches("VERIFY PROOF")) { if (switchPos("SYNTAX_ONLY")) { - verifyProofs(g_fullArg[2],0); /* Parse only */ + verifyProofs(g_fullArg[2],0); // Parse only } else { - verifyProofs(g_fullArg[2],1); /* Parse and verify */ + verifyProofs(g_fullArg[2],1); // Parse and verify } continue; } @@ -6356,12 +6329,12 @@ void command(int argc, char *argv[]) { m = switchPos("MATHBOX_SKIP") == 0; n = switchPos("VERBOSE") != 0; verifyMarkup(g_fullArg[2], - (flag)i, /* 1 = check date consistency */ - (flag)j, /* 1 = check top date */ - (flag)k, /* 1 = check external files (gifs and bib) */ - (flag)l, /* 1 = check labels for underscores */ - (flag)m, /* 1 = check mathbox cross-references */ - (flag)n); /* 1 = verbose mode */ + (flag)i, // 1 = check date consistency + (flag)j, // 1 = check top date + (flag)k, // 1 = check external files (gifs and bib) + (flag)l, // 1 = check labels for underscores + (flag)m, // 1 = check mathbox cross-references + (flag)n); // 1 = verbose mode continue; } @@ -6378,10 +6351,10 @@ void command(int argc, char *argv[]) { + ((switchPos("NUMBER_AFTER_LABEL") != 0) ? ADD_COLORED_LABEL_NUMBER : 0) + ((switchPos("BIB_REFS") != 0) ? PROCESS_BIBREFS : 0) + ((switchPos("UNDERSCORES") != 0) ? PROCESS_UNDERSCORES : 0); - processMarkup(g_fullArg[1], /* Input file */ - g_fullArg[2], /* Output file */ + processMarkup(g_fullArg[1], // Input file + g_fullArg[2], // Output file (switchPos("CSS") != 0), - i); /* Action bits */ + i); // Action bits continue; } diff --git a/src/mmunif.c b/src/mmunif.c index 6d0a797d..a6227192 100644 --- a/src/mmunif.c +++ b/src/mmunif.c @@ -21,34 +21,34 @@ // 11[0] is the total number of variables ($1, $2, etc.) in schemeA and schemeB, // i.e. the two schemes being unified. // -// unkVarsLen = ((nmbrString *)((*stateVector)[11]))[0]; +// unkVarsLen = ((nmbrString *)((*stateVector)[11]))[0]; // // 11[1] or stackTop is the number of variables (minus 1) that will require // substitutions in order to perform the unification. Warning: stackTop may be // -1, which could be confused with "end of nmbrString" by some nmbrString // functions. // -// stackTop = ((nmbrString *)((*stateVector)[11]))[1]; +// stackTop = ((nmbrString *)((*stateVector)[11]))[1]; // // 11[2] is the number of variables in schemeA, used by oneDirUnif() (only). // -// schemeAUnkVarsLen = ((nmbrString *)((*stateVector)[11]))[2]; +// schemeAUnkVarsLen = ((nmbrString *)((*stateVector)[11]))[2]; // // 11[3] is the number of entries in the "Henty filter", used by unifyH() (only). // -// g_hentyFilterSize = ((nmbrString *)((*stateVector)[11]))[3]; +// g_hentyFilterSize = ((nmbrString *)((*stateVector)[11]))[3]; // // Entry 8 is the result of unifying schemeA and schemeB, which are the two // schemes being unified. // -// unifiedScheme = (nmbrString *)((*stateVector)[8]); +// unifiedScheme = (nmbrString *)((*stateVector)[8]); // // Entries 0 through 3 each have length unkVarsLen. Entry 1 is a list of token // numbers for the temporary variables substituted in the unification. // // Entry 0 has all variables ($1, $2, etc.) in schemeA and schemeB. // -// unkVars = (nmbrString *)((*stateVector)[0]); +// unkVars = (nmbrString *)((*stateVector)[0]); // // In entries 1 through 3, only variables 0 through stackTop (inclusive) have // meaning. These entries, along with unifiedScheme, determine what variables @@ -59,9 +59,9 @@ // in entry 1. // Entry 3 is the length of the substitution for each variable in entry 1. // -// stackUnkVar = (nmbrString *)((*stateVector)[1]); -// stackUnkVarStart = (nmbrString *)((*stateVector)[2]); -// stackUnkVarLen = (nmbrString *)((*stateVector)[3]); +// stackUnkVar = (nmbrString *)((*stateVector)[1]); +// stackUnkVarStart = (nmbrString *)((*stateVector)[2]); +// stackUnkVarLen = (nmbrString *)((*stateVector)[3]); // // Entries 4 thru 7 each point to unkVarsLen nmbrString's. These entries save the // data needed to resume unification at any point. Entries 4 and 5 are @@ -69,17 +69,17 @@ // Only the first stackTop+1 nmbrString's have meaning. Note that stackTop may be // -1. // -// stackSaveUnkVarStart = (pntrString *)((*stateVector)[4]); -// stackSaveUnkVarLen = (pntrString *)((*stateVector)[5]); -// stackSaveSchemeA = (pntrString *)((*stateVector)[6]); -// stackSaveSchemeB = (pntrString *)((*stateVector)[7]); +// stackSaveUnkVarStart = (pntrString *)((*stateVector)[4]); +// stackSaveUnkVarLen = (pntrString *)((*stateVector)[5]); +// stackSaveSchemeA = (pntrString *)((*stateVector)[6]); +// stackSaveSchemeB = (pntrString *)((*stateVector)[7]); // // Entries 9 and 10 save the contents of 2 and 3 in oneDirUnif (only) // -// nmbrLet((nmbrString **)(&(*stateVector)[9]), -// (nmbrString *)((*stateVector)[2])); -// nmbrLet((nmbrString **)(&(*stateVector)[10]), -// (nmbrString *)((*stateVector)[3])); +// nmbrLet((nmbrString **)(&(*stateVector)[9]), +// (nmbrString *)((*stateVector)[2])); +// nmbrLet((nmbrString **)(&(*stateVector)[10]), +// (nmbrString *)((*stateVector)[3])); // // Entries 12 through 15 hold the "Henty filter", i.e. a list of all "normalized" // unifications so far. Used by unifyH() (only). Each entry 12 through 15 is a @@ -92,10 +92,10 @@ // Entry 15[i] is the unified scheme that resulted from the particular unification. // Note: i = 0 through g_hentyFilterSize-1 below. // -// hentyVars = (nmbrString *)(((pntrString *)((*stateVector)[12]))[i]); -// hentyVarStart = (nmbrString *)(((pntrString *)((*stateVector)[13]))[i]); -// hentyVarLen = (nmbrString *)(((pntrString *)((*stateVector)[14]))[i]); -// hentySubstList = (nmbrString *)(((pntrString *)((*stateVector)[15]))[i]); +// hentyVars = (nmbrString *)(((pntrString *)((*stateVector)[12]))[i]); +// hentyVarStart = (nmbrString *)(((pntrString *)((*stateVector)[13]))[i]); +// hentyVarLen = (nmbrString *)(((pntrString *)((*stateVector)[14]))[i]); +// hentySubstList = (nmbrString *)(((pntrString *)((*stateVector)[15]))[i]); #include "mmvstr.h" #include "mmdata.h" diff --git a/src/mmwtex.c b/src/mmwtex.c index ca1247c9..55f0f423 100644 --- a/src/mmwtex.c +++ b/src/mmwtex.c @@ -860,7 +860,7 @@ long texDefWhiteSpaceLen(char *ptr) // ptr. Comments are considered white space. ptr should point to the first // character of the token. If ptr points to a white space character, 0 // is returned. If ptr points to a null character, 0 is returned. If ptr -// points to a quoted string, the quoted string is returned. A non-alphanumeric\ +// points to a quoted string, the quoted string is returned. A non-alphanumeric // characters ends a token and is a single token. long texDefTokenLen(char *ptr) { @@ -1655,18 +1655,18 @@ void printTexHeader(flag texHeaderFlag) flag printTexComment(vstring commentPtr, flag htmlCenterFlag, long actionBits, // see below // Indicators for actionBits: - // #define ERRORS_ONLY 1 - just report errors, don't print output - // #define PROCESS_SYMBOLS 2 - // #define PROCESS_LABELS 4 - // #define ADD_COLORED_LABEL_NUMBER 8 - // #define PROCESS_BIBREFS 16 - // #define PROCESS_UNDERSCORES 32 - // #define CONVERT_TO_HTML 64 - convert '<' to '>' unless + // #define ERRORS_ONLY 1 - just report errors, don't print output + // #define PROCESS_SYMBOLS 2 + // #define PROCESS_LABELS 4 + // #define ADD_COLORED_LABEL_NUMBER 8 + // #define PROCESS_BIBREFS 16 + // #define PROCESS_UNDERSCORES 32 + // #define CONVERT_TO_HTML 64 - convert '<' to '>' unless // , present - // #define METAMATH_COMMENT 128 - $) terminates string - // #define PROCESS_EVERYTHING PROCESS_SYMBOLS + PROCESS_LABELS \ - // + ADD_COLORED_LABEL_NUMBER + PROCESS_BIBREFS \ - // + PROCESS_UNDERSCORES + CONVERT_HTML + METAMATH_COMMENT \ + // #define METAMATH_COMMENT 128 - $) terminates string + /* #define PROCESS_EVERYTHING PROCESS_SYMBOLS + PROCESS_LABELS \ + + ADD_COLORED_LABEL_NUMBER + PROCESS_BIBREFS \ + + PROCESS_UNDERSCORES + CONVERT_HTML + METAMATH_COMMENT */ // 10-Dec-2018 nm - expanded meaning of errorsOnly for MARKUP command: // 2 = process as if in ... preformatted mode but