/*****************************************************************************/
/* Program name:  metamath                                                   */
/* Copyright (C) 2008 NORMAN MEGILL  nm at alum.mit.edu  http://metamath.org */
/* License terms:  GNU General Public License Version 2 or any later version */
/*****************************************************************************/
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/

#define MVERSION "0.07.38 26-Apr-2008"
/* 0.07.38 26-Apr-2008 nm metamath.c, mmdata.h, mmdata.c, mmvstr.c, mmhlpb.c -
   Enhanced / EXCLUDE 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 <step>" to "IMPROVE <step>" for user convenience and to be consistent
   with "ASSIGN <step>" */
/* 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 */

/* 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
    mmhlpa.c - The help file, part 1.
    mmhlpb.c - The help file, part 2.
    mminou.c - Basic input and output interface
    mmmaci.c - THINK C Macintosh interface (probably obsolete now)
    mmpars.c - Parses the source file
    mmpfas.c - Proof Assistant
    mmunif.c - Unification algorithm for Proof Assistant
    mmutil.c - Miscellaneous I/O utilities for non-ANSI compilers (has become
               obsolete and is now an empty shell)
    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> TAG) (not generally useful)
*/

/*****************************************************************************/
/* ------------- Compilation Instructions ---------------------------------- */
/*****************************************************************************/

/* These are the instructions for the gcc compiler (standard in Linux and
   Cygwin for 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 metamath.c m*.c -o metamath
   3. For better speed and error checking, use these gcc options:
         gcc m*.c -o metamath -O3 -funroll-loops -finline-functions \
             -fomit-frame-pointer -Wall -ansi -pedantic
   4. The Windows version in the download was compiled with LCC-Win32:
         lc -O m*.c -o metamath.exe
*/


/*****************************************************************************/


/*----------------------------------------------------------------------*/


#include <string.h>
#include <stdio.h>
#include <limits.h>
#include <stdlib.h>
#include <ctype.h>
#include <stdarg.h>
#ifdef THINK_C
#include <console.h>
#endif
#include "mmutil.h"
#include "mmvstr.h"
#include "mmdata.h"
#include "mmcmdl.h"
#include "mmcmds.h"
#include "mmhlpa.h"
#include "mmhlpb.h"
#include "mminou.h"
#include "mmpars.h"
#include "mmveri.h"
#include "mmpfas.h"
#include "mmunif.h"
#include "mmword.h"
#include "mmwtex.h"
#ifdef THINK_C
#include "mmmaci.h"
#endif

void command(int argc, char *argv[]);

int qsortStringCmp(const void *p1, const void *p2);
vstring qsortKey; /* Pointer only; do not deallocate */

int main(int argc, char *argv[])
{

/* argc is the number of arguments; argv points to an array containing them */
#ifdef THINK_C
/* Set console attributes */
console_options.pause_atexit = 0; /* No pause at exit */
console_options.title = (unsigned char*)"\pMetamath";
#endif

#ifdef THINK_C
  /* The standard stream triggers the console package to initialize the
     Macintosh Toolbox managers and use the console interface.  cshow must
     be called before using our own window to prevent crashing (THINK C
     Standard Library Reference p. 43). */
  cshow(stdout);
  /* Initialize MacIntosh interface */
  /*ToolBoxInit(); */ /* cshow did this automatically */
  /* Display opening window */
  /*
  WindowInit();
  DrawMyPicture();
  */
  /* Wait for mouse click or key */
  /*while (!Button());*/
#endif


  /****** If 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 TAG 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.) */
  listMode = 0; /* Force Metamath mode as startup */


  toolsMode = listMode;

  if (!listMode) {
    /*print2("Metamath - Version %s\n", MVERSION);*/
    print2("Metamath - Version %s%s", MVERSION, space(27 - strlen(MVERSION)));
  }
  /* if (argc < 2) */ print2("Type HELP for help, EXIT to exit.\n");

  /* Allocate big arrays */
  initBigArrays();

  /* Process a command line until EXIT */
  command(argc, argv);

  /* Close logging command file */
  if (listMode && listFile_fp != NULL) {
    fclose(listFile_fp);
  }

  return 0;

}



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 */

  /* The variables in command() are static so that they won't be destroyed
    by a longjmp return to setjmp. */
  long e, i, j, k, m, l, n, p, q, s /*,tokenNum*/;
  vstring str1 = "", str2 = "", str3 = "", str4 = "", str5= "";
  nmbrString *nmbrTmpPtr; /* Pointer only; not allocated directly */
  nmbrString *nmbrTmp = NULL_NMBRSTRING;
  nmbrString *nmbrSaveProof = NULL_NMBRSTRING;
  /*pntrString *pntrTmpPtr;*/ /* Pointer only; not allocated directly */
  /*pntrString *pntrTmpPtr1;*/ /* Pointer only; not allocated directly */
  /*pntrString *pntrTmpPtr2;*/ /* Pointer only; not allocated directly */
  pntrString *pntrTmp = NULL_PNTRSTRING;
  pntrString *expandedProof = NULL_PNTRSTRING;
  flag tmpFlag;

  /* Variables for SHOW PROOF */
  flag pipFlag; /* Proof-in-progress flag */
  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 */
  flag unknownFlag;
  flag notUnifiedFlag;
  flag reverseFlag;
  long detailStep;
  flag noIndentFlag; /* Flag to use non-indented display */
  long splitColumn; /* Column at which formula starts in nonindented display */
  flag texFlag; /* Flag for TeX */
  flag saveFlag; /* Flag to save in source */
  long indentation; /* Number of spaces to indent proof */
  vstring labelMatch = ""; /* SHOW PROOF <label> argument */

  flag axiomFlag; /* For SHOW TRACE_BACK */
  flag recursiveFlag; /* For SHOW USAGE */
  long fromLine, toLine; /* For TYPE, SEARCH */
  flag joinFlag; /* For SEARCH */
  long searchWindow; /* For SEARCH */
  FILE *type_fp; /* For TYPE, SEARCH */
  long maxEssential; /* For MATCH */
  nmbrString *essentialFlags = NULL_NMBRSTRING;
                                            /* For ASSIGN/IMPROVE FIRST/LAST */
  long offset; /* For ASSIGN/IMPROVE/LET w/ negative step number */

  flag texHeaderFlag; /* For OPEN TEX, CLOSE TEX */
  flag commentOnlyFlag; /* For SHOW STATEMENT */
  flag briefFlag; /* For SHOW STATEMENT */
  flag linearFlag; /* For SHOW LABELS */

  /* toolsMode-specific variables */
  flag commandProcessedFlag = 0; /* Set when the first command line processed;
                                    used to exit shell command line mode */
  FILE *list1_fp;
  FILE *list2_fp;
  FILE *list3_fp;
  vstring list2_fname = "", list2_ftmpname = "";
  vstring list3_ftmpname = "";
  vstring oldstr = "", newstr = "";
  long lines, changedLines, oldChangedLines, twoMatches, p1, p2;
  long firstChangedLine;
  flag cmdMode, changedFlag, outMsgFlag;
  double sum;
  vstring bufferedLine = "";

  /* Initialization to avoid compiler warning (should not be theoretically
     necessary) */
  p = 0;
  q = 0;
  s = 0;
  texHeaderFlag = 0;
  firstChangedLine = 0;

  while (1) {

    if (listMode) {
      /* If called from the OS shell with arguments, do one command
         then exit program. */
      /* (However, let a SUBMIT job complete) */
      if (argc > 1 && commandProcessedFlag && !commandFileOpenFlag) return;
    }

    errorCount = 0; /* Reset error count before each read or proof parse. */

    /* Deallocate stuff that may have been used in previous pass */
    let(&str1,"");
    let(&str2,"");
    let(&str3,"");
    let(&str4,"");
    let(&str5,"");
    nmbrLet(&nmbrTmp, NULL_NMBRSTRING);
    pntrLet(&pntrTmp, NULL_PNTRSTRING);
    nmbrLet(&nmbrSaveProof, NULL_NMBRSTRING);
    nmbrLet(&essentialFlags, NULL_NMBRSTRING);
    j = nmbrLen(rawArgNmbr);
    if (j != rawArgs) bug(1110);
    j = pntrLen(rawArgPntr);
    if (j != rawArgs) bug(1111);
    rawArgs = 0;
    for (i = 0; i < j; i++) let((vstring *)(&rawArgPntr[i]), "");
    pntrLet(&rawArgPntr, NULL_PNTRSTRING);
    nmbrLet(&rawArgNmbr, NULL_NMBRSTRING);
    j = pntrLen(fullArg);
    for (i = 0; i < j; i++) let((vstring *)(&fullArg[i]),"");
    pntrLet(&fullArg,NULL_PNTRSTRING);
    j = pntrLen(expandedProof);
    if (j) {
      for (i = 0; i < j; i++) {
        let((vstring *)(&expandedProof[i]),"");
      }
     pntrLet(&expandedProof,NULL_PNTRSTRING);
    }

    let(&list2_fname, "");
    let(&list2_ftmpname, "");
    let(&list3_ftmpname, "");
    let(&oldstr, "");
    let(&newstr, "");
    let(&labelMatch, "");
    /* (End of space deallocation) */

    midiFlag = 0; /* 8/28/00 Initialize here in case SHOW PROOF exits early */

    if (memoryStatus) {
      /*??? Change to user-friendly message */
#ifdef THINK_C
      print2("Memory:  string %ld xxxString %ld free %ld\n",db,db3,(long)FreeMem());
      getPoolStats(&i, &j, &k);
      print2("Pool:  free alloc %ld  used alloc %ld  used actual %ld\n",i,j,k);
#else
      print2("Memory:  string %ld xxxString %ld\n",db,db3);
#endif
      getPoolStats(&i, &j, &k);
      print2("Pool:  free alloc %ld  used alloc %ld  used actual %ld\n",i,j,k);
    }

    if (!toolsMode) {
      if (PFASmode) {
        let(&commandPrompt,"MM-PA> ");
      } else {
        let(&commandPrompt,"MM> ");
      }
    } else {
      if (listMode) {
        let(&commandPrompt,"Tools> ");
      } else {
        let(&commandPrompt,"TOOLS> ");
      }
    }

    let(&commandLine,""); /* Deallocate previous contents */

    if (!commandProcessedFlag && argc > 1 && argsProcessed < argc - 1
        && !commandFileOpenFlag) {
      /* if (toolsMode) { */  /* 10-Oct-2006 nm Fix bug: changed to listMode */
      if (listMode) {
        /* If program was compiled in TOOLS mode, the command-line argument
           is assumed to be a single TOOLS command; build the equivalent
           TOOLS command */
        for (i = 1; i < argc; i++) {
          argsProcessed++;
          /* Put quotes around an argument with spaces or tabs or quotes
             or empty string */
          if (instr(1, argv[i], " ") || instr(1, argv[i], "\t")
              || instr(1, argv[i], "\"") || instr(1, argv[i], "'")
              || (argv[i])[0] == 0) {
            /* If it contains a double quote, use a single quote */
            if (instr(1, argv[i], "\"")) {
              let(&str1, cat("'", argv[i], "'", NULL));
            } else {
              /* (??? (TODO)Case of both ' and " is not handled) */
              let(&str1, cat("\"", argv[i], "\"", NULL));
            }
          } else {
            let(&str1, argv[i]);
          }
          let(&commandLine, cat(commandLine, (i == 1) ? "" : " ", str1, NULL));
        }
      } else {
        /* If program was compiled in default (Metamath) mode, each command-line
           argument is considered a full Metamath command.  User is responsible
           for ensuring necessary quotes around arguments are passed in. */
        argsProcessed++;
        scrollMode = 0; /* Set continuous scrolling until completed */
        let(&commandLine, cat(commandLine, argv[argsProcessed], NULL));
        if (argc == 2 && instr(1, argv[1], " ") == 0) {
          /* Assume the user intended a READ command.  This special mode allows
             invocation via "metamath xxx.mm". */
          if (instr(1, commandLine, "\"") || instr(1, commandLine, "'")) {
            /* If it already has quotes don't put quotes */
            let(&commandLine, cat("READ ", commandLine, NULL));
          } else {
            /* Put quotes so / won't be interpreted as qualifier separator */
            let(&commandLine, cat("READ \"", commandLine, "\"", NULL));
          }
        }
      }
      print2("%s\n", cat(commandPrompt, commandLine, NULL));
    } else {
      /* Get command from user input or SUBMIT script file */
      commandLine = cmdInput1(commandPrompt);
    }
    if (argsProcessed == argc && !commandProcessedFlag) {
      commandProcessedFlag = 1;
      scrollMode = 1; /* Set prompted (default) scroll mode */
    }
    if (argsProcessed == argc - 1) {
      argsProcessed++; /* Indicates restore scroll mode next time around */
      if (toolsMode) {
        /* If program was compiled in TOOLS mode, we're only going to execute
           one command; set flag to exit next time around */
        commandProcessedFlag = 1;
      }
    }

    /* See if it's an operating system command */
    /* (This is a command line that begins with a quote) */
    if (commandLine[0] == '\'' || commandLine[0] == '\"') {
      /* See if this computer has this feature */
      if (!system(NULL)) {
        print2("?This computer does not accept an operating system command.\n");
        continue;
      } else {
        /* Strip off quote and trailing quote if any */
        let(&str1, right(commandLine, 2));
        if (commandLine[0]) { /* (Prevent stray pointer if empty string) */
          if (commandLine[0] == commandLine[strlen(commandLine) - 1]) {
            let(&str1, left(str1, strlen(str1) - 1));
          }
        }
        /* Do the operating system command */
        system(str1);
#ifdef VAXC
        printf("\n"); /* Last line from VAX doesn't have new line */
#endif
        continue;
      }
    }

    parseCommandLine(commandLine);
    if (rawArgs == 0) continue; /* Empty or comment line */
    if (!processCommandLine()) continue;

    if (commandEcho || (toolsMode && listFile_fp != NULL)) {
      /* Build the complete command and print it for the user */
      k = pntrLen(fullArg);
      let(&str1,"");
      for (i = 0; i < k; i++) {
        if (instr(1, fullArg[i], " ") || instr(1, fullArg[i], "\t")
            || instr(1, fullArg[i], "\"") || instr(1, fullArg[i], "'")
            || ((char *)(fullArg[i]))[0] == 0) {
          /* If the argument has spaces or tabs or quotes
             or is empty string, put quotes around it */
          if (instr(1, fullArg[i], "\"")) {
            let(&str1, cat(str1, "'", fullArg[i], "' ", NULL));
          } else {
            /* (???Case of both ' and " is not handled) */
            let(&str1, cat(str1, "\"", fullArg[i], "\" ", NULL));
          }
        } else {
          let(&str1, cat(str1, fullArg[i], " ", NULL));
        }
      }
      let(&str1, left(str1,strlen(str1) - 1)); /* Trim trailing space */
      /* The tilde is a special flag for printLongLine to print a
         tilde before the carriage return in a split line, not after */
      if (commandEcho) printLongLine(str1, "~", " ");
      if (toolsMode && listFile_fp != NULL) {
        /* Put line in list.tmp as command */
        fprintf(listFile_fp, "%s\n", str1);  /* Print to list command file */
      }

    }

    if (cmdMatches("BEEP") || cmdMatches("B")) {
      /* Print a bell (if user types ahead "B", the bell lets him know when
         his command is finished - useful for long-running commands */
      print2("%c",7);
      continue;
    }

    if (cmdMatches("HELP")) {
      /* Build the complete command */
      k = pntrLen(fullArg);
      let(&str1,"");
      for (i = 0; i < k; i++) {
        let(&str1, cat(str1, fullArg[i], " ", NULL));
      }
      if (toolsMode) {
        help0(left(str1, strlen(str1) - 1));
        help1(left(str1, strlen(str1) - 1));
      } else {
        help1(left(str1, strlen(str1) - 1));
        help2(left(str1, strlen(str1) - 1));
      }
      continue;
    }


    if (cmdMatches("SET SCROLL")) {
      if (cmdMatches("SET SCROLL CONTINUOUS")) {
        scrollMode = 0;
        print2("Continuous scrolling is now in effect.\n");
      } else {
        scrollMode = 1;
        print2("Prompted scrolling is now in effect.\n");
      }
      continue;
    }

    if (cmdMatches("EXIT") || cmdMatches("QUIT")) {
    /*???        || !strcmp(cmd,"^Z")) { */

      if (toolsMode && !listMode) {
        /* Quitting tools command from within Metamath */
        if (!PFASmode) {
          print2(
 "Exiting the Text Tools.  Type EXIT again to exit Metamath.\n");
        } else {
          print2(
 "Exiting the Text Tools.  Type EXIT again to exit the Proof Assistant.\n");
        }
        toolsMode = 0;
        continue;
      }

      if (PFASmode) {

        if (proofChanged) {
          print2(
              "Warning:  You have not saved changes to the proof of \"%s\".\n",
              statement[proveStatement].labelName); /* 21-Jan-06 nm */
          /* 17-Aug-04 nm Added / FORCE qualifier */
          if (switchPos("/ FORCE") == 0) {
            str1 = cmdInput1("Do you want to EXIT anyway (Y, N) <N>? ");
            if (str1[0] != 'y' && str1[0] != 'Y') {
              print2("Use SAVE NEW_PROOF to save the proof.\n");
              continue;
            }
          } else {
            /* User specified / FORCE, so answer question automatically */
            print2("Do you want to EXIT anyway (Y, N) <N>? Y\n");
          }
          proofChanged = 0;
        }

        print2(
 "Exiting the Proof Assistant.  Type EXIT again to exit Metamath.\n");

        /* Deallocate proof structure */
        i = nmbrLen(proofInProgress.proof);
        nmbrLet(&proofInProgress.proof, NULL_NMBRSTRING);
        for (j = 0; j < i; j++) {
          nmbrLet((nmbrString **)(&(proofInProgress.target[j])),
              NULL_NMBRSTRING);
          nmbrLet((nmbrString **)(&(proofInProgress.source[j])),
              NULL_NMBRSTRING);
          nmbrLet((nmbrString **)(&(proofInProgress.user[j])),
              NULL_NMBRSTRING);
        }
        pntrLet(&proofInProgress.target, NULL_PNTRSTRING);
        pntrLet(&proofInProgress.source, NULL_PNTRSTRING);
        pntrLet(&proofInProgress.user, NULL_PNTRSTRING);

        PFASmode = 0;
        continue;
      } else {
        if (sourceChanged) {
          print2("Warning:  You have not saved changes to the source.\n");
          /* 17-Aug-04 nm Added / FORCE qualifier */
          if (switchPos("/ FORCE") == 0) {
            str1 = cmdInput1("Do you want to EXIT anyway (Y, N) <N>? ");
            if (str1[0] != 'y' && str1[0] != 'Y') {
              print2("Use WRITE SOURCE to save the changes.\n");
              continue;
            }
          } else {
            /* User specified / FORCE, so answer question automatically */
            print2("Do you want to EXIT anyway (Y, N) <N>? Y\n");
          }
          sourceChanged = 0;
        }

        if (texFileOpenFlag) {
          print2("The %s file \"%s\" was closed.\n",
              htmlFlag ? "HTML" : "LaTeX", texFileName);
          printTexTrailer(texHeaderFlag);
          fclose(texFilePtr);
          texFileOpenFlag = 0;
        }
        if (logFileOpenFlag) {
          print2("The log file \"%s\" was closed %s %s.\n",logFileName,
              date(),time_());
          fclose(logFilePtr);
          logFileOpenFlag = 0;
        }
        return; /* Exit from program */
      }
    }

    if (cmdMatches("SUBMIT")) {
      if (commandFileOpenFlag) {
        printf("?You may not nest SUBMIT commands.\n");
        continue;
      }
      let(&commandFileName, fullArg[1]);
      commandFilePtr = fSafeOpen(commandFileName, "r");
      if (!commandFilePtr) continue; /* Couldn't open (err msg was provided) */
      commandFileOpenFlag = 1;

      /* 23-Oct-2006 nm Added / SILENT */
      if (switchPos("/ SILENT") == 0) {
        commandFileSilentFlag = 0;
      } else {
        commandFileSilentFlag = 1;
      }
      if (!commandFileSilentFlag)
        print2("Taking command lines from file \"%s\"...\n",commandFileName);

      continue;
    }

    if (toolsMode) {
      /* Start of toolsMode-specific commands */
#define ADD_MODE 1
#define DELETE_MODE 2
#define CLEAN_MODE 3
#define SUBSTITUTE_MODE 4
#define SWAP_MODE 5
#define INSERT_MODE 6
#define BREAK_MODE 7
#define BUILD_MODE 8
#define MATCH_MODE 9
#define RIGHT_MODE 10
      cmdMode = 0;
      if (cmdMatches("ADD")) cmdMode = ADD_MODE;
      else if (cmdMatches("DELETE")) cmdMode = DELETE_MODE;
      else if (cmdMatches("CLEAN")) cmdMode = CLEAN_MODE;
      else if (cmdMatches("SUBSTITUTE") || cmdMatches("S"))
        cmdMode = SUBSTITUTE_MODE;
      else if (cmdMatches("SWAP")) cmdMode = SWAP_MODE;
      else if (cmdMatches("INSERT")) cmdMode = INSERT_MODE;
      else if (cmdMatches("BREAK")) cmdMode = BREAK_MODE;
      else if (cmdMatches("BUILD")) cmdMode = BUILD_MODE;
      else if (cmdMatches("MATCH")) cmdMode = MATCH_MODE;
      else if (cmdMatches("RIGHT")) cmdMode = RIGHT_MODE;
      if (cmdMode) {
        list1_fp = fSafeOpen(fullArg[1], "r");
        if (!list1_fp) continue; /* Couldn't open it (error msg was provided) */
        if (cmdMode == RIGHT_MODE) {
          /* Find the longest line */
          p = 0;
          while (linput(list1_fp, NULL, &str1)) {
            if (p < strlen(str1)) p = strlen(str1);
          }
          rewind(list1_fp);
        }
        let(&list2_fname, fullArg[1]);
        if (list2_fname[strlen(list2_fname) - 2] == '~') {
          let(&list2_fname, left(list2_fname, strlen(list2_fname) - 2));
          print2("The output file will be called %s.\n", list2_fname);
        }
        let(&list2_ftmpname, "");
        list2_ftmpname = fGetTmpName("zz~tools");
        list2_fp = fSafeOpen(list2_ftmpname, "w");
        if (!list2_fp) continue; /* Couldn't open it (error msg was provided) */
        lines = 0;
        changedLines = 0;
        twoMatches = 0;
        changedFlag = 0;
        outMsgFlag = 0;
        switch (cmdMode) {
          case ADD_MODE:
            break;
          case DELETE_MODE:
            break;
          case CLEAN_MODE:
            let(&str4, edit(fullArg[2], 32));
            q = 0;
            if (instr(1, str4, "P") > 0) q = q + 1;
            if (instr(1, str4, "D") > 0) q = q + 2;
            if (instr(1, str4, "G") > 0) q = q + 4;
            if (instr(1, str4, "B") > 0) q = q + 8;
            if (instr(1, str4, "R") > 0) q = q + 16;
            if (instr(1, str4, "C") > 0) q = q + 32;
            if (instr(1, str4, "E") > 0) q = q + 128;
            if (instr(1, str4, "Q") > 0) q = q + 256;
            if (instr(1, str4, "L") > 0) q = q + 512;
            if (instr(1, str4, "T") > 0) q = q + 1024;
            if (instr(1, str4, "U") > 0) q = q + 2048;
            if (instr(1, str4, "V") > 0) q = q + 4096;
            break;
          case SUBSTITUTE_MODE:
            let(&newstr, fullArg[3]); /* The replacement string */
            if (((vstring)(fullArg[4]))[0] == 'A' ||
                ((vstring)(fullArg[4]))[0] == 'a') { /* ALL */
              q = -1;
            } else {
              q = val(fullArg[4]);
              if (q == 0) q = 1;    /* The occurrence # of string to subst */
            }
            s = 0;
            /*
            if (!strcmp(fullArg[2], "\\n")) {
            */
            s = instr(1, fullArg[2], "\\n");
            if (s) {
              /*s = 1;*/ /* Replace lf flag */
              q = 1; /* Only 1st occurrence makes sense in this mode */
            }
            if (!strcmp(fullArg[3], "\\n")) {
              let(&newstr, "\n"); /* Replace with lf */
            }
            break;
          case SWAP_MODE:
            break;
          case INSERT_MODE:
            p = val(fullArg[3]);
            break;
          case BREAK_MODE:
            outMsgFlag = 1;
            break;
          case BUILD_MODE:
            let(&str4, "");
            outMsgFlag = 1;
            break;
          case MATCH_MODE:
            outMsgFlag = 1;
        } /* End switch */
        let(&bufferedLine, "");
        /*
        while (linput(list1_fp, NULL, &str1)) {
        */
        while (1) {
          if (bufferedLine[0]) {
            /* Get input from buffered line (from rejected \n replacement) */
            let(&str1, bufferedLine);
            let(&bufferedLine, "");
          } else {
            if (!linput(list1_fp, NULL, &str1)) break;
          }
          lines++;
          oldChangedLines = changedLines;
          let(&str2, str1);
          switch (cmdMode) {
            case ADD_MODE:
              let(&str2, cat(fullArg[2], str1, fullArg[3], NULL));
              if (strcmp(str1, str2)) changedLines++;
              break;
            case DELETE_MODE:
              p1 = instr(1, str1, fullArg[2]);
              if (strlen(fullArg[2]) == 0) p1 = 1;
              p2 = instr(p1, str1, fullArg[3]);
              if (strlen(fullArg[3]) == 0) p2 = strlen(str1) + 1;
              if (p1 != 0 && p2 != 0) {
                let(&str2, cat(left(str1, p1 - 1), right(str1, p2 + strlen(
                    fullArg[3])), NULL));
                changedLines++;
              }
              break;
            case CLEAN_MODE:
              if (q) {
                let(&str2, edit(str1, q));
                if (strcmp(str1, str2)) changedLines++;
              }
              break;
            case SUBSTITUTE_MODE:
              let(&str2, str1);
              p = 0;
              p1 = 0;

              k = 1;
              /* See if an additional match on line is required */
              if (((vstring)(fullArg[5]))[0] != 0) {
                if (!instr(1, str2, fullArg[5])) {
                  /* No match on line; prevent any substitution */
                  k = 0;
                }
              }

              if (s && k) { /* We're asked to replace a newline char */
                /* Read in the next line */
                /*
                if (linput(list1_fp, NULL, &str4)) {
                  let(&str2, cat(str1, "\\n", str4, NULL));
                */
                if (linput(list1_fp, NULL, &bufferedLine)) {
                  /* Join the next line and see if the string matches */
                  if (instr(1, cat(str1, "\\n", bufferedLine, NULL),
                      fullArg[2])) {
                    let(&str2, cat(str1, "\\n", bufferedLine, NULL));
                    let(&bufferedLine, "");
                  } else {
                    k = 0; /* No match - leave bufferedLine for next pass */
                  }
                } else { /* EOF reached */
                  print2("Warning: file %s has an odd number of lines\n",
                      fullArg[1]);
                }
              }

              while (k) {
                p1 = instr(p1 + 1, str2, fullArg[2]);
                if (!p1) break;
                p++;
                if (p == q || q == -1) {
                  let(&str2, cat(left(str2, p1 - 1), newstr,
                      right(str2, p1 + strlen(fullArg[2])), NULL));
                  if (newstr[0] == '\n') {
                    /* Replacement string is an lf */
                    lines++;
                    changedLines++;
                  }
                  p1 = p1 - strlen(fullArg[2]) + strlen(newstr);
                  if (q != -1) break;
                }
              }
              if (strcmp(str1, str2)) changedLines++;
              break;
            case SWAP_MODE:
              p1 = instr(1, str1, fullArg[2]);
              if (p1) {
                p2 = instr(p1 + 1, str1, fullArg[2]);
                if (p2) twoMatches++;
                let(&str2, cat(right(str1, p1) + strlen(fullArg[2]),
                    fullArg[2], left(str1, p1 - 1), NULL));
                if (strcmp(str1, str2)) changedLines++;
              }
              break;
            case INSERT_MODE:
              if (strlen(str2) < p - 1)
                let(&str2, cat(str2, space(p - 1 - strlen(str2)), NULL));
              let(&str2, cat(left(str2, p - 1), fullArg[2],
                  right(str2, p), NULL));
              if (strcmp(str1, str2)) changedLines++;
              break;
            case BREAK_MODE:
              let(&str2, str1);
              changedLines++;
              for (i = 0; i < strlen(fullArg[2]); i++) {
                p = 0;
                while (1) {
                  p = instr(p + 1, str2, chr(((vstring)(fullArg[2]))[i]));
                  if (!p) break;
                  /* Put spaces arount special one-char tokens */
                  let(&str2, cat(left(str2, p - 1), " ",
                      mid(str2, p, 1),
                      " ", right(str2, p + 1), NULL));
                  p++;
                }
              }
              let(&str2, edit(str2, 8 + 16 + 128)); /* Reduce & trim spaces */
              for (p = strlen(str2) - 1; p >= 0; p--) {
                if (str2[p] == ' ') {
                  str2[p] = '\n';
                  changedLines++;
                }
              }
              if (!str2[0]) changedLines--; /* Don't output blank line */
              break;
            case BUILD_MODE:
              if (str2[0] != 0) { /* Ignore blank lines */
                if (str4[0] == 0) {
                  let(&str4, str2);
                } else {
                  if (strlen(str4) + strlen(str2) > 72) {
                    let(&str4, cat(str4, "\n", str2, NULL));
                    changedLines++;
                  } else {
                    let(&str4, cat(str4, " ", str2, NULL));
                  }
                }
                p = instr(1, str4, "\n");
                if (p) {
                  let(&str2, left(str4, p - 1));
                  let(&str4, right(str4, p + 1));
                } else {
                  let(&str2, "");
                }
              }
              break;
            case MATCH_MODE:
              if (((vstring)(fullArg[2]))[0] == 0) {
                /* Match any non-blank line */
                p = str1[0];
              } else {
                p = instr(1, str1, fullArg[2]);
              }
              if (((vstring)(fullArg[3]))[0] == 'n' ||
                  ((vstring)(fullArg[3]))[0] == 'N') {
                p = !p;
              }
              if (p) changedLines++;
              break;
            case RIGHT_MODE:
              let(&str2, cat(space(p - strlen(str2)), str2, NULL));
              if (strcmp(str1, str2)) changedLines++;
              break;
          } /* End switch(cmdMode) */
          if (lines == 1) let(&str3, left(str2, 79)); /* For msg */
          if (oldChangedLines != changedLines && !changedFlag) {
            changedFlag = 1;
            let(&str3, left(str2, 79)); /* For msg */
            firstChangedLine = lines;
            if ((cmdMode == SUBSTITUTE_MODE && newstr[0] == '\n')
                || cmdMode == BUILD_MODE) /* Joining lines */ {
              firstChangedLine = 1; /* Better message */
            }
          }
          if (((cmdMode != BUILD_MODE && cmdMode != BREAK_MODE)
              || str2[0] != 0)
              && (cmdMode != MATCH_MODE || p))
            fprintf(list2_fp, "%s\n", str2);
        } /* Next input line */
        if (cmdMode == BUILD_MODE) {
          if (str4[0]) {
            /* Output last partial line */
            fprintf(list2_fp, "%s\n", str4);
            changedLines++;
            if (!str3[0]) {
              let(&str3, str4); /* For msg */
            }
          }
        }
        /* Convert any lf's to 1st line in string for readability of msg */
        p = instr(1, str3, "\n");
        if (p) let(&str3, left(str3, p - 1));
        if (!outMsgFlag) {
          if (!changedFlag) {
            if (!lines) {
              print2("The file %s has no lines.\n", fullArg[1]);
            } else {
              print2(
"The file %s has %ld lines; none were changed.  First line:\n",
                list2_fname, lines);
              print2("%s\n", str3);
            }
          } else {
            print2(
"The file %s has %ld lines; %ld were changed.  First changed line is %ld:\n",
                list2_fname, lines, changedLines, firstChangedLine);
            print2("%s\n", str3);
          }
          if (twoMatches) {
            print2(
"Warning:  %ld lines has more than one \"%s\".  The first one was used.\n",
                 twoMatches, fullArg[2]);
          }
        } else {
          if (changedLines == 0) let(&str3, "");
          print2(
"The input had %ld lines, the output has %ld lines.  First output line:\n",
              lines, changedLines);
          print2("%s\n", str3);
        }
        fclose(list1_fp);
        fclose(list2_fp);
        fSafeRename(list2_ftmpname, list2_fname);
        continue;
      } /* end if cmdMode */

#define SORT_MODE 1
#define UNDUPLICATE_MODE 2
#define DUPLICATE_MODE 3
#define UNIQUE_MODE 4
#define REVERSE_MODE 5
      cmdMode = 0;
      if (cmdMatches("SORT")) cmdMode = SORT_MODE;
      else if (cmdMatches("UNDUPLICATE")) cmdMode = UNDUPLICATE_MODE;
      else if (cmdMatches("DUPLICATE")) cmdMode = DUPLICATE_MODE;
      else if (cmdMatches("UNIQUE")) cmdMode = UNIQUE_MODE;
      else if (cmdMatches("REVERSE")) cmdMode = REVERSE_MODE;
      if (cmdMode) {
        list1_fp = fSafeOpen(fullArg[1], "r");
        if (!list1_fp) continue; /* Couldn't open it (error msg was provided) */
        let(&list2_fname, fullArg[1]);
        if (list2_fname[strlen(list2_fname) - 2] == '~') {
          let(&list2_fname, left(list2_fname, strlen(list2_fname) - 2));
          print2("The output file will be called %s.\n", list2_fname);
        }
        let(&list2_ftmpname, "");
        list2_ftmpname = fGetTmpName("zz~tools");
        list2_fp = fSafeOpen(list2_ftmpname, "w");
        if (!list2_fp) continue; /* Couldn't open it (error msg was provided) */

        /* Count the lines */
        lines = 0;
        while (linput(list1_fp, NULL, &str1)) lines++;
        if (cmdMode != SORT_MODE  && cmdMode != REVERSE_MODE) {
          print2("The input file has %ld lines.\n", lines);
        }

        /* Close and reopen the input file */
        fclose(list1_fp);
        list1_fp = fSafeOpen(fullArg[1], "r");
        /* Allocate memory */
        pntrLet(&pntrTmp, pntrSpace(lines));
        /* Assign the lines to string array */
        for (i = 0; i < lines; i++) linput(list1_fp, NULL,
            (vstring *)(&pntrTmp[i]));

        /* Sort */
        if (cmdMode != REVERSE_MODE) {
          if (cmdMode == SORT_MODE) {
            qsortKey = fullArg[2]; /* Do not deallocate! */
          } else {
            qsortKey = "";
          }
          qsort(pntrTmp, lines, sizeof(void *), qsortStringCmp);
        } else { /* Reverse the lines */
          for (i = lines / 2; i < lines; i++) {
            qsortKey = pntrTmp[i]; /* Use qsortKey as handy tmp var here */
            pntrTmp[i] = pntrTmp[lines - 1 - i];
            pntrTmp[lines - 1 - i] = qsortKey;
          }
        }

        /* Output sorted lines */
        changedLines = 0;
        let(&str3, "");
        for (i = 0; i < lines; i++) {
          j = 0; /* Flag that line should be printed */
          switch (cmdMode) {
            case SORT_MODE:
            case REVERSE_MODE:
              j = 1;
              break;
            case UNDUPLICATE_MODE:
              if (i == 0) {
                j = 1;
              } else {
                if (strcmp((vstring)(pntrTmp[i - 1]), (vstring)(pntrTmp[i]))) {
                  j = 1;
                }
              }
              break;
            case DUPLICATE_MODE:
              if (i > 0) {
                if (!strcmp((vstring)(pntrTmp[i - 1]), (vstring)(pntrTmp[i]))) {
                  if (i == lines - 1) {
                    j = 1;
                  } else {
                    if (strcmp((vstring)(pntrTmp[i]),
                        (vstring)(pntrTmp[i + 1]))) {
                      j = 1;
                    }
                  }
                }
              }
              break;
            case UNIQUE_MODE:
              if (i < lines - 1) {
                if (strcmp((vstring)(pntrTmp[i]), (vstring)(pntrTmp[i + 1]))) {
                  if (i == 0) {
                    j = 1;
                  } else {
                    if (strcmp((vstring)(pntrTmp[i - 1]),
                        (vstring)(pntrTmp[i]))) {
                      j = 1;
                    }
                  }
                }
              } else {
                if (i == 0) {
                  j = 1;
                } else {
                  if (strcmp((vstring)(pntrTmp[i - 1]),
                        (vstring)(pntrTmp[i]))) {
                      j = 1;
                  }
                }
              }
              break;
          } /* end switch (cmdMode) */
          if (j) {
            fprintf(list2_fp, "%s\n", (vstring)(pntrTmp[i]));
            changedLines++;
            if (changedLines == 1)
              let(&str3, left((vstring)(pntrTmp[i]), 79));
          }
        } /* next i */
        print2("The output file has %ld lines.  The first line is:\n",
            changedLines);
        print2("%s\n", str3);

        /* Deallocate memory */
        for (i = 0; i < lines; i++) let((vstring *)(&pntrTmp[i]), "");
        pntrLet(&pntrTmp,NULL_PNTRSTRING);

        fclose(list1_fp);
        fclose(list2_fp);
        fSafeRename(list2_ftmpname, list2_fname);
        continue;
      } /* end if cmdMode */

      if (cmdMatches("PARALLEL")) {
        list1_fp = fSafeOpen(fullArg[1], "r");
        list2_fp = fSafeOpen(fullArg[2], "r");
        if (!list1_fp) continue; /* Couldn't open it (error msg was provided) */
        if (!list2_fp) continue; /* Couldn't open it (error msg was provided) */
        let(&list3_ftmpname, "");
        list3_ftmpname = fGetTmpName("zz~tools");
        list3_fp = fSafeOpen(list3_ftmpname, "w");
        if (!list3_fp) continue; /* Couldn't open it (error msg was provided) */

        p1 = 1; p2 = 1; /* not eof */
        p = 0; q = 0; /* lines */
        j = 0; /* 1st line flag */
        let(&str3, "");
        while (1) {
          let(&str1, "");
          if (p1) {
            p1 = (linput(list1_fp, NULL, &str1) != NULL);
            if (p1) p++;
            else let(&str1, "");
          }
          let(&str2, "");
          if (p2) {
            p2 = (linput(list2_fp, NULL, &str2) != NULL);
            if (p2) q++;
            else let(&str2, "");
          }
          if (!p1 && !p2) break;
          let(&str4, cat(str1, fullArg[4], str2, NULL));
          fprintf(list3_fp, "%s\n", str4);
          if (!j) {
            let(&str3, str4); /* Save 1st line for msg */
            j = 1;
          }
        }
        if (p == q) {
          print2(
"The input files each had %ld lines.  The first output line is:\n", p);
        } else {
          print2(
"Warning: file \"%s\" had %ld lines while file \"%s\" had %ld lines.\n",
              fullArg[1], p, fullArg[2], q);
          if (p < q) p = q;
          print2("The output file \"%s\" has %ld lines.  The first line is:\n",
              fullArg[3], p);
        }
        print2("%s\n", str3);

        fclose(list1_fp);
        fclose(list2_fp);
        fclose(list3_fp);
        fSafeRename(list3_ftmpname, fullArg[3]);
        continue;
      }


      if (cmdMatches("NUMBER")) {
        list1_fp = fSafeOpen(fullArg[1], "w");
        if (!list1_fp) continue; /* Couldn't open it (error msg was provided) */
        j = strlen(str(val(fullArg[2])));
        k = strlen(str(val(fullArg[3])));
        if (k > j) j = k;
        for (i = val(fullArg[2]); i <= val(fullArg[3]);
            i = i + val(fullArg[4])) {
          let(&str1, str(i));
          fprintf(list1_fp, "%s\n", str1);
        }
        fclose(list1_fp);
        continue;
      }

      if (cmdMatches("COUNT")) {
        list1_fp = fSafeOpen(fullArg[1], "r");
        if (!list1_fp) continue; /* Couldn't open it (error msg was provided) */
        p1 = 0;
        p2 = 0;
        lines = 0;
        q = 0; /* Longest line length */
        i = 0; /* First longest line */
        j = 0; /* Number of longest lines */
        sum = 0.0; /* Sum of numeric content of lines */
        firstChangedLine = 0;
        while (linput(list1_fp, NULL, &str1)) {
          lines++;

          /* Longest line */
          if (q < strlen(str1)) {
            q = strlen(str1);
            let(&str4, str1);
            i = lines;
            j = 0;
          }

          if (q == strlen(str1)) {
            j++;
          }

          if (instr(1, str1, fullArg[2])) {
            if (!firstChangedLine) {
              firstChangedLine = lines;
              let(&str3, str1);
            }
            p1++;
            p = 0;
            while (1) {
              p = instr(p + 1, str1, fullArg[2]);
              if (!p) break;
              p2++;
            }
          }
          sum = sum + val(str1);
        }
        print2(
"The file has %ld lines.  The string \"%s\" occurs %ld times on %ld lines.\n",
            lines, fullArg[2], p2, p1);
        if (firstChangedLine) {
          print2("The first occurrence is on line %ld:\n", firstChangedLine);
          print2("%s\n", str3);
        }
        print2(
"The first longest line (out of %ld) is line %ld and has %ld characters:\n",
            j, i, q);
        printLongLine(str4, "    "/*startNextLine*/, ""/*breakMatch*/);
            /* breakMatch empty means break line anywhere */  /* 6-Dec-03 */
        print2("If each line were a number, their sum would be %s\n", str(sum));
        fclose(list1_fp);
        continue;
      }

      if (cmdMatches("TYPE") || cmdMatches("T")) {
        list1_fp = fSafeOpen(fullArg[1], "r");
        if (!list1_fp) continue; /* Couldn't open it (error msg was provided) */
        if (rawArgs == 2) {
          n = 10;
        } else {
          if (((vstring)(fullArg[2]))[0] == 'A' ||
              ((vstring)(fullArg[2]))[0] == 'a') { /* ALL */
            n = -1;
          } else {
            n = val(fullArg[2]);
          }
        }
        for (i = 0; i < n || n == -1; i++) {
          if (!linput(list1_fp, NULL, &str1)) break;
          if (!print2("%s\n", str1)) break;
        }
        fclose(list1_fp);
        continue;
      } /* end TYPE */

      if (cmdMatches("TAG")) {
        list1_fp = fSafeOpen(fullArg[1], "r");
        list2_fp = fSafeOpen(fullArg[2], "r");
        if (!list1_fp) continue; /* Couldn't open it (error msg was provided) */
        if (!list2_fp) continue; /* Couldn't open it (error msg was provided) */
        if (!getRevision(fullArg[4])) {
          print2(
"?The revision tag must be of the form /*nn*/ or /*#nn*/.  Please try again.\n");
          continue;
        }
        let(&list3_ftmpname, "");
        list3_ftmpname = fGetTmpName("zz~tools");
        list3_fp = fSafeOpen(list3_ftmpname, "w");
        if (!list3_fp) continue; /* Couldn't open it (error msg was provided) */

        revise(list1_fp, list2_fp, list3_fp, fullArg[4],
            (long)val(fullArg[5]));

        fSafeRename(list3_ftmpname, fullArg[3]);
        continue;
      }

      if (cmdMatches("COPY") || cmdMatches("C")) {
        let(&list2_ftmpname, "");
        list2_ftmpname = fGetTmpName("zz~tools");
        list2_fp = fSafeOpen(list2_ftmpname, "w");
        if (!list2_fp) continue; /* Couldn't open it (error msg was provided) */
        lines = 0;
        let(&str4, cat(fullArg[1], ",", NULL));
        lines = 0;
        j = 0; /* Error flag */
        while (1) {
          if (!str4[0]) break; /* Done scanning list */
          p = instr(1, str4, ",");
          let(&str3, left(str4, p - 1));
          let(&str4, right(str4, p + 1));
          list1_fp = fSafeOpen((str3), "r");
          if (!list1_fp) { /* Couldn't open it (error msg was provided) */
            j = 1; /* Error flag */
            break;
          }
          n = 0;
          while (linput(list1_fp, NULL, &str1)) {
            lines++; n++;
            fprintf(list2_fp, "%s\n", str1);
          }
          if (instr(1, fullArg[1], ",")) { /* More than 1 input file */
            print2("The input file \"%s\" has %ld lines.\n", str3, n);
          }
          fclose(list1_fp);
        }
        if (j) continue; /* One of the input files couldn't be opened */
        fclose(list2_fp);
        print2("The output file \"%s\" has %ld lines.\n", fullArg[2], lines);
        fSafeRename(list2_ftmpname, fullArg[2]);
        continue;
      }

      print2("?This command has not been implemented yet.\n");
      continue;
    } /* End of toolsMode-specific commands */

    if (cmdMatches("TOOLS")) {
      print2(
"Entering the Text Tools utilities.  Type HELP for help, EXIT to exit.\n");
      toolsMode = 1;
      continue;
    }

    if (cmdMatches("READ")) {
      if (statements) {
        printLongLine(cat(
            "?Sorry, reading of more than one source file is not allowed.  ",
            "The file \"", input_fn, "\" has already been READ in.  ",
                                                             /* 11-Dec-05 nm */
            "You may type ERASE to start over.  Note that additional source ",
        "files may be included in the source file with \"$[ <filename> $]\".",
                                                             /* 11-Dec-05 nm */
            NULL),"  "," ");
        continue;
      }
      let(&input_fn, fullArg[1]);
      input_fp = fSafeOpen(input_fn, "r");
      if (!input_fp) continue; /* Couldn't open it (error msg was provided) */

      fclose(input_fp);
      readInput();
      if (switchPos("/ VERIFY")) {
        verifyProofs("*",1); /* Parse and verify */
      } else {
        /* verifyProofs("*",0); */ /* Parse only (for gross error checking) */
      }

      /* 10/21/02 - detect Microsoft bugs reported by several users, when the
         HTML output files are named "con.html" etc. */
      /* If we want a standard error message underlining token, this could go
         in mmpars.c */
      /* From Microsoft's site:
         "The following reserved words cannot be used as the name of a file:
         CON, PRN, AUX, CLOCK$, NUL, COM1, COM2, COM3, COM4, COM5, COM6, COM7,
         COM8, COM9, LPT1, LPT2, LPT3, LPT4, LPT5, LPT6, LPT7, LPT8, and LPT9.
         Also, reserved words followed by an extension - for example,
         NUL.tx7 - are invalid file names." */
      /* Check for labels that will lead to illegal Microsoft file names for
         Windows users.  Don't bother checking CLOCK$ since $ is already
         illegal */
      let(&str1, cat(
         ",CON,PRN,AUX,NUL,COM1,COM2,COM3,COM4,COM5,COM6,COM7,",
         "COM8,COM9,LPT1,LPT2,LPT3,LPT4,LPT5,LPT6,LPT7,LPT8,LPT9,", NULL));
      for (i = 1; i <= statements; i++) {
        let(&str2, cat(",", edit(statement[i].labelName, 32/*uppercase*/), ",",
            NULL));
        if (instr(1, str1, str2) ||
            /* 5-Jan-04 mm*.html is reserved for mmtheorems.html, etc. */
            !strcmp(",MM", left(str2, 3))) {
          print2("\n");
          printLongLine(cat("?Error in statement \"",
              statement[i].labelName, "\" at line ", str(statement[i].lineNum),
              " in file \"", statement[i].fileName,
              "\".  To workaround a Microsoft operating system limitation, the",
              " the following reserved words cannot be used for label names:",
              " CON, PRN, AUX, CLOCK$, NUL, COM1, COM2, COM3, COM4, COM5,",
              " COM6, COM7, COM8, COM9, LPT1, LPT2, LPT3, LPT4, LPT5, LPT6,",
              " LPT7, LPT8, and LPT9.  Also, \"mm*.html\" is reserved for",
              " Metamath file names.  Use another name for this label.", NULL),
              "", " ");
          errorCount++;
        }
      }
      /* 10/21/02 end */

      if (!errorCount) {
        let(&str1, "No errors were found.");
        if (!switchPos("/ VERIFY")) {
            let(&str1, cat(str1,
       "  However, proofs were not checked.  Type VERIFY PROOF *",
       " if you want to check them.",
            NULL));
        }
        printLongLine(str1, "", " ");
      } else {
        print2("\n");
        if (errorCount == 1) {
          print2("One error was found.\n");
        } else {
          print2("%ld errors were found.\n", (long)errorCount);
        }
      }

      continue;
    }

    if (cmdMatches("WRITE SOURCE")) {
      let(&output_fn, fullArg[2]);
      output_fp = fSafeOpen(output_fn, "w");
      if (!output_fp) continue; /* Couldn't open it (error msg was provided)*/

      /* Added 24-Oct-03 nm */
      if (switchPos("/ CLEAN") > 0) {
        cmdMode = 1; /* Clean out any proof-in-progress (that user has flagged
                        with a ? in its date comment field) */
      } else {
        cmdMode = 0; /* Output all proofs (normal) */
      }

      writeInput(cmdMode); /* Added argument 24-Oct-03 nm */
      fclose(output_fp);
      if (cmdMode == 0) sourceChanged = 0; /* Don't unset flag if CLEAN option
                                    since some new proofs may not be saved. */
      continue;
    } /* End of WRITE SOURCE */


    if (cmdMatches("WRITE THEOREM_LIST")) {
      /* 4-Dec-03 - Write out an HTML summary of the theorems to
         mmtheorems.html, mmtheorems2.html,... */
      /* THEOREMS_PER_PAGE is the default number of proof descriptions to output. */
#define THEOREMS_PER_PAGE 100
      /* i is the actual number of proof descriptions to output. */
      /* See if the user overrode the default. */
      i = switchPos("/ THEOREMS_PER_PAGE");
      if (i) {
        i = val(fullArg[i + 1]); /* Use user's value */
      } else {
        i = THEOREMS_PER_PAGE; /* Use the default value */
      }

      if (!texDefsRead) {
        htmlFlag = 1;
        print2("Reading definitions from $t statement of %s...\n", input_fn);
        if (!readTexDefs()) {
          tmpFlag = 1; /* Error flag to recover input file */
          continue; /* An error occurred */
        }
      } else {
        /* Current limitation - can only read def's from .mm file once */
        if (!htmlFlag) {
          print2("?You cannot use both LaTeX and HTML in the same session.\n");
          print2(
              "You must EXIT and restart Metamath to switch to the other.\n");
          continue;
        }
      }
      /* Output the theorem list */
      writeTheoremList(i); /* (located in mmwtex.c) */
      continue;
    }  /* End of "WRITE THEOREM_LIST" */


    if (cmdMatches("WRITE BIBLIOGRAPHY")) {
      /* 10/10/02 -
         This utility builds the bibliographical cross-references to various
         textbooks and updates the user-specified file normally called
         mmbiblio.html.
       */
      tmpFlag = 0; /* Error flag to recover input file */
      list1_fp = fSafeOpen(fullArg[2], "r");
      if (list1_fp == NULL) {
        /* Couldn't open it (error msg was provided)*/
        continue;
      }
      fclose(list1_fp);
      /* This will rename the input mmbiblio.html as mmbiblio.html~1 */
      list2_fp = fSafeOpen(fullArg[2], "w");
      if (list2_fp == NULL) {
          /* Couldn't open it (error msg was provided)*/
        continue;
      }
      /* Note: in older versions the "~1" string was OS-dependent, but we
         don't support VAX or THINK C anymore...  Anyway we reopen it
         here with the renamed file in case the OS won't let us rename
         an opened file during the fSafeOpen for write above. */
      list1_fp = fSafeOpen(cat(fullArg[2], "~1", NULL), "r");
      if (list1_fp == NULL) bug(1116);
      if (!texDefsRead) {
        htmlFlag = 1;
        print2("Reading definitions from $t statement of %s...\n", input_fn);
        if (!readTexDefs()) {
          tmpFlag = 1; /* Error flag to recover input file */
          goto bib_error; /* An error occurred */
        }
      }

      /* Transfer the input file up to the special "<!-- #START# -->" comment */
      while (1) {
        if (!linput(list1_fp, NULL, &str1)) {
          print2(
"?Error: Could not find \"<!-- #START# -->\" line in input file \"%s\".\n",
              fullArg[2]);
          tmpFlag = 1; /* Error flag to recover input file */
          break;
        }
        fprintf(list2_fp, "%s\n", str1);
        if (!strcmp(str1, "<!-- #START# -->")) break;
      }
      if (tmpFlag) goto bib_error;

      p2 = 1; /* Pass 1 or 2 flag */
      lines = 0;
      while (1) {

        if (p2 == 2) {  /* Pass 2 */
          /* Allocate memory for sorting */
          pntrLet(&pntrTmp, pntrSpace(lines));
          lines = 0;
        }

        /* Scan all $a and $p statements */
        for (i = 1; i <= statements; i++) {
          if (statement[i].type != (char)p__ &&
            statement[i].type != (char)a__) continue;
          /* Omit ...OBS (obsolete) and ...NEW (to be implemented) statements */
          if (instr(1, statement[i].labelName, "NEW")) continue;
          if (instr(1, statement[i].labelName, "OBS")) continue;
          let(&str1, "");
          str1 = getDescription(i); /* Get the statement's comment */
          if (!instr(1, str1, "[")) continue;
          for (j = 0; j < strlen(str1); j++) {
            if (str1[j] == '\n') str1[j] = ' '; /* Change newlines to spaces */
            if (str1[j] == '\r') bug(1119);
          }
          let(&str1, edit(str1, 8 + 128 + 16)); /* Reduce & trim whitespace */
          /* Put spaces before page #s (up to 4 digits) for sorting */
          j = 0;
          while (1) {
            j = instr(j + 1, str1, " p. "); /* Heuristic - match " p. " */
            if (!j) break;
            if (j) {
              for (k = j + 4; k <= strlen(str1) + 1; k++) {
                if (!isdigit(str1[k - 1])) {
                  let(&str1, cat(left(str1, j + 2),
                      space(4 - (k - (j + 4))), right(str1, j + 3), NULL));
                  /* Add ### after page number as marker */
                  let(&str1, cat(left(str1, j + 7), "###", right(str1, j + 8),
                      NULL));
                  break;
                }
              }
            }
          }
          /* Process any bibliographic references in comment */
          j = 0;
          n = 0;
          while (1) {
            j = instr(j + 1, str1, "["); /* Find reference (not robust) */
            if (!j) break;
            if (!isalnum(str1[j])) continue; /* Not start of reference */
            n++;
            /* Backtrack from [reference] to a starting keyword */
            m = 0;
            let(&str2, edit(str1, 32)); /* to uppercase */
            for (k = j - 1; k >= 1; k--) {
              /* ??? Future: make this a loop from a list that can be
                 printed in the error message if not found */
              if (0
                  || !strcmp(mid(str2, k, strlen("THEOREM")), "THEOREM")
                  || !strcmp(mid(str2, k, strlen("LEMMA")), "LEMMA")
                  || !strcmp(mid(str2, k, strlen("LEMMAS")), "LEMMAS")
                  || !strcmp(mid(str2, k, strlen("DEFINITION")), "DEFINITION")
                  || !strcmp(mid(str2, k, strlen("COMPARE")), "COMPARE")
                  || !strcmp(mid(str2, k, strlen("PROPOSITION")), "PROPOSITION")
                  || !strcmp(mid(str2, k, strlen("COROLLARY")), "COROLLARY")
                  || !strcmp(mid(str2, k, strlen("AXIOM")), "AXIOM")
                  || !strcmp(mid(str2, k, strlen("RULE")), "RULE")
                  || !strcmp(mid(str2, k, strlen("REMARK")), "REMARK")
                  || !strcmp(mid(str2, k, strlen("EXERCISE")), "EXERCISE")
                  || !strcmp(mid(str2, k, strlen("PROBLEM")), "PROBLEM")
                  || !strcmp(mid(str2, k, strlen("NOTATION")), "NOTATION")
                  || !strcmp(mid(str2, k, strlen("EXAMPLE")), "EXAMPLE")
                  || !strcmp(mid(str2, k, strlen("PROPERTY")), "PROPERTY")
                  || !strcmp(mid(str2, k, strlen("FIGURE")), "FIGURE")
                  || !strcmp(mid(str2, k, strlen("POSTULATE")), "POSTULATE")
                  || !strcmp(mid(str2, k, strlen("EQUATION")), "EQUATION")
                  || !strcmp(mid(str2, k, strlen("SCHEME")), "SCHEME")
                  /* Don't use SCHEMA since we may have THEOREM SCHEMA
                  || !strcmp(mid(str2, k, strlen("SCHEMA")), "SCHEMA")
                  */
                  || !strcmp(mid(str2, k, strlen("CHAPTER")), "CHAPTER")
                  ) {
                m = k;
                break;
              }
              let(&str3, ""); /* Clear tmp alloc stack created by "mid" */
            }
            if (!m) {
              if (p2 == 1) {
                print2("?Warning: No keyword match in \"%s\".\n",
                  statement[i].labelName);
                /* ??? Future - show the actual list */
                print2(
       "?(See metamath.c source for list of keywords THEOREM, LEMMA, etc.)\n");
              }
              continue; /* Not a bib ref - ignore */
            }
            /* m is at the start of a keyword */
            p = instr(m, str1, "["); /* Start of bibliograpy reference */
            q = instr(p, str1, "]"); /* End of bibliography reference */
            if (!q) {
              if (p2 == 1) print2(
                  "?Warning: Reference not found in HTML file in \"%s\".\n",
                  statement[i].labelName);
              continue; /* Not a bib ref - ignore */
            }
            s = instr(q, str1, "###"); /* Page number marker */
            if (!s) {
              if (p2 == 1) print2(
                  "?Warning: No page number after reference in \"%s\".\n",
                  statement[i].labelName);
              continue; /* No page number given - ignore */
            }
            /* Now we have a real reference; increment reference count */
            lines++;
            if (p2 == 1) continue; /* In 1st pass, we just count refs */

            let(&str2, seg(str1, m, p - 1));     /* "Theorem #" */
            let(&str3, seg(str1, p + 1, q - 1));  /* "[bibref]" w/out [] */
            let(&str4, seg(str1, q + 1, s - 1)); /* " p. nnnn" */
            str2[0] = toupper(str2[0]);
            /* Eliminate noise like "of" in "Theorem 1 of [bibref]" */
            for (k = strlen(str2); k >=1; k--) {
              if (0
                  || !strcmp(mid(str2, k, strlen(" of ")), " of ")
                  || !strcmp(mid(str2, k, strlen(" in ")), " in ")
                  || !strcmp(mid(str2, k, strlen(" from ")), " from ")
                  || !strcmp(mid(str2, k, strlen(" on ")), " on ")
                  ) {
                let(&str2, left(str2, k - 1));
                break;
              }
              let(&str2, str2);
            }

            let(&newstr, "");
            newstr = pinkHTML(i); /* Get little pink number */
            let(&oldstr, cat(
                /* Construct the sorting key */
                /* The space() helps Th. 9 sort before Th. 10 on same page */
                str3, " ", str4, space(20 - strlen(str2)), str2,
                "|||",  /* ||| means end of sort key */
                /* Construct just the statement href for combining dup refs */
                "<A HREF=\"", statement[i].labelName,
                ".html\">", statement[i].labelName, "</A>",
                newstr,
                "&&&",  /* &&& means end of statement href */
                /* Construct actual HTML table row (without ending tag
                   so duplicate references can be added) */
                (i < extHtmlStmt) ?
                   "<TR>" :
                   cat("<TR BGCOLOR=", PURPLISH_BIBLIO_COLOR, ">", NULL),
                "<TD NOWRAP>[<A HREF=\"",
                (i < extHtmlStmt) ?
                   htmlBibliography :
                   extHtmlBibliography,
                "#",
                str3,
                "\">", str3, "</A>]", str4,
                "</TD><TD>", str2, "</TD><TD><A HREF=\"",
                statement[i].labelName,
                ".html\">", statement[i].labelName, "</A>",
                newstr, NULL));
            /* Put construction into string array for sorting */
            let((vstring *)(&pntrTmp[lines - 1]), oldstr);
          }
        }
        /* 'lines' should be the same in both passes */
        print2("Pass %ld finished.  %ld references were processed.\n", p2, lines);
        if (p2 == 2) break;
        p2++;    /* Increment from pass 1 to pass 2 */
      }

      /* Sort */
      qsortKey = "";
      qsort(pntrTmp, lines, sizeof(void *), qsortStringCmp);

      /* Combine duplicate references */
      let(&str1, "");  /* Last biblio ref */
      for (i = 0; i < lines; i++) {
        j = instr(1, (vstring)(pntrTmp[i]), "|||");
        let(&str2, left((vstring)(pntrTmp[i]), j - 1));
        if (!strcmp(str1, str2)) {
          n++;
          /* Combine last with this */
          k = instr(j, (vstring)(pntrTmp[i]), "&&&");
          /* Extract statement href */
          let(&str3, seg((vstring)(pntrTmp[i]), j + 3, k -1));
          let((vstring *)(&pntrTmp[i]),
              cat((vstring)(pntrTmp[i - 1]), " &nbsp;", str3, NULL));
          let((vstring *)(&pntrTmp[i - 1]), ""); /* Clear previous line */
        }
        let(&str1, str2);
      }

      /* Write output */
      n = 0;
      for (i = 0; i < lines; i++) {
        j = instr(1, (vstring)(pntrTmp[i]), "&&&");
        if (j) {  /* Don't print blanked out combined lines */
          n++;
          /* Take off prefixes and reduce spaces */
          let(&str1, edit(right((vstring)(pntrTmp[i]), j + 3), 16));
          j = 1;
          /* Break up long lines for text editors */
          let(&printString, "");
          outputToString = 1;
          printLongLine(cat(str1, "</TD></TR>", NULL),
              " ",  /* Start continuation line with space */
              "\""); /* Don't break inside quotes e.g. "Arial Narrow" */
          outputToString = 0;
          fprintf(list2_fp, "%s", printString);
          let(&printString, "");
        }
      }


      /* Discard the input file up to the special "<!-- #END# -->" comment */
      while (1) {
        if (!linput(list1_fp, NULL, &str1)) {
          print2(
"?Error: Could not find \"<!-- #END# -->\" line in input file \"%s\".\n",
              fullArg[2]);
          tmpFlag = 1; /* Error flag to recover input file */
          break;
        }
        if (!strcmp(str1, "<!-- #END# -->")) {
          fprintf(list2_fp, "%s\n", str1);
          break;
        }
      }
      if (tmpFlag) goto bib_error;

      /* 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. */
        if (!strcmp("This page was last updated on ", left(str1, 30))) {
          let(&str1, cat(left(str1, 30), date(), ".", NULL));
        }

        fprintf(list2_fp, "%s\n", str1);
      }

      print2("%ld table rows were written.\n", n);
      /* Deallocate string array */
      for (i = 0; i < lines; i++) let((vstring *)(&pntrTmp[i]), "");
      pntrLet(&pntrTmp,NULL_PNTRSTRING);


     bib_error:
      fclose(list1_fp);
      fclose(list2_fp);
      if (tmpFlag) {
        /* Recover input files in case of error */
        remove(fullArg[2]);  /* Delete output file */
        rename(cat(fullArg[2], "~1", NULL), fullArg[2]);
            /* Restore input file name */
        print2("?The file \"%s\" was not modified.\n", fullArg[2]);
      }
      continue;
    }  /* End of "WRITE BIBLIOGRAPHY" */


    if (cmdMatches("WRITE RECENT_ADDITIONS")) {
      /* 18-Sep-03 -
         This utility creates a list of recent proof descriptions and updates
         the user-specified file normally called mmrecent.html.
       */

      /* RECENT_COUNT is the default number of proof descriptions to output. */
#define RECENT_COUNT 100
      /* i is the actual number of proof descriptions to output. */
      /* See if the user overrode the default. */
      i = switchPos("/ LIMIT");
      if (i) {
        i = val(fullArg[i + 1]); /* Use user's value */
      } else {
        i = RECENT_COUNT; /* Use the default value */
      }

      if (!texDefsRead) {
        htmlFlag = 1;
        print2("Reading definitions from $t statement of %s...\n", input_fn);
        if (!readTexDefs()) {
          tmpFlag = 1; /* Error flag to recover input file */
          continue; /* An error occurred */
        }
      } else {
        /* Current limitation - can only read def's from .mm file once */
        if (!htmlFlag) {
          print2("?You cannot use both LaTeX and HTML in the same session.\n");
          print2(
              "You must EXIT and restart Metamath to switch to the other.\n");
          continue;
        }
      }

      tmpFlag = 0; /* Error flag to recover input file */
      list1_fp = fSafeOpen(fullArg[2], "r");
      if (list1_fp == NULL) {
        /* Couldn't open it (error msg was provided)*/
        continue;
      }
      fclose(list1_fp);
      /* This will rename the input mmrecent.html as mmrecent.html~1 */
      list2_fp = fSafeOpen(fullArg[2], "w");
      if (list2_fp == NULL) {
          /* Couldn't open it (error msg was provided)*/
        continue;
      }
      /* Note: in older versions the "~1" string was OS-dependent, but we
         don't support VAX or THINK C anymore...  Anyway we reopen it
         here with the renamed file in case the OS won't let us rename
         an opened file during the fSafeOpen for write above. */
      list1_fp = fSafeOpen(cat(fullArg[2], "~1", NULL), "r");
      if (list1_fp == NULL) bug(1117);

      /* Transfer the input file up to the special "<!-- #START# -->" comment */
      while (1) {
        if (!linput(list1_fp, NULL, &str1)) {
          print2(
"?Error: Could not find \"<!-- #START# -->\" line in input file \"%s\".\n",
              fullArg[2]);
          tmpFlag = 1; /* Error flag to recover input file */
          break;
        }
        /* 13-May-04 nm Put in "last updated" stamp */
        if (!strcmp(left(str1, 21), "<!-- last updated -->")) {
          let(&str1, cat(left(str1, 21), " <I>Last updated on ", date(),
          /* ??Future: make "EDT"/"EST" or other automatic */
          /*  " at ", time_(), " EST.</I>", NULL)); */
          /* 10-Nov-04 nm Just make it "ET" for "Eastern Time" */
            " at ", time_(), " ET.</I>", NULL));
        }
        fprintf(list2_fp, "%s\n", str1);
        if (!strcmp(str1, "<!-- #START# -->")) break;
      }
      if (tmpFlag) goto wrrecent_error;

      /* Get and parse today's date */
      let(&str1, date());
      j = instr(1, str1, "-");
      k = val(left(str1, j - 1)); /* Day */
#define MONTHS "JanFebMarAprMayJunJulAugSepOctNovDec"
      l = ((instr(1, MONTHS, mid(str1, j + 1, 3)) - 1) / 3) + 1; /* 1 = Jan */
      m = str1[j + 6]; /* Character after 2-digit year */  /* nm 10-Apr-06 */
      if (m == ' ' || m == ']') {                          /* nm 10-Apr-06 */
        /* Handle 2-digit year */
        m = val(mid(str1, j + 5, 2));  /* Year */
#define START_YEAR 93 /* Earliest 19xx year in set.mm database */
        if (m < START_YEAR) {
          m = m + 2000;
        } else {
          m = m + 1900;
        }
      } else {                                            /* nm 10-Apr-06 */
        /* Handle 4-digit year */                         /* nm 10-Apr-06 */
        m = val(mid(str1, j + 5, 4));  /* Year */         /* nm 10-Apr-06 */
      }                                                   /* nm 10-Apr-06 */

      n = 0; /* Count of how many output so far */
      while (n < i /*RECENT_COUNT*/ && m > START_YEAR + 1900 - 1) {
        /* Build date string to match */
        /* Match for 2-digit year */
        let(&str1, cat("$([", str(k), "-", mid(MONTHS, 3 * l - 2, 3), "-",
            right(str(m), 3), "]$)", NULL));
        /* Match for 2-digit year */  /* nm 10-Apr-06 */
        let(&str5, cat("$([", str(k), "-", mid(MONTHS, 3 * l - 2, 3), "-",
            str(m), "]$)", NULL));
        for (s = statements; s >= 1; s--) {

          if (statement[s].type != (char)p__) continue;

          /* Get the comment section after the statement */
          let(&str2, space(statement[s + 1].labelSectionLen));
          memcpy(str2, statement[s + 1].labelSectionPtr,
              statement[s + 1].labelSectionLen);
          p = instr(1, str2, "$)");
          let(&str2, left(str2, p + 1)); /* Get 1st comment (if any) */
          let(&str2, edit(str2, 2)); /* Discard spaces */
          /* See if the date comment matches */
          if (instr(1, str2, str1) || instr(1, str2, str5)) { /* 10-Apr-06 */
            /* We have a match, so increment the match count */
            n++;
            let(&str3, "");
            str3 = getDescription(s);
            let(&str4, "");
            str4 = pinkHTML(s); /* Get little pink number */
            /* Output the description comment */
            /* Break up long lines for text editors with printLongLine */
            let(&printString, "");
            outputToString = 1;
            print2("\n"); /* Blank line for HTML human readability */
            printLongLine(cat(
                  (s < extHtmlStmt) ?
                       "<TR>" :
                       cat("<TR BGCOLOR=", PURPLISH_BIBLIO_COLOR, ">", NULL),
                  "<TD NOWRAP>",  /* IE breaks up the date */
                  /* mid(str1, 4, strlen(str1) - 6), */ /* Date */
                  /* Use 4-digit year */   /* 10-Apr-06 */
                  mid(str5, 4, strlen(str5) - 6), /* Date */  /* 10-Apr-06 */
                  "</TD><TD ALIGN=CENTER><A HREF=\"",
                  statement[s].labelName, ".html\">",
                  statement[s].labelName, "</A>",
                  str4, "</TD><TD ALIGN=LEFT>", NULL),  /* Description */
                              /* 28-Dec-05 nm Added ALIGN=LEFT for IE */
                " ",  /* Start continuation line with space */
                "\""); /* Don't break inside quotes e.g. "Arial Narrow" */

            showStatement = s; /* For printTexComment */
            outputToString = 0; /* For printTexComment */
            texFilePtr = list2_fp;
            /* 18-Sep-03 ???Future - make this just return a string??? */
            printTexComment(str3, 0); /* Sends result to texFilePtr */
            texFilePtr = NULL;
            outputToString = 1; /* Restore after printTexComment */

            /* Get HTML hypotheses => assertion */
            let(&str4, "");
            str4 = getHTMLHypAndAssertion(s); /* In mmwtex.c */
            printLongLine(cat("</TD></TR><TR",
                  (s < extHtmlStmt) ?
                       ">" :
                       cat(" BGCOLOR=", PURPLISH_BIBLIO_COLOR, ">", NULL),
                /*** old
                "<TD BGCOLOR=white>&nbsp;</TD><TD COLSPAN=2 ALIGN=CENTER>",
                str4, "</TD></TR>", NULL),
                ****/
                /* 27-Oct-03 nm */
                "<TD COLSPAN=3 ALIGN=CENTER>",
                str4, "</TD></TR>", NULL),

                " ",  /* Start continuation line with space */
                "\""); /* Don't break inside quotes e.g. "Arial Narrow" */

            outputToString = 0;
            fprintf(list2_fp, "%s", printString);
            let(&printString, "");

            if (n >= i /*RECENT_COUNT*/) break; /* We're done */

            /* 27-Oct-03 nm Put separator row if not last theorem */
            outputToString = 1;
            printLongLine(cat("<TR BGCOLOR=white><TD COLSPAN=3>",
                "<FONT SIZE=-3>&nbsp;</FONT></TD></TR>", NULL),
                " ",  /* Start continuation line with space */
                "\""); /* Don't break inside quotes e.g. "Arial Narrow" */

            /* 29-Jul-04 nm Put the previous, current, and next statement
               labels in HTML comments so a script can use them to update
               web site incrementally */
            /* This section can be deleted without side effects */
            /* Find the previous statement with a web page */
            j = 0;
            for (q = s - 1; q >= 1; q--) {
              if (statement[q].type == (char)p__ ||
                  statement[q].type == (char)a__ ) {
                j = q;
                break;
              }
            }
            if (j) print2("<!-- For script: %s -->\n", statement[j].labelName);
            /* Current statement */
            print2("<!-- For script: %s -->\n", statement[s].labelName);
            /* Find the next statement with a web page */
            j = 0;
            for (q = s + 1; q <= statements; q++) {
              if (statement[q].type == (char)p__ ||
                  statement[q].type == (char)a__ ) {
                j = q;
                break;
              }
            }
            if (j) print2("<!-- For script: %s -->\n", statement[j].labelName);
            /* End of 29-Jul-04 section */

            outputToString = 0;
            fprintf(list2_fp, "%s", printString);
            let(&printString, "");

          }
        } /* Next s - statement number */
        /* Decrement date */
        if (k > 1) {
          k--; /* Decrement day */
        } else {
          k = 31; /* Non-existent day 31's will never match, which is OK */
          if (l > 1) {
            l--; /* Decrement month */
          } else {
            l = 12; /* Dec */
            m --; /* Decrement year */
          }
        }
      } /* next while - Scan next date */


      /* Discard the input file up to the special "<!-- #END# -->" comment */
      while (1) {
        if (!linput(list1_fp, NULL, &str1)) {
          print2(
"?Error: Could not find \"<!-- #END# -->\" line in input file \"%s\".\n",
              fullArg[2]);
          tmpFlag = 1; /* Error flag to recover input file */
          break;
        }
        if (!strcmp(str1, "<!-- #END# -->")) {
          fprintf(list2_fp, "%s\n", str1);
          break;
        }
      }
      if (tmpFlag) goto wrrecent_error;

      /* 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. */
        if (!strcmp("This page was last updated on ", left(str1, 30))) {
          let(&str1, cat(left(str1, 30), date(), ".", NULL));
        }

        fprintf(list2_fp, "%s\n", str1);
      }

      print2("The %ld most recent theorem(s) were written.\n", n);

     wrrecent_error:
      fclose(list1_fp);
      fclose(list2_fp);
      if (tmpFlag) {
        /* Recover input files in case of error */
        remove(fullArg[2]);  /* Delete output file */
        rename(cat(fullArg[2], "~1", NULL), fullArg[2]);
            /* Restore input file name */
        print2("?The file \"%s\" was not modified.\n", fullArg[2]);
      }
      continue;
    }  /* End of "WRITE RECENT_ADDITIONS" */


    if (cmdMatches("SHOW LABELS")) {
        texFlag = 0;
        linearFlag = 0;
        if (switchPos("/ LINEAR")) linearFlag = 1;
        if (switchPos("/ ALL")) {
          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 */
          print2(
"The assertions that match are shown with statement number, label, and type.\n");
        }
        j = 0;
        k = 0;
        for (i = 1; i <= statements; i++) {
          if (!statement[i].labelName[0]) continue; /* No label */
          if (!m && statement[i].type != (char)p__ &&
              statement[i].type != (char)a__) continue; /* No /ALL switch */
          /* 30-Jan-06 nm Added single-character-match wildcard argument */
          if (!matches(statement[i].labelName, fullArg[2], '*', '?')) continue;
          let(&str1,cat(str(i)," ",
              statement[i].labelName," $",chr(statement[i].type)," ",NULL));
#define COL 19 /* Characters per column */
          if (j + strlen(str1) > MAX_LEN
              || (linearFlag && j != 0)) { /* j != 0 to suppress 1st CR */
            print2("\n");
            j = 0;
            k = 0;
          }
          if (strlen(str1) > COL || linearFlag) {
            j = j + strlen(str1);
            k = k + strlen(str1) - COL;
            print2(str1);
          } else {
            if (k == 0) {
              j = j + COL;
              print2("%s%s",str1,space(COL - strlen(str1)));
            } else {
              k = k - (COL - strlen(str1));
              if (k > 0) {
                print2(str1);
                j = j + strlen(str1);
              } else {
                print2("%s%s",str1,space(COL - strlen(str1)));
                j = j + COL;
                k = 0;
              }
            }
          }
        }
        print2("\n");
        continue;
    }

    if (cmdMatches("SHOW SOURCE")) {
      for (i = 1; i <= statements; i++) {
        if (!strcmp(fullArg[2],statement[i].labelName)) break;
      }
      if (i > statements) {
        printLongLine(cat("?There is no statement with label \"",
            fullArg[2], "\".  ",
            "Use SHOW LABELS for a list of valid labels.", NULL), "", " ");
        showStatement = 0;
        continue;
      }
      showStatement = i;

      let(&str1, "");
      str1 = outputStatement(showStatement);
      let(&str1,edit(str1,128)); /* Trim trailing spaces */
      if (str1[strlen(str1)-1] == '\n') let(&str1, left(str1,
          strlen(str1) - 1));
      printLongLine(str1, "", "");
      let(&str1,""); /* Deallocate vstring */
      continue;
    } /* 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. */

      if (rawArgs != 5) {
        print2("?The HTML qualifiers may not be combined with others.\n");
        continue;
      }

      if (texDefsRead) {
        /* Current limitation - can only read def's from .mm file once */
        if (!htmlFlag) {
          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");
          goto htmlDone;
        } else {
          if ((switchPos("/ ALT_HTML") || switchPos("/ BRIEF_ALT_HTML"))
              == (altHtmlFlag == 0)) {
            print2(
              "?You cannot use both HTML and ALT_HTML in the same session.\n");
            print2(
              "You must EXIT and restart Metamath to switch to the other.\n");
            goto htmlDone;
          }
        }
      }

      if (switchPos("/ BRIEF_HTML") || switchPos("/ BRIEF_ALT_HTML")) {
        if (strcmp(fullArg[2], "*")) {
          print2(
              "?For BRIEF_HTML or BRIEF_ALT_HTML, the label must be \"*\"\n");
          goto htmlDone;
        }
        briefHtmlFlag = 1;
      } else {
        briefHtmlFlag = 0;
      }

      if (switchPos("/ ALT_HTML") || switchPos("/ BRIEF_ALT_HTML")) {
        altHtmlFlag = 1;
      } else {
        altHtmlFlag = 0;
      }

      q = 0;

      /* Special feature:  if the match statement has a "*" in it, we
         will also output mmascii.html, mmtheorems.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) */
      if (instr(1, fullArg[2], "*") || briefHtmlFlag) {
        s = -2; /* -2 is for ASCII table; -1 is for theorems;
                    0 is for definitions */
      } else {
        s = 1;
      }

      for (s = s; s <= statements; s++) {

        if (s > 0 && 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
        */

        if (s > 0) {
          if (!statement[s].labelName[0]) continue; /* No label */
          /* 30-Jan-06 nm Added single-character-match wildcard argument */
          if (!matches(statement[s].labelName, fullArg[2], '*', '?')) continue;
          if (statement[s].type != (char)a__
              && statement[s].type != (char)p__) continue;
        }

        q = 1; /* Flag that at least one matching statement was found */

        if (s > 0) {
          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 showStatement is
             compared to extHtmlStmt in printTexHeader in mmwtex.c */
          showStatement = 1;
        }


        /*** Open the html file ***/
        htmlFlag = 1;
        /* Open the html output file */
        switch (s) {
          case -2:
            let(&texFileName, "mmascii.html");
            break;
          case -1:
            let(&texFileName, "mmtheoremsall.html");
            break;
          case 0:
            let(&texFileName, "mmdefinitions.html");
            break;
          default:
            let(&texFileName, cat(statement[showStatement].labelName, ".html",
                NULL));
        }
        print2("Creating HTML file \"%s\"...\n", texFileName);
        texFilePtr = fSafeOpen(texFileName, "w");
        if (!texFilePtr) goto htmlDone; /* Couldn't open it (err msg was
            provided) */
        texFileOpenFlag = 1;
        printTexHeader((s > 0) ? 1 : 0 /*texHeaderFlag*/);
        if (!texDefsRead) {
          /* 9/6/03 If there was an error reading the $t xx.mm statement,
             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 = statements + 1; /* To force loop to exit */
          goto ABORT_S; /* Go to end of loop where file is closed out */
        }

        if (s <= 0) {
          outputToString = 1;
          if (s == -2) {
            printLongLine(cat("<CENTER><FONT COLOR=", GREEN_TITLE_COLOR,
                "><B>",
                "Symbol to ASCII Correspondence for Text-Only Browsers",
                " (in order of first appearance)",
                "</B></FONT></CENTER><P>", NULL), "", "\"");
          }
          /* 13-Oct-2006 nm todo - </CENTER> still appears - where is it? */
          if (!briefHtmlFlag) print2("<CENTER>\n");
          print2("<TABLE BORDER CELLSPACING=0 BGCOLOR=%s\n",
              MINT_BACKGROUND_COLOR);
          /* For bobby.cast.org approval */
          switch (s) {
            case -2:
              print2("SUMMARY=\"Symbol to ASCII correspondences\">\n");
              break;
            case -1:
              print2("SUMMARY=\"List of theorems\">\n");
              break;
            case 0:
              print2("SUMMARY=\"List of syntax, axioms and definitions\">\n");
              break;
          }
          switch (s) {
            case -2:
              print2("<TR ALIGN=LEFT><TD><B>\n");
              break;
            case -1:
              print2(
         "<CAPTION><B>List of Theorems</B></CAPTION><TR ALIGN=LEFT><TD><B>\n");
              break;
            case 0:
              printLongLine(cat(
/*"<CAPTION><B>List of Syntax (not <FONT COLOR=\"#00CC00\">|-&nbsp;</FONT>), ",*/
                  /* 2/9/02 (in case |- suppressed) */
                  "<CAPTION><B>List of Syntax, ",
                  "Axioms (<FONT COLOR=", GREEN_TITLE_COLOR, ">ax-</FONT>) and",
                  " Definitions (<FONT COLOR=", GREEN_TITLE_COLOR,
                  ">df-</FONT>)", "</B></CAPTION><TR ALIGN=LEFT><TD><B>",
                  NULL), "", "\"");
              break;
          }
          switch (s) {
            case -2:
              print2("Symbol</B></TD><TD><B>ASCII\n");
              break;
            case -1:
              print2(
                  "Ref</B></TD><TD><B>Description\n");
              break;
            case 0:
              printLongLine(cat(
                  "Ref</B></TD><TD><B>",
                "Expression (see link for any distinct variable requirements)",
                NULL), "", "\"");
              break;
          }
          print2("</B></TD></TR>\n");
          m = 0; /* Statement number map */
          let(&str3, ""); /* For storing ASCII token list in s=-2 mode */
          for (i = 1; i <= statements; i++) {
            if (i == extHtmlStmt && s != -2) {
              /* Print a row that identifies the start of the extended
                 database (e.g. Hilbert Space Explorer) */
              printLongLine(cat(
                  "<TR><TD COLSPAN=2 ALIGN=CENTER><A NAME=\"startext\"></A>",
                  "The list of syntax, axioms (ax-) and definitions (df-) for",
                  " the <B><FONT COLOR=", GREEN_TITLE_COLOR, ">",
                  extHtmlTitle,
                  "</FONT></B> starts here</TD></TR>", NULL), "", "\"");
            }
            if (statement[i].type == (char)p__ ||
                statement[i].type == (char)a__ ) m++;
            if ((s == -1 && statement[i].type != (char)p__)
                || (s == 0 && statement[i].type != (char)a__)
                || (s == -2 && statement[i].type != (char)c__
                    && statement[i].type != (char)v__)
                ) 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 */
                for (j = 0; j < statement[i].mathStringLen; j++) {
                  let(&str1, mathToken[(statement[i].mathString)[j]].tokenName);
                  /* Output each token only once in case of multiple decl. */
                  if (!instr(1, str3, cat(" ", str1, " ", NULL))) {
                    let(&str3, cat(str3, " ", str1, " ", NULL));
                    let(&str2, "");
                    str2 = tokenToTex(mathToken[(statement[i].mathString)[j]
                        ].tokenName);
                    /* 2/9/02  Skip any tokens (such as |-) that may be suppressed */
                    if (!str2[0]) continue;
                    /* Convert special characters to HTML entities */
                    for (k = 0; k < strlen(str1); k++) {
                      if (str1[k] == '&') {
                        let(&str1, cat(left(str1, k), "&amp;",
                            right(str1, k + 2), NULL));
                        k = k + 4;
                      }
                      if (str1[k] == '<') {
                        let(&str1, cat(left(str1, k), "&lt;",
                            right(str1, k + 2), NULL));
                        k = k + 3;
                      }
                      if (str1[k] == '>') {
                        let(&str1, cat(left(str1, k), "&gt;",
                            right(str1, k + 2), NULL));
                        k = k + 3;
                      }
                    } /* next k */
                    printLongLine(cat("<TR ALIGN=LEFT><TD>",
                        str2,
                        "</TD><TD><TT>",
                        str1,
                        "</TT></TD></TR>", NULL), "", "\"");
                  }
                } /* next j */
                /* Close out the string now to prevent memory overflow */
                fprintf(texFilePtr, "%s", printString);
                let(&printString, "");
                break;
              case -1: /* Falls through to next case */
              case 0:
                /* Count the number of essential hypotheses k */
                /* Not needed anymore??? since getHTMLHypAndAssertion() */
                /*
                k = 0;
                j = nmbrLen(statement[i].reqHypList);
                for (n = 0; n < j; n++) {
                  if (statement[statement[i].reqHypList[n]].type
                      == (char)e__) {
                    k++;
                  }
                }
                */
                let(&str1, "");
                if (s == 0 || briefHtmlFlag) {
                  let(&str1, "");
                  /* 18-Sep-03 Get HTML hypotheses => assertion */
                  str1 = getHTMLHypAndAssertion(i); /* In mmwtex.c */
                  let(&str1, cat(str1, "</TD></TR>", NULL));
                }

                /* 13-Oct-2006 nm Made some changes to BRIEF_HTML/_ALT_HTML
                   to use its mmtheoremsall.html output for the Palm PDA */
                if (briefHtmlFlag) {
                  /* Get page number in mmtheorems*.html of WRITE THEOREMS */
                  k = ((statement[i].pinkNumber - 1) /
                      THEOREMS_PER_PAGE) + 1; /* Page # */
                  let(&str2, cat("<TR ALIGN=LEFT><TD ALIGN=LEFT>",
                      /*"<FONT COLOR=\"#FA8072\">",*/
                      "<FONT COLOR=ORANGE>",
                      str(statement[i].pinkNumber), "</FONT> ",
                      "<FONT COLOR=GREEN><A HREF=\"",
                      "mmtheorems", (k == 1) ? "" : str(k), ".html#",
                      statement[i].labelName,
                      "\">", statement[i].labelName,
                      "</A></FONT>", NULL));
                  let(&str1, cat(str2, " ", str1, NULL));
                } else {
                  /* Get little pink (or rainbow-colored) number */
                  let(&str4, "");
                  str4 = pinkHTML(i);
                  let(&str2, cat("<TR ALIGN=LEFT><TD><A HREF=\"",
                      statement[i].labelName,
                      ".html\">", statement[i].labelName,
                      "</A>", str4, NULL));
                  let(&str1, cat(str2, "</TD><TD>", str1, NULL));
                }
                /* End of 13-Oct-2006 changed section */

                print2("\n");  /* New line for HTML source readability */
                printLongLine(str1, "", "\"");

                if (s == 0 || briefHtmlFlag) {
                              /* Set s == 0 here for Web site version,
                                 s == s for symbol version of theorem list */
                  /* The below has been replaced by getHTMLHypAndAssertion(i)
                     above. */
                  /*printTexLongMath(statement[i].mathString, "", "", 0, 0);*/
                  /*outputToString = 1;*/ /* Is reset by printTexLongMath */
                } else {
                  /* Theorems are listed w/ description; otherwise file is too
                     big for convenience */
                  let(&str1, "");
                  str1 = getDescription(i);
                  if (strlen(str1) > 29)
                    let(&str1, cat(left(str1, 26), "...", NULL));
                  let(&str1, cat(str1, "</TD></TR>", NULL));
                  printLongLine(str1, "", "\"");
                }
                /* Close out the string now to prevent overflow */
                fprintf(texFilePtr, "%s", printString);
                let(&printString, "");
                break;
            } /* end switch */
          } /* next i (statement number) */
          /* print2("</TABLE></CENTER>\n"); */ /* 8/8/03 Removed - already
              done somewhere else, causing validator.w3.org to fail */
          outputToString = 0;  /* closing will write out the string */

        } else { /* s > 0 */

          /*** Output the html statement body ***/
          typeStatement(showStatement,
              0 /*briefFlag*/,
              0 /*commentOnlyFlag*/,
              1 /*texFlag*/,   /* means latex or html */
              1 /*htmlFlag*/);

        } /* if s <= 0 */

       ABORT_S:
        /*** Close the html file ***/
        printTexTrailer(1 /*texHeaderFlag*/);
        fclose(texFilePtr);
        texFileOpenFlag = 0;
        let(&texFileName,"");

      } /* next s */

      if (!q) {
        /* No matching statement was found */
        printLongLine(cat("?There is no statement whose label matches \"",
            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. */
     htmlDone:
      continue;
    } /* if (cmdMatches("SHOW STATEMENT") && switchPos("/ HTML")...) */


    /* If we get here, the user did not specify one of the qualifiers /HTML,
       /BRIEF_HTML, /ALT_HTML, or /BRIEF_ALT_HTML */
    if (cmdMatches("SHOW STATEMENT") && !switchPos("/ HTML")) {

      texFlag = 0;
      /* 27-Jul-05 nm Added SIMPLE_TEX */
      if (switchPos("/ TEX") || switchPos("/ SIMPLE_TEX")
          || switchPos("/ HTML"))
        texFlag = 1;

      briefFlag = 1;
      simpleTexFlag = 0;
      if (switchPos("/ TEX")) briefFlag = 0;
      /* 27-Jul-05 nm Added SIMPLE_TEX */
      if (switchPos("/ SIMPLE_TEX")) briefFlag = 0;
      if (switchPos("/ SIMPLE_TEX")) simpleTexFlag = 1;
      if (switchPos("/ FULL")) briefFlag = 0;

      commentOnlyFlag = 0;
      if (switchPos("/ COMMENT")) {
        commentOnlyFlag = 1;
        briefFlag = 1;
      }


      if (switchPos("/ FULL")) {
        briefFlag = 0;
        commentOnlyFlag = 0;
      }

      if (texFlag) {
        if (!texFileOpenFlag) {
          print2(
      "?You have not opened a %s file.  Use the OPEN TEX command first.\n",
              htmlFlag ? "HTML" : "LaTeX");
          continue;
        }
      }

      if (texFlag && (commentOnlyFlag || briefFlag)) {
        print2("?TEX qualifier should be used alone\n");
        continue;
      }

      q = 0;

      for (s = 1; s <= statements; s++) {
        if (!statement[s].labelName[0]) continue; /* No label */
        /* 30-Jan-06 nm Added single-character-match wildcard argument */
        if (!matches(statement[s].labelName, fullArg[2], '*', '?')) continue;
        if (briefFlag || commentOnlyFlag || texFlag) {
          /* For brief or comment qualifier, if label has wildcards,
             show only $p and $a's */
          /* 30-Jan-06 nm Added single-character-match wildcard argument */
          if (statement[s].type != (char)p__
              && statement[s].type != (char)a__ && (instr(1, fullArg[2], "*")
                  || instr(1, fullArg[2], "?")))
            continue;
        }

        if (q && !texFlag) {
          if (!print2("%s\n", string(79, '-'))) /* Put line between
                                                   statements */
            break; /* Break for speedup if user quit */
        }
        if (texFlag) print2("Outputting statement \"%s\"...\n",
            statement[s].labelName);

        q = 1; /* Flag that at least one matching statement was found */

        showStatement = s;


        typeStatement(showStatement,
            briefFlag,
            commentOnlyFlag,
            texFlag,
            htmlFlag);
      } /* Next s */

      if (!q) {
        /* No matching statement was found */
        printLongLine(cat("?There is no statement whose label matches \"",
            fullArg[2], "\".  ",
            "Use SHOW LABELS for a list of valid labels.", NULL), "", " ");
        continue;
      }

      if (texFlag && !htmlFlag) {
        print2("The LaTeX source was written to \"%s\".\n", texFileName);
        /* 27-Jul-05 nm Added SIMPLE_TEX */
        simpleTexFlag = 0;
      }
      continue;
    } /* (cmdMatches("SHOW STATEMENT") && !switchPos("/ HTML")) */

    if (cmdMatches("SHOW SETTINGS")) {
      print2("Metamath settings on %s at %s:\n",date(),time_());
      if (commandEcho) {
        print2("(SET ECHO...) Command ECHO is ON.\n");
      } else {
        print2("(SET ECHO...) Command ECHO is OFF.\n");
      }
      if (scrollMode) {
        print2("(SET SCROLL...) SCROLLing mode is PROMPTED.\n");
      } else {
        print2("(SET SCROLL...) SCROLLing mode is CONTINUOUS.\n");
      }
      print2("(SET WIDTH...) Screen display WIDTH is %ld.\n", screenWidth);
      print2("(SET HEIGHT...) Screen display HEIGHT is %ld.\n",
          screenHeight + 1);
      if (strlen(input_fn)) {
        print2("(READ...) %ld statements have been read from '%s'.\n",
          statements, input_fn);
      } else {
        print2("(READ...) No source file has been read in yet.\n");
      }
      if (PFASmode) {
        print2("(PROVE...) The statement you are proving is '%s'.\n",
            statement[proveStatement].labelName);
      }
      print2(
    "(SET UNIFICATION_TIMEOUT...) The unification timeout parameter is %ld.\n",
          userMaxUnifTrials);
      print2(
    "(SET SEARCH_LIMIT...) The SEARCH_LIMIT for the IMPROVE command is %ld.\n",
          userMaxProveFloat);
      if (minSubstLen) {
        print2(
     "(SET EMPTY_SUBSTITUTION...) EMPTY_SUBSTITUTION is not allowed (OFF).\n");
      } else {
        print2(
          "(SET EMPTY_SUBSTITUTION...) EMPTY_SUBSTITUTION is allowed (ON).\n");
      }
      if (hentyFilter) { /* 18-Nov-05 nm Added to the SHOW listing */
        print2(
              "(SET JEREMY_HENTY_FILTER...) The Henty filter is turned ON.\n");
      } else {
        print2(
             "(SET JEREMY_HENTY_FILTER...) The Henty filter is turned OFF.\n");
      }
      if (showStatement) {
        print2("(SHOW...) The default statement for SHOW commands is '%s'.\n",
            statement[showStatement].labelName);
      }
      if (logFileOpenFlag) {
        print2("(OPEN LOG...) The log file '%s' is open.\n", logFileName);
      } else {
        print2("(OPEN LOG...) No log file is currently open.\n");
      }
      if (texFileOpenFlag) {
        print2("The %s file '%s' is open.\n", htmlFlag ? "HTML" : "LaTeX",
            texFileName);
      }
      continue;
    }

    if (cmdMatches("SHOW MEMORY")) {
      /*print2("%ld bytes of data memory have been used.\n",db+db3);*/
      j = 32000000; /* The largest we'ed ever look for */
#ifdef THINK_C
      i = FreeMem();
#else
      i = getFreeSpace(j);
#endif
      if (i > j-3) {
        print2("At least %ld bytes of memory are free.\n",j);
      } else {
        print2("%ld bytes of memory are free.\n",i);
      }
      continue;
    }

    if (cmdMatches("SHOW TRACE_BACK")) {
        for (i = 1; i <= statements; i++) {
          if (!strcmp(fullArg[2],statement[i].labelName)) break;
        }
        if (i > statements) {
          printLongLine(cat("?There is no statement with label \"",
              fullArg[2], "\".  ",
              "Use SHOW LABELS for a list of valid labels.", NULL), "", " ");
          showStatement = 0;
          continue;
        }
        showStatement = i;

        essentialFlag = 0;
        axiomFlag = 0;
        endIndent = 0;
        i = switchPos("/ ESSENTIAL");
        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) endIndent = val(fullArg[i + 1]);

        i = switchPos("/ TREE");
        if (i) {
          if (axiomFlag) {
            print2(
                "(Note:  The AXIOMS switch is ignored in TREE mode.)\n");
          }
          if (switchPos("/ COUNT_STEPS")) {
            print2(
                "(Note:  The COUNT_STEPS switch is ignored in TREE mode.)\n");
          }
          traceProofTree(showStatement, essentialFlag, endIndent);
        } else {
          if (endIndent != 0) {
           print2(
"(Note:  The DEPTH is ignored if the TREE switch is not used.)\n");
          }

          i = switchPos("/ COUNT_STEPS");
          if (i) {
            countSteps(showStatement, essentialFlag);
          } else {
            traceProof(showStatement, essentialFlag, axiomFlag);
          }
        }

        continue;

    }


    if (cmdMatches("SHOW USAGE")) {

      /* 7-Jan-2008 nm Added / ALL qualifier */
      if (switchPos("/ ALL")) {
        m = 1;  /* Always include $e, $f statements */
      } else {
        m = 0;  /* If wildcards are used, show $a, $p only */
      }

      showStatement = 0;
      for (i = 1; i <= statements; i++) { /* 7-Jan-2008 */

        /* 7-Jan-2008 nm Added wildcard handling */
        if (!statement[i].labelName[0]) continue; /* No label */
        if (!m && statement[i].type != (char)p__ &&
            statement[i].type != (char)a__ && (instr(1, fullArg[2], "*")
            || instr(1, fullArg[2], "?")))
          continue; /* No /ALL switch and wildcard and not $p, $a */
        /* Wildcard matching */
        if (!matches(statement[i].labelName, fullArg[2], '*', '?')) continue;

        showStatement = i;
        recursiveFlag = 0;
        j = switchPos("/ RECURSIVE");
        if (j) recursiveFlag = 1; /* Recursive (indirect) usage */
        j = switchPos("/ DIRECT");
        if (j) recursiveFlag = 0; /* Direct references only */

        let(&str1, "");
        str1 = traceUsage(showStatement, recursiveFlag);

        /* Count the number of statements = # of spaces */
        k = strlen(str1) - strlen(edit(str1, 2));

        if (!k) {
          printLongLine(cat("Statement \"",
              statement[showStatement].labelName,
              "\" is not referenced in the proof of any statement.", NULL),
              "", " ");
        } else {
          if (recursiveFlag) {
            let(&str2, "\" directly or indirectly affects");
          } else {
            let(&str2, "\" is directly referenced in");
          }
          if (k == 1) {
            printLongLine(cat("Statement \"",
                statement[showStatement].labelName,
                str2, " the proof of ",
                str(k), " statement:", NULL), "", " ");
          } else {
            printLongLine(cat("Statement \"",
                statement[showStatement].labelName,
                str2, " the proofs of ",
                str(k), " statements:", NULL), "", " ");
          }
        }

        if (k) {
          let(&str1, cat(" ", str1, NULL));
        } else {
          let(&str1, "  (None)");
        }

        /* Print the output */
        printLongLine(str1, "  ", " ");
      } /* next i */

      if (showStatement == 0) {
        printLongLine(cat("?There are no labels matching \"",
            fullArg[2], "\".  ",
            "See HELP SHOW USAGE for matching rules.", NULL), "", " ");
      }
      continue;
    } /* cmdMatches("SHOW USAGE") */


    if (cmdMatches("SHOW PROOF")
        || cmdMatches("SHOW NEW_PROOF")
        || cmdMatches("SAVE PROOF")
        || cmdMatches("SAVE NEW_PROOF")
        || cmdMatches("MIDI")) {
      if (switchPos("/ HTML")) {
        print2("?HTML qualifier is obsolete - use SHOW STATEMENT * / HTML\n");
        continue;
      }
      if (cmdMatches("SHOW PROOF") || cmdMatches("SAVE PROOF")) {
        pipFlag = 0;
      } else {
        pipFlag = 1; /* Proof-in-progress (NEW_PROOF) flag */
      }
      if (cmdMatches("SHOW")) {
        saveFlag = 0;
      } else {
        saveFlag = 1; /* The command is SAVE PROOF */
      }

      /* Establish defaults for omitted qualifiers */
      startStep = 0;
      endStep = 0;
      startIndent = 0; /* Not used */
      endIndent = 0;
      /*essentialFlag = 0;*/
      essentialFlag = 1; /* 10/9/99 - friendlier default */
      renumberFlag = 0;
      unknownFlag = 0;
      notUnifiedFlag = 0;
      reverseFlag = 0;
      detailStep = 0;
      noIndentFlag = 0;
      splitColumn = DEFAULT_COLUMN;
      texFlag = 0;

      i = switchPos("/ FROM_STEP");
      if (i) startStep = val(fullArg[i + 1]);
      i = switchPos("/ TO_STEP");
      if (i) endStep = val(fullArg[i + 1]);
      i = switchPos("/ DEPTH");
      if (i) endIndent = val(fullArg[i + 1]);
      /* 10/9/99 - 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")) {
        print2("?You may not specify both / ESSENTIAL and / ALL.\n");
        continue;
      }
      i = switchPos("/ RENUMBER");
      if (i) renumberFlag = 1;
      i = switchPos("/ UNKNOWN");
      if (i) unknownFlag = 1;
      i = switchPos("/ NOT_UNIFIED"); /* pip mode only */
      if (i) notUnifiedFlag = 1;
      i = switchPos("/ REVERSE");
      if (i) reverseFlag = 1;
      i = switchPos("/ LEMMON");
      if (i) noIndentFlag = 1;
      i = switchPos("/ START_COLUMN");
      if (i) splitColumn = val(fullArg[i + 1]);
      i = switchPos("/ TEX") || switchPos("/ HTML");
      if (i) texFlag = 1;


      if (cmdMatches("MIDI")) { /* 8/28/00 */
        midiFlag = 1;
        pipFlag = 0;
        saveFlag = 0;
        let(&labelMatch, fullArg[1]);
        i = switchPos("/ PARAMETER"); /* MIDI only */
        if (i) {
          let(&midiParam, fullArg[i + 1]);
        } else {
          let(&midiParam, "");
        }
      } else {
        midiFlag = 0;
        if (!pipFlag) let(&labelMatch, fullArg[2]);
      }


      if (texFlag) {
        if (!texFileOpenFlag) {
          print2(
     "?You have not opened a %s file.  Use the OPEN %s command first.\n",
              htmlFlag ? "HTML" : "LaTeX",
              htmlFlag ? "HTML" : "TEX");
          continue;
        }
        /**** this is now done after outputting
        print2("The %s source was written to \"%s\".\n",
            htmlFlag ? "HTML" : "LaTeX", texFileName);
        */
      }

      i = switchPos("/ DETAILED_STEP"); /* non-pip mode only */
      if (i) {
        detailStep = val(fullArg[i + 1]);
        if (!detailStep) detailStep = -1; /* To use as flag; error message
                                             will occur in showDetailStep() */
      }

/*??? Need better warnings for switch combinations that don't make sense */

      q = 0;
      for (s = 1; s <= statements; s++) {
        /* 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 (statement[s].type != (char)p__) continue; /* Not $p */
          /* 30-Jan-06 nm Added single-character-match wildcard argument */
          if (!matches(statement[s].labelName, labelMatch, '*', '?')) continue;
          showStatement = s;
        }

        q = 1; /* Flag that at least one matching statement was found */

        if (detailStep) {
          /* Show the details of just one step */
          showDetailStep(showStatement, detailStep);
          continue;
        }

        if (switchPos("/ STATEMENT_SUMMARY")) { /* non-pip mode only */
          /* Just summarize the statements used in the proof */
          proofStmtSumm(showStatement, essentialFlag, texFlag);
          continue;
        }

        if (switchPos("/ PACKED") || switchPos("/ NORMAL") ||
            switchPos("/ COMPRESSED") || saveFlag) {
          /*??? Add error msg if other switches were specified. (Ignore them.)*/

          if (!pipFlag) {
            i = showStatement;
          } else {
            i = proveStatement;
          }

          /* Get the amount to indent the proof by */
          indentation = 2 + getSourceIndentation(i);

          if (!pipFlag) {
            parseProof(showStatement);  /* Prints message if severe error */
            if (wrkProof.errorSeverity > 1) {  /* 21-Aug-04 nm */
                              /* Prevent bugtrap in nmbrSquishProof -> */
                              /* nmbrGetSubProofLen if proof corrupted */
              print2(
          "?The proof has a severe error and cannot be displayed or saved.\n");
              continue;
            }
            /* verifyProof(showStatement); */ /* Not necessary */
            nmbrLet(&nmbrSaveProof, nmbrUnsquishProof(wrkProof.proofString));
          } else {
            nmbrLet(&nmbrSaveProof, proofInProgress.proof);
          }
          if (switchPos("/ PACKED")  || switchPos("/ COMPRESSED")) {
            nmbrLet(&nmbrSaveProof, nmbrSquishProof(nmbrSaveProof));
          }

          if (switchPos("/ COMPRESSED")) {
            let(&str1, compressProof(nmbrSaveProof, i));
          } else {
            let(&str1, nmbrCvtRToVString(nmbrSaveProof));
          }


          if (saveFlag) {
            /* ??? This is a problem when mixing html and save proof */
            if (printString[0]) bug(1114);
            let(&printString, "");
            outputToString = 1; /* Flag for print2 to add to printString */
          } else {
            if (!print2("Proof of \"%s\":\n", statement[i].labelName))
              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")) {
            printLongLine(cat(space(indentation), str1, " $.", NULL),
              space(indentation), "& "); /* "&" is special flag to break
                  compressed part of proof anywhere */
          } else {
            printLongLine(cat(space(indentation), str1, " $.", NULL),
              space(indentation), " ");
          }
          if /*(pipFlag)*/ (1) { /* Add the date proof was created */
            /* 6/13/98 If the proof already has a date stamp, don't add
               a new one.  Note: for the last statement, i + 1
               will refer to a final "dummy" statement containing
               text (comments) through the end of file, stored in its
               labelSectionXxx structure members. */
            let(&str2, space(statement[i + 1].labelSectionLen));
            memcpy(str2, statement[i + 1].labelSectionPtr,
                statement[i + 1].labelSectionLen);
            if (pipFlag && !instr(1, str2, "$([")
                /* 7-Sep-04 Allow both "$([<date>])$" and "$( [<date>] )$" */
                && !instr(1, str2, "$( [")) {
            /* 6/13/98 end */
              /* No date stamp existed before.  Create one for today's
                 date.  Note that the characters after "$." at the end of
                 the proof normally go in the labelSection of the next
                 statement, but a special mode in outputStatement() (in
                 mmpars.c) will output the date stamp characters for a saved
                 proof. */
              /* print2("%s$([%s]$)\n", space(indentation), date()); */
              /* 4/23/04 nm Initialize with a "?" date followed by today's
                 date.  The "?" date can be edited by the user when the
                 proof is becomes "official." */
              /*print2("%s$([?]$) $([%s]$)\n", space(indentation), date());*/
              /* 7-Sep-04 Put space around "[<date>]" */
              print2("%s$( [?] $) $( [%s] $)\n", space(indentation), date());
            } else {
              if (saveFlag && (instr(1, str2, "$([")
                  /* 7-Sep-04 Allow both "$([<date>])$" and "$( [<date>] )$" */
                  || instr(1, str2, "$( ["))) {
                /* An old date stamp existed, and we're saving the proof to
                   the output file.  Make sure the indentation of the old
                   date stamp (which exists in the labelSection of the
                   next statement) matches the indentation of the saved
                   proof.  To do this, we "delete" the indentation spaces
                   on the old date in the labelSection of the next statement,
                   and we put the actual required indentation spaces at
                   the end of the saved proof.  This is done because the
                   labelSectionPtr of the next statement does not point to
                   an isolated string that can be allocated/deallocated but
                   rather to a place in the input source buffer. */
                /* Correct the indentation on old date */
                while ((statement[i + 1].labelSectionPtr)[0] !=
                    '$') {
                  /* "Delete" spaces before old date (by moving source
                     buffer pointer forward), and also "delete"
                     the \n that comes before those spaces */
                  /* If the proof is saved a 2nd time, this loop will
                     not be entered because the pointer will already be
                     at the "$". */
                  (statement[i + 1].labelSectionPtr)++;
                  (statement[i + 1].labelSectionLen)--;
                }
                if (!outputToString) bug(1115);
                /* The final \n will not appear in final output (done in
                   outputStatement() in mmpars.c) because the proofSectionLen
                   below is adjusted to omit it.  This will allow the
                   space(indentation) to appear before the old date without an
                   intervening \n. */
                print2("%s\n", space(indentation));
              }
            }
          }
          if (saveFlag) {
            sourceChanged = 1;
            proofChanged = 0;
            /* ASCII 1 is a flag that string was allocated and not part of
               original source file text buffer */
            let(&printString, cat(chr(1), "\n", printString, NULL));
            if (statement[i].proofSectionPtr[-1] == 1) {
              /* Deallocate old proof if not original source */
              let(&str1, "");
              str1 = statement[i].proofSectionPtr - 1;
              let(&str1, "");
            }
            statement[i].proofSectionPtr = printString + 1;
            /* Subtr 1 char for ASCII 1 at beg, 1 char for "\n" */
            statement[i].proofSectionLen = strlen(printString) - 2;
            printString = "";
            outputToString = 0;
            if (!pipFlag) {
              printLongLine(cat("The proof of \"", statement[i].labelName,
                  "\" has been reformatted and saved internally.",
                  NULL), "", " ");
            } else {
              printLongLine(cat("The new proof of \"", statement[i].labelName,
                  "\" has been saved internally.",
                  NULL), "", " ");
            }
          } else {
            print2(cat(
                "---------The proof of \"",statement[i].labelName,
                "\" to clip out ends above this line.\n",NULL));
          } /* End if saveFlag */
          nmbrLet(&nmbrSaveProof, NULL_NMBRSTRING);
          if (pipFlag) break; /* Only one iteration for NEW_PROOF stuff */
          continue;  /* to next s iteration */
        } /* end if (switchPos("/ PACKED") || switchPos("/ NORMAL") ||
            switchPos("/ COMPRESSED") || saveFlag) */

        if (saveFlag) bug(1112); /* Shouldn't get here */

        if (!pipFlag) {
          i = showStatement;
        } else {
          i = proveStatement;
        }
        if (texFlag) {
          outputToString = 1; /* Flag for print2 to add to printString */
          if (!htmlFlag) {
            print2("\n");
            print2("\\vspace{1ex}\n");
            printLongLine(cat("Proof of ",
                "{\\tt ",
                asciiToTt(statement[i].labelName),
                "}:", NULL), "", " ");
            print2("\n");
            print2("\n");
          } else {
            bug(1118);
            /*???? The code below is obsolete - now down in show statement*/
            /*
            print2("<CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR=%s>\n",
                MINT_BACKGROUND_COLOR);
            print2("<CAPTION><B>Proof of Theorem <FONT\n");
            printLongLine(cat("   COLOR=", GREEN_TITLE_COLOR, ">",
                asciiToTt(statement[i].labelName),
                "</FONT></B></CAPTION>", NULL), "", "\"");
            print2(
                "<TR><TD><B>Step</B></TD><TD><B>Hyp</B></TD><TD><B>Ref</B>\n");
            print2("</TD><TD><B>Expression</B></TD></TR>\n");
            */
          }
          outputToString = 0;
          /* 8/26/99: Obsolete: */
          /* printTexLongMath in typeProof will do this
          fprintf(texFilePtr, "%s", printString);
          let(&printString, "");
          */
          /* 8/26/99: printTeXLongMath now clears printString in LaTeX
             mode before starting its output, so we must put out the
             printString ourselves here */
          fprintf(texFilePtr, "%s", printString);
          let(&printString, ""); /* We'll clr it anyway */
        } else {
          /* Terminal output - display the statement if wildcard is used */
          if (!pipFlag) {
            /* 30-Jan-06 nm Added single-character-match wildcard argument */
            if (instr(1, labelMatch, "*") || instr(1, labelMatch, "?")) {
              if (!print2("Proof of \"%s\":\n", statement[i].labelName))
                break; /* Break for speedup if user quit */
            }
          }
        }


        if (texFlag) print2("Outputting proof of \"%s\"...\n",
            statement[s].labelName);

        typeProof(i,
            pipFlag,
            startStep,
            endStep,
            startIndent, /* Not used */
            endIndent,
            essentialFlag,
            renumberFlag,
            unknownFlag,
            notUnifiedFlag,
            reverseFlag,
            noIndentFlag,
            splitColumn,
            texFlag,
            htmlFlag);
        if (texFlag && htmlFlag) {
          outputToString = 1;
          print2("</TABLE>\n");
          print2("</CENTER>\n");
          /* print trailer will close out string later */
          outputToString = 0;
        }

        /*???CLEAN UP */
        /*nmbrLet(&wrkProof.proofString, nmbrSaveProof);*/

        /*E*/ if (0) { /* for debugging: */
          printLongLine(nmbrCvtRToVString(wrkProof.proofString)," "," ");
          print2("\n");

          nmbrLet(&nmbrSaveProof, nmbrSquishProof(wrkProof.proofString));
          printLongLine(nmbrCvtRToVString(nmbrSaveProof)," "," ");
          print2("\n");

          nmbrLet(&nmbrTmp, nmbrUnsquishProof(nmbrSaveProof));
          printLongLine(nmbrCvtRToVString(nmbrTmp)," "," ");

          nmbrLet(&nmbrTmp, nmbrGetTargetHyp(nmbrSaveProof,showStatement));
          printLongLine(nmbrCvtAnyToVString(nmbrTmp)," "," "); print2("\n");

          nmbrLet(&nmbrTmp, nmbrGetEssential(nmbrSaveProof));
          printLongLine(nmbrCvtAnyToVString(nmbrTmp)," "," "); print2("\n");

          cleanWrkProof(); /* Deallocate verifyProof storage */
        } /* end debugging */

        if (pipFlag) break; /* Only one iteration for NEW_PROOF stuff */
      } /* Next s */
      if (!q) {
        /* No matching statement was found */
        printLongLine(cat("?There is no $p statement whose label matches \"",
            (cmdMatches("MIDI")) ? fullArg[1] : fullArg[2],
            "\".  ",
            "Use SHOW LABELS to see list of valid labels.", NULL), "", " ");
      } else {
        if (saveFlag) {
          print2("Remember to use WRITE SOURCE to save changes permanently.\n");
        }
        if (texFlag) {
          print2("The LaTeX source was written to \"%s\".\n", texFileName);
        }
      }

      continue;
    } /* if (cmdMatches("SHOW PROOF")... */

/*E*/ /*???????? DEBUG command for debugging only */
    if (cmdMatches("DBG")) {
      print2("DEBUGGING MODE IS FOR DEVELOPER'S USE ONLY!\n");
      print2("Argument:  %s\n", fullArg[1]);
      nmbrLet(&nmbrTmp, parseMathTokens(fullArg[1], proveStatement));
      for (j = 0; j < 3; j++) {
        print2("Trying depth %ld\n", j);
        nmbrTmpPtr = proveFloating(nmbrTmp, proveStatement, j, 0, 0);
        if (nmbrLen(nmbrTmpPtr)) break;
      }

      print2("Result:  %s\n", nmbrCvtRToVString(nmbrTmpPtr));
      nmbrLet(&nmbrTmpPtr, NULL_NMBRSTRING);

      continue;
    }
/*E*/ /*???????? DEBUG command for debugging only */

    if (cmdMatches("PROVE")) {
      /*??? Make sure only $p statements are allowed. */
      for (i = 1; i <= statements; i++) {
        if (!strcmp(fullArg[1],statement[i].labelName)) break;
      }
      if (i > statements) {
        printLongLine(cat("?There is no statement with label \"",
            fullArg[1], "\".  ",
            "Use SHOW LABELS for a list of valid labels.", NULL), "", " ");
        proveStatement = 0;
        continue;
      }
      proveStatement = i;
      if (statement[proveStatement].type != (char)p__) {
        printLongLine(cat("?Statement \"", fullArg[1],
            "\" is not a $p statement.", NULL), "", " ");
        proveStatement = 0;
        continue;
      }
      print2(
"Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.\n");

      /* Obsolete:
      print2("You will be working on the proof of statement %s:\n",
          statement[proveStatement].labelName);
      printLongLine(cat("  $p ", nmbrCvtMToVString(
          statement[proveStatement].mathString), NULL), "    ", " ");
      */

      PFASmode = 1; /* Set mode for commands here and in mmcmdl.c */
      /* Note:  Proof Assistant mode can equivalently be determined by:
            nmbrLen(proofInProgress.proof) != 0  */

      parseProof(proveStatement);
      verifyProof(proveStatement); /* Necessary??? */
      if (wrkProof.errorSeverity > 1) {
     print2("The starting proof has a severe error.  It will not be used.\n");
        nmbrLet(&nmbrSaveProof, nmbrAddElement(NULL_NMBRSTRING, -(long)'?'));
      } else {
        nmbrLet(&nmbrSaveProof, wrkProof.proofString);
      }
      cleanWrkProof(); /* Deallocate verifyProof storage */

      /* Right now, only non-packed proofs are handled. */
      nmbrLet(&nmbrSaveProof, nmbrUnsquishProof(nmbrSaveProof));

      /* Assign initial proof structure */
      if (nmbrLen(proofInProgress.proof)) bug(1113); /* Should've been deall.*/
      nmbrLet(&proofInProgress.proof, nmbrSaveProof);
      i = nmbrLen(proofInProgress.proof);
      pntrLet(&proofInProgress.target, pntrNSpace(i));
      pntrLet(&proofInProgress.source, pntrNSpace(i));
      pntrLet(&proofInProgress.user, pntrNSpace(i));
      nmbrLet((nmbrString **)(&(proofInProgress.target[i - 1])),
          statement[proveStatement].mathString);
      pipDummyVars = 0;

      /* Assign known subproofs */
      assignKnownSubProofs();

      /* Initialize remaining steps */
      for (j = 0; j < i/*proof length*/; j++) {
        if (!nmbrLen(proofInProgress.source[j])) {
          initStep(j);
        }
      }

      /* Unify whatever can be unified */
      autoUnify(0); /* 0 means no "congrats" message */

/*
      print2(
"Periodically save your work with SAVE NEW_PROOF and WRITE SOURCE.\n");
      print2(
"There is no UNDO command yet.  You can OPEN LOG to track what you've done.\n");
*/
      /* Show the user the statement to be proved */
      print2("You will be working on statement (from \"S