/*****************************************************************************/
/*        Copyright (C) 2004  NORMAN MEGILL  nm at alum.mit.edu              */
/*            License terms:  GNU General Public License                     */
/*****************************************************************************/
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/

#include <string.h>
#include <stdio.h>
#include <limits.h>
#include <stdlib.h>
#include <ctype.h>
#include <stdarg.h>
#include <setjmp.h>
#include "mmvstr.h"
#include "mmdata.h"
#include "mminou.h"
#include "mmcmdl.h" /* 9/3/99 - for commandPrompt global */

#ifdef __WATCOMC__
  /* Bugs in WATCOMC:
     1. #include <conio.h> has compile errors
     2. Two consecutive calls to vprintf after va_start causes register dump
            or corrupts 2nd arg.
  */
/* From <conio.h>: */
#ifndef _CONIO_H_INCLUDED
extern int cprintf(const char *f__mt,...);
#define _CONIO_H_INCLUDED
#endif
#endif  /* End #ifdef __WATCOMC__ */

#ifdef THINK_C
#include <console.h>
#endif

#define QUOTED_SPACE 3 /*ASCII 3 that temporarily zaps a space */


int errorCount = 0;

/* Global variables used by print2() */
flag logFileOpenFlag = 0;
FILE *logFilePtr;
FILE *listFile_fp = NULL;
/* Global variables used by print2() */
flag outputToString = 0;
vstring printString = "";
/* Global variables used by cmdInput() */
flag commandFileOpenFlag = 0;
FILE *commandFilePtr;
vstring commandFileName = "";

FILE *inputDef_fp,*input_fp,*output_fp; /* File pointers */
vstring inputDef_fn="",input_fn="",output_fn="";        /* File names */

long screenWidth = 79; /* Screen width */
int printedLines = 0; /* Lines printed since last user input (mod scrn hght) */
flag scrollMode = 1; /* Flag for continuous (0) or prompted (1) scroll */
flag quitPrint = 0; /* Flag that user quit the output */
flag localScrollMode = 1; /* 0 = Scroll continuously only till next prompt */

/* Buffer for B (back) command at end-of-page prompt - for future use */
pntrString *backBuffer = NULL_PNTRSTRING;
long backBufferPos = 0;
flag backFromCmdInput = 0; /* User typed "B" at main prompt */

/* Special:  if global flag outputToString = 1, then the output is not
             printed but is added to global string printString */
/* Returns 0 if user typed "q" during scroll prompt; this lets a procedure
   interrupt it's output for speedup (rest of output will be suppressed anyway
   until next command line prompt) */
flag print2(char* fmt,...)
{
  /* This performs the same operations as printf, except that if a log file is
    open, the characters will also be printed to the log file. */
  /* Also, scrolling is paused at each page if in scroll-prompted mode. */
  va_list ap;
  char c;
  long nlpos, lineLen, charsPrinted;
#ifdef THINK_C
  int ii, jj;
#endif
  char printBuffer[PRINTBUFFERSIZE];
  long i;

/*E*/flag savedb9=0;
/*E*/if(db9) savedb9=1; db9=0; /* recursive call to print2 crashes - gcc bug? */
  if (backBufferPos == 0) {
    /* Initialize backBuffer - 1st time in program */
    /* Warning:  Don't call bug(), because it calls print2. */
    if (pntrLen(backBuffer)) printf("*** BUG #1501\n");
    backBufferPos = 1;
    pntrLet(&backBuffer, pntrAddElement(backBuffer));
  }

  if ((!quitPrint && !commandFileOpenFlag && (scrollMode == 1
           && localScrollMode == 1)
      && printedLines >= SCREEN_HEIGHT && !outputToString)
      || backFromCmdInput) {
    /* It requires a scrolling prompt */
    while(1) {
      if (backFromCmdInput && backBufferPos == pntrLen(backBuffer))
        break; /* Exhausted buffer */
      if (backBufferPos < 1 || backBufferPos > pntrLen(backBuffer))
        /* Warning:  Don't call bug(), because it calls print2. */
        printf("*** BUG #1502 %ld\n", backBufferPos);
      if (backBufferPos == 1) {
        printf(
"Press <return> for more, Q <return> to quit, S <return> to scroll to end... "
          );
      } else {
        printf(
"Press <return> for more, Q <ret> quit, S <ret> scroll, B <ret> back up... "
         );
      }
      c = getchar();
      if (c == '\n') {
        if (backBufferPos == pntrLen(backBuffer)) {
          /* Normal output */
          break;
        } else {
          /* Get output from buffer */
          backBufferPos++;
          printf("%s", (vstring)(backBuffer[backBufferPos - 1]));
          continue;
        }
      }
      if (getchar() == '\n') {
        if (c == 'q' || c == 'Q') {
          if (!backFromCmdInput)
            quitPrint = 1;
          break;
        }
        if (c == 's' || c == 'S') {

          if (backBufferPos < pntrLen(backBuffer)) {
            /* Print rest of buffer to screen */
            /*
            for (backBufferPos = backBufferPos + 1; backBufferPos <=
                pntrLen(backBuffer); backBufferPos++) {
            */
            /* 11-Sep-04 Don't use global var as loop var */
            while (backBufferPos + 1 <= pntrLen(backBuffer)) {
              backBufferPos++;
              printf("%s", (vstring)(backBuffer[backBufferPos - 1]));
            }
          }
          if (!backFromCmdInput)
            localScrollMode = 0; /* Continuous scroll */
          break;

        }
        if (backBufferPos > 1) {
          if (c == 'b' || c == 'B') {
            backBufferPos--;
            printf("%s", (vstring)(backBuffer[backBufferPos - 1]));
            continue;
          }
        }

        printf("%c", 7); /* Bell */
        continue;
      }
      while (c != '\n') c = getchar();
    } /* While 1 */
    if (backFromCmdInput)
      goto PRINT2_RETURN;
    printedLines = 0; /* Reset the number of lines printed on the screen */
    if (!quitPrint) {
      backBufferPos++;
      pntrLet(&backBuffer, pntrAddElement(backBuffer));
    }
  }



  if (quitPrint && !outputToString)
    goto PRINT2_RETURN;    /* User typed 'q'
      above or earlier; 8/27/99: don't return if we're outputting to
      a string since we want to complete the writing to the string. */

  va_start(ap, fmt);
  charsPrinted = vsprintf(printBuffer, fmt, ap); /* Put formatted string into
      buffer */
  va_end(ap);

  /* Normally, long proofs are broken up into 80-or-less char lines
     by this point (via printLongLine) so this should never be a problem
     for them.  But in principle a very long line argument to print2
     could be a problem, although currently it should never occur
     (except maybe in long lines in tools? - if so, switch to printLongLine
     there to fix the bug). */
  /* Warning:  Don't call bug(), because it calls print2. */
  if (charsPrinted >= PRINTBUFFERSIZE
      /* || charsPrinted < 0 */
      /* There is a bug on the Sun with gcc version 2.7.2.2 where
         vsprintf returns approx. -268437768, so ignore the bug */
      ) {
    printf("*** BUG 1503\n");
    printf("?PRINTBUFFERSIZE %ld <= charsPrinted %ld in mminou.c\n",
        (long)PRINTBUFFERSIZE, charsPrinted);
    printf("?Memory may now be corrupted.\n");
    printf("?Save your work, exit, and verify output files.\n");
    printf("?You should recompile with increased PRINTBUFFERSIZE.\n");
  }

  nlpos = instr(1, printBuffer, "\n");
  lineLen = strlen(printBuffer);

  /* 10/14/02 Change any ASCII 3's back to spaces, where they were set in
     printLongLine to handle the broken quote problem */
  for (i = 0; i < lineLen; i++) {
    if (printBuffer[i] == QUOTED_SPACE) printBuffer[i] = ' ';
  }

  if ((lineLen > screenWidth + 1) /* && (screenWidth != MAX_LEN) */
         && !outputToString  /* for HTML 7/3/98 */ ) {
    /* Force wrapping of lines that are too long by recursively calling
       print2() via printLongLine().  Note:  "+ 1" above accounts for \n. */
    /* Note that breakMatch is "" so it may break in middle of a word */
    if (!nlpos) {
      /* No end of line */
      printLongLine(left(printBuffer, lineLen), "", "");
    } else {
      printLongLine(left(printBuffer, lineLen - 1), "", "");
    }
    goto PRINT2_RETURN;
  }

  if (!outputToString) {
    if (nlpos == 0) { /* Partial line (usu. status bar) - print immediately */

#ifdef __WATCOMC__
      cprintf("%s", printBuffer); /* Immediate console I/O (printf buffers it)*/
#else
      printf("%s", printBuffer);
#endif

#ifdef THINK_C
      /* Force a console flush to see it (otherwise only CR flushes it) */
      cgetxy(&ii, &jj, stdout);
#endif

#ifdef __STDC__
      /*
      The following change to mminou.c was necessary on my Unix (Linux)
      system to get the `verify proof *' progress bar to display
      progressively (rather than all at once). I've conditionalized it on
      __STDC__, since it should be harmless on any ANSI C system.
        -- Stephen McCamant  smccam @ uclink4.berkeley.edu 12/9/00
      */
      fflush(stdout);
#endif

    } else {
      printf("%s", printBuffer); /* Normal line */
      printedLines++;
      if (!(scrollMode == 1 && localScrollMode == 1)) {
        /* Even in non-scroll (continuous output) mode, still put paged-mode
           lines into backBuffer in case user types a "B" command later,
           so user can page back from end. */
        if (printedLines > SCREEN_HEIGHT) {
          printedLines = 1;
          backBufferPos++;
          pntrLet(&backBuffer, pntrAddElement(backBuffer));
        }
      }
    }
    /* Add line to backBuffer string array */
    /* Warning:  Don't call bug(), because it calls print2. */
    if (backBufferPos < 1) printf("*** PROGRAM BUG #1504\n");
    let((vstring *)(&(backBuffer[backBufferPos - 1])), cat(
        (vstring)(backBuffer[backBufferPos - 1]), printBuffer, NULL));
  } /* End if !outputToString */

  if (logFileOpenFlag && !outputToString) {
    fprintf(logFilePtr, "%s", printBuffer);  /* Print to log file */
  }

  if (listMode && listFile_fp != NULL && !outputToString) {
    /* Put line in list.tmp as comment */
    fprintf(listFile_fp, "! %s", printBuffer);  /* Print to list command file */
  }

  if (outputToString) {
    let(&printString, cat(printString, printBuffer, NULL));
  }

  /* Check for lines too long */
  if (lineLen > screenWidth + 1) { /* The +1 ignores \n */
    /* Warning:  Don't call bug(), because it calls print2. */
    printf("*** PROGRAM BUG #1505\n");
    printf("%ld %s\n", lineLen, printBuffer);
    /*printf(NULL);*/  /* Force crash on VAXC to see where it came from */
  }
  /* \n not allowed in middle of line */
  /* Warning:  Don't call bug(), because it calls print2. */
  if (nlpos != 0 && nlpos != lineLen) printf("*** PROGRAM BUG #1506\n");

 PRINT2_RETURN:
/*E*/if (savedb9) db9=1;
  return (!quitPrint);
}


/* printLongLine automatically puts a newline \n in the output line. */
/* startNextLine is the string to place before continuation lines. */
/* breakMatch is a list of characters at which the line can be broken. */
/* Special:  startNextLine starts with "~" means add tilde after broken line */
/* Special:  breakMatch begins with "&" means compressed proof */
/* Special:  breakMatch empty means break line anywhere */
/* Special:  breakMatch begins with octal 1 means nested tree display (right
             justify continuation lines); 1 is changed to space for
             break matching */
/* Special:  if breakMatch is \, then put % at end of previous line for LaTeX*/
/* Special:  if breakMatch is " (quote), treat as if space but don't break
             quotes, and also let lines grow long - use this call for all HTML
             code */ /* Added 10/14/02 */
void printLongLine(vstring line, vstring startNextLine, vstring breakMatch)
{
  vstring longLine = "";
  vstring multiLine = "";
  vstring prefix = "";
  vstring startNextLine1 = "";
  vstring breakMatch1 = "";
  long i, j, p;
  long startNextLineLen;
  flag firstLine;
  flag tildeFlag = 0;
  flag treeIndentationFlag = 0;

  /* 10/14/02 added for HTML handling */
  flag htmlFlag = 0; /* 1 means printLongLine was called with "\"" as
                        breakMatch argument (for HTML code) */
  flag quoteMode = 0; /* 1 means inside quote */
  char quoteChar = '"'; /* Current quote character */
  long quoteStartPos = 0; /* Start of quote */
  long saveScreenWidth; /* To let screenWidth grow temporarily */

  long saveTempAllocStack;

  /* Blank line (the rest of algorithm would ignore it; output and return) */
  if (!line[0]) {
    /* 10/14/02 Do a dummy let() so caller can always depend on printLongLine
       to empty the tempalloc string stack (for the rest of this code, the
       first let() will do this) */
    let(&longLine, "");
    print2("\n");
    return;
  }

  /* Change the stack allocation start to prevent arguments from being
     deallocated.  We need to do this because more than one argument
     may be passed in with cat(), chr(), etc. and let() can only grab
     one, destroying the others  */
  saveTempAllocStack = startTempAllocStack;
  startTempAllocStack = tempAllocStackTop; /* For let() stack cleanup */
  /* Added 10/14/02 */
  /* Grab the input arguments */
  let(&multiLine, line);
  let(&startNextLine1, startNextLine);
  let(&breakMatch1, breakMatch);
  /* Now relax - back to normal; we can let temporary allocation stack die. */
  startTempAllocStack = saveTempAllocStack;

  /* 10/14/02 */
  /* We must copy input argument breakMatch to a variable string because we
     will be zapping one of its characters, and ordinarily breakMatch is
     passed in as a constant string.  However, this is now done with argument
     grabbing above so we're OK. */

  /* Flag to right justify continuation lines */
  if (breakMatch1[0] == 1) {
    treeIndentationFlag = 1;
    breakMatch1[0] = ' '; /* Change to a space (the real break character) */
  }

  /* HTML mode */   /* Added 10/14/02 */
  /* The HTML mode is intended not to break inside quoted HTML tag
     strings.  All HTML output should be called with this mode.
     Since we don't parse HTML this method is not perfect.  Only double
     quotes are inspected, so all HTML strings with spaces must be
     surrounded by double quotes.  If text quotes surround a tag
     with a quoted string, this code will not work and must be
     enhanced. */
  /* Whenever we are inside of a quote, we change a space to ASCII 3 to
     prevent matching it.  The reverse is done in the print2() function,
     where all ASCII 3's are converted back to space. */
  /* Note added 10/20/02: tidy.exe breaks HREF quotes with new line.
     Check HTML spec - do we really need this code? */
  j = strlen(multiLine);
  /* Do a bug check to make sure no real ASCII 3's are ever printed */
  for (i = 0; i < j; i++) {
    if (multiLine[i] == QUOTED_SPACE) bug(1514); /* Should never be the case */
  }
  if (breakMatch1[0] == '\"') {
    htmlFlag = 1;
    breakMatch1[0] = ' '; /* Change to a space (the real break character) */
    /* Scan string for quoted strings */
    quoteMode = 0;
    for (i = 0; i < j; i++) {

      /* 10/24/02 - This code has problems with SHOW STATEMENT/ALT_HTML
         It is bypassed completely now. */
      if (i == i) break;

      /* Special case: ignore ALT='"' in set.mm */
      if (multiLine[i] == '"' && i >= 5
          && !strncmp("ALT='\"'\"", multiLine + i - 5, 7))
        continue;
      if (!quoteMode) {
        /* If we wanted to handle double and single nested quotes: */
        /* if (multiLine[i] == '\'' || multiLine[i] == '"') { */
        /* But since single quotes are ambiguous with apostrophes, we will
           demand that only double quotes be used around HTML tag strings
           that have spaces such as <FONT FACE="Arial Narrow">. */
        if (multiLine[i] == '"') {
          quoteMode = 1;
          quoteStartPos = i;
          quoteChar = multiLine[i];
        }
      } else {
        if (multiLine[i] == quoteChar) {
          quoteMode = 0;
        }
      }
      if (quoteMode == 1 && multiLine[i] == ' ') {
        /* Zap the space with ASCII 3 */
        multiLine[i] = QUOTED_SPACE;
      }
    }
    /* If we ended in quoteMode, it wasn't a real quote.  Revert the
       space zapping. */
    if (quoteMode == 1) {
      for (i = quoteStartPos; i < j; i++) {
        if (multiLine[i] == QUOTED_SPACE) multiLine[i] = ' ';
      }
    }
    /* As a special case for more safety, we'll zap the ubiquitous
       "Arial Narrow" used for the little pink numbers. */
    i = 0;
    while (1) {
      i = instr(i + 1, multiLine, "Arial Narrow");
      if (i) multiLine[i + 4] = QUOTED_SPACE;
      else break;
    }
  }


  /* The tilde is a special flag for printLongLine to print a
     tilde before the carriage return in a split line, not after */
  if (startNextLine1[0] == '~') {
    tildeFlag = 1;
    let(&startNextLine1, " ");
  }


  while (multiLine[0]) { /* While there are multi caller-inserted newlines */

    /* Process caller-inserted newlines */
    p = instr(1, multiLine, "\n");
    if (p) {
      /* Get the next caller's line */
      let(&longLine, left(multiLine, p - 1));
      /* Postpone the remaining lines to multiLine for next time around */
      let(&multiLine, right(multiLine, p + 1));
    } else {
      let(&longLine, multiLine);
      let(&multiLine, "");
    }

    saveScreenWidth = screenWidth;
   HTML_RESTART:
    /* Now we will break up one caller's line */
    firstLine = 1;

    startNextLineLen = strlen(startNextLine1);
    /* Prevent infinite loop if next line prefix is longer than screen */
    if (startNextLineLen > screenWidth - 4) {
      startNextLineLen = screenWidth - 4;
      let(&startNextLine1, left(startNextLine1, screenWidth - 4));
    }
    while (strlen(longLine) + (1 - firstLine) * startNextLineLen >
        screenWidth - (long)tildeFlag - (long)(breakMatch1[0] == '\\')) {
      p = screenWidth - (long)tildeFlag - (long)(breakMatch1[0] == '\\') + 1;
      if (!firstLine) p = p - startNextLineLen;

      /* Assume compressed proof if 1st char of breakMatch1 is "&" */
      if (breakMatch1[0] == '&'
          && !instr(p, left(longLine, strlen(longLine) - 3), " ")
          && longLine[p - 3] != ' ') /* Don't split trailing "$." */ {
        /* We're in the compressed proof section; break line anywhere */
        p = p;
      } else {
        if (!breakMatch1[0]) {
          p = p; /* Break line anywhere */
        } else {
          if (breakMatch1[0] == '&') {
            /* Compressed proof */
            p = p - 1; /* We will add a trailing space to line for easier
                          label searches by the user during editing */
          }
          if (p <= 0) bug(1518);
          /*while (!instr(1, breakMatch1, mid(longLine,p,1)) && p > 0) {*/
          /* Speedup */
          while (strchr(breakMatch1, longLine[p - 1]) == NULL) {
            p--;
            if (!p) break;
          }
          if (p <= 0 && htmlFlag) {
            /* The line couldn't be broken.  Since it's an HTML line, we
               can increase screenWidth until it will fit. */
            screenWidth++;
            /******* for debugging screen width change
            if (outputToString){
              outputToString = 0;
              print2("debug: screenWidth = %ld\n", screenWidth);
              outputToString = 1;
            }
            ********* end debug */
            /* If this bug happens, we'll have to increase PRINTBUFFERSIZE
               or change the HTML code being printed. */
            if (screenWidth >= PRINTBUFFERSIZE - 1) bug(1517);
            goto HTML_RESTART; /* Ugly but another while loop nesting would
                                  be even more confusing */
          }

          if (breakMatch1[0] == '&') {
            /* Compressed proof */
            p = p + 1; /* We will add a trailing space to line for easier
                          label searches by the user during editing */
          }
        } /* end if (!breakMatch1[0]) else */
      } /* end if (breakMatch1[0] == '&' &&... else */

      if (p <= 0) {
        /* Break character not found; give up at
           screenWidth - (long)tildeFlag  - (long)(breakMatch1[0] == '\\')+ 1 */
        p = screenWidth - (long)tildeFlag  - (long)(breakMatch1[0] == '\\')+ 1;
        if (!firstLine) p = p - startNextLineLen;
        if (p <= 0) p = 1; /* If startNextLine too long */
      }
      if (!p) bug(1515); /* p should never be 0 by this point */
      /* If we broke at a non-space 1st char, line length won't get reduced */
      /* Hopefully this will never happen with the breakMatch's we use,
         otherwise the code will require a rework. */
      if (p == 1 && longLine[0] != ' ') bug(1516);
      if (firstLine) {
        firstLine = 0;
        let(&prefix, "");
      } else {
        let(&prefix, startNextLine1);
        if (treeIndentationFlag) {
          if (startNextLineLen + p - 1 < screenWidth) {
            /* Right justify output for continuation lines */
            let(&prefix, cat(prefix, space(screenWidth - startNextLineLen
                - p + 1), NULL));
          }
        }
      }
      if (!tildeFlag) {
        if (breakMatch1[0] == '\\') {
          /* Add LaTeX comment char to ignore carriage return */
          print2("%s\n",cat(prefix, left(longLine,p - 1), "%", NULL));
        } else {
          print2("%s\n",cat(prefix, left(longLine,p - 1), NULL));
        }
      } else {
        print2("%s\n",cat(prefix, left(longLine,p - 1), "~", NULL));
      }
      if (longLine[p - 1] == ' ' &&
          breakMatch1[0] /* But not "break anywhere" line */) {
        /* Remove leading space for neatness */
        if (longLine[p] == ' ') {
          /* There could be 2 spaces at the end of a sentence. */
          let(&longLine, right(longLine, p + 2));
        } else {
          let(&longLine, right(longLine,p + 1));
        }
      } else {
        let(&longLine, right(longLine,p));
      }
    } /* end while longLine too long */
    if (!firstLine) {
      if (treeIndentationFlag) {
        /* Right justify output for continuation lines */
        print2("%s\n",cat(startNextLine1, space(screenWidth
              - startNextLineLen - strlen(longLine)), longLine, NULL));
      } else {
        print2("%s\n",cat(startNextLine1, longLine, NULL));
      }
    } else {
      print2("%s\n",longLine);
    }
    screenWidth = saveScreenWidth; /* Restore to normal */

  } /* end while multiLine != "" */

  let(&multiLine, ""); /* Deallocate */
  let(&longLine, ""); /* Deallocate */
  let(&prefix, ""); /* Deallocate */
  let(&startNextLine1, ""); /* Deallocate */
  let(&breakMatch1, ""); /* Deallocate */

  return;
} /* printLongLine */


vstring cmdInput(FILE *stream, vstring ask)
{
  /* This function prints a prompt (if 'ask' is not NULL) and gets a line from
    the stream.  NULL is returned when end-of-file is encountered.
    New memory is allocated each time linput is called.  This space must
    be freed by the user if not needed. */
  vstring g = ""; /* always init vstrings to "" for let(&...) to work */
  long i;
#define CMD_BUFFER_SIZE 2000

  while (1) { /* For "B" backup loop */
    if (ask) printf("%s",ask);
    let(&g, space(CMD_BUFFER_SIZE)); /* Allocate CMD_BUFFER_SIZE characters */
    if (g[CMD_BUFFER_SIZE]) bug(1520); /* Bug in let() (improbable) */
    g[CMD_BUFFER_SIZE - 1] = 0; /* For overflow detection */
    if (!fgets(g, CMD_BUFFER_SIZE, stream)) {
      /* End of file */
      return NULL;
    }
    /*g[CMD_BUFFER_SIZE - 1] = 0;*/ /* Guarantee strlen will work */
    /* Warning:  Don't call bug(), because it calls print2 which may call this. */
    if (g[CMD_BUFFER_SIZE - 1]) {
      /* Warning:  Don't call bug(), because it calls print2. */
      /* Detect input overflow */
      printf("***BUG #1508\n");
    }
    i = strlen(g);
    /* Detect operating system bug of inputting no characters */
    if (!i) printf("***BUG #1507\n");
    /* Warning:  Don't call bug(), because it calls print2. */
    /* Detect input overflow - THIS MAY OR MAY NOT WORK; THE PROGRAM MAY
       CRASH BEFORE IT EVER GETS TO THIS POINT */
    /*if (i >= CMD_BUFFER_SIZE - 1) printf("*** BUG #1508\n");*/
/*E*/db = db - (CMD_BUFFER_SIZE - i); /* track string space used to detect leaks */
    if (g[1]) {
      i--;
      if (g[i] != '\n') printf("***BUG #1519\n");
      g[i]=0;   /* Eliminate new-line character by zapping it */
/*E*/db = db - 1;
    } else {
      if (g[0] != '\n') printf("***BUG #1521\n");
      /* Eliminate new-line by deallocating vstring space (if we just zap
         character [0], let() will later think g is an empty string constant
         and will never deallocate g) */
      let(&g, "");
    }

    /* If user typed "B" (for back), go back to the back buffer to
       let the user scroll through it */
    if ((!strcmp(g, "B") || !strcmp(g, "b")) /* User typed "B" */
        && pntrLen(backBuffer) > 1   /* The back-buffer still exists and
                                         there was a previous page */
        && !commandFileOpenFlag
        && (scrollMode == 1 && localScrollMode == 1)
        && !outputToString) {
      /* Set variables so only backup buffer will be looked at in print2() */
      backBufferPos = pntrLen(backBuffer) - 1;
      printf("%s", (vstring)(backBuffer[backBufferPos - 1]));
      backFromCmdInput = 1; /* Flag for print2() */
      print2(""); /* Only the backup buffer will be looked at */
      backFromCmdInput = 0;
    } else {
      /* If the command line is empty (at main prompt), let user still
         type "B" for convenience in case too many
         returns where hit while scrolling */
      if (commandFileOpenFlag) break; /* 23-Aug-04 We're taking from a SUBMIT
                              file so break out of loop that looks for "B" */
      if (ask == NULL) printf("***BUG #1523\n"); /* 23-Aug-04 In non-SUBMIT
          mode 'ask' won't be NULL, so flag non-fatal bug here just in case */
      if (g[0]) break; /* 23-Aug-04 Command line not empty so break out of loop
                          that looks for "B" */
      if (ask != NULL &&
          /* User entered empty command line but not at a prompt */
          /* commandPrompt is assigned in metamath.c and declared in
             mmcmdl.h */
          strcmp(ask, commandPrompt)) {
        break; /* Break out of loop that looks for "B" */
      }
    }
  } /* while 1 */

  return g;
}

vstring cmdInput1(vstring ask)
{
  /* This function gets a line from either the terminal or the command file
    stream depending on commandFileOpenFlag.  It calls cmdInput(). */
  /* Warning: the calling program must deallocate the returned string. */
  vstring commandLine = "";
  vstring ask1 = "";
  long p, i;

  let(&ask1, ask); /* In case ask is temporarily allocated (i.e will become
                      deallocated at next let() */
  /* Look for lines too long */
  while (strlen(ask1) > screenWidth) {
    p = screenWidth - 1;
    while (ask1[p] != ' ' && p > 0) p--;
    if (!p) p = screenWidth - 1;
    print2("%s\n", left(ask1, p));
    let(&ask1, right(ask1, p + 1));
  }
  /* Allow 10 characters for answer */
  if (strlen(ask1) > screenWidth - 10) {
    p = screenWidth - 11;
    while (ask1[p] != ' ' && p > 0) p--;
    if (p) {  /* (Give up if no spaces) */
      print2("%s\n", left(ask1, p));
      let(&ask1, right(ask1, p + 1));
    }
  }

  printedLines = 0; /* Reset number of lines printed since last user input */
  quitPrint = 0; /* Reset quit print flag */
  localScrollMode = 1; /* Reset to prompted scroll */

  while (1) {
    if (!commandFileOpenFlag) {
      commandLine = cmdInput(stdin,ask1);
      if (!commandLine) {
        commandLine = ""; /* Init vstring (was NULL) */
        let(&commandLine, "^Z"); /* ^Z found */
      }
      if (logFileOpenFlag) fprintf(logFilePtr, "%s%s\n", ask1, commandLine);

      /* Clear backBuffer from previous scroll session */
        for (i = 0; i < pntrLen(backBuffer); i++) {
        let((vstring *)(&(backBuffer[i])), "");
      }
      backBufferPos = 1;
      pntrLet(&backBuffer, NULL_PNTRSTRING);
      pntrLet(&backBuffer, pntrAddElement(backBuffer));

      /* Add user's typing to the backup buffer for display on 1st screen */
      let((vstring *)(&(backBuffer[backBufferPos - 1])), cat(
          (vstring)(backBuffer[backBufferPos - 1]), ask1,
          commandLine, "\n", NULL));

      if (listMode && listFile_fp != NULL) {
        /* Put line in list.tmp as comment */
        fprintf(listFile_fp, "! %s\n", commandLine);
      }

    } else { /* Get line from SUBMIT file */
      commandLine = cmdInput(commandFilePtr, NULL);
      if (!commandLine) { /* EOF found */
        fclose(commandFilePtr);
        print2("%s[End of command file \"%s\".]\n", ask1, commandFileName);
        commandFileOpenFlag = 0;
        commandLine = "";
        break; /*continue;*/
      }
      print2("%s%s\n", ask1, commandLine);
    }
    break;
  }

  let(&ask1, ""); /* 10/20/02 Deallocate */
  return commandLine;
}


void errorMessage(vstring line, long lineNum, short column, short tokenLength,
  vstring error, vstring fileName, long statementNum, flag severity)
{
  /* Note:  "line" may be terminated with \n.  "error" and "fileName"
     should NOT be terminated with \n.  This is done for the convenience
     of the calling functions. */
  vstring errorPointer = "";
  vstring tmpStr = "";
  vstring prntStr = "";
  vstring line1 = "";
  int j;

  /* Make sure vstring argument doesn't get deallocated with another let */
/*??? USE SAVETEMPALLOC*/
  let(&tmpStr,error); /* error will get deallocated here */
  error = "";
  let(&error,tmpStr); /* permanently allocate error */

  /* Add a newline to line1 if there is none */
  if (line) {
    if (line[strlen(line) - 1] != '\n') {
      let(&line1, line);
    } else {
      bug(1509);
    }
  } else {
    line1 = NULL;
  }

  if (fileName) {
    /* Put a blank line between error msgs if we are parsing a file */
    print2("\n");
  }

  switch (severity) {
    case (char)_notice:
      let(&prntStr, "?Notice"); break;
    case (char)_warning:
      let(&prntStr, "?Warning"); break;
    case (char)_error:
      let(&prntStr, "?Error"); break;
    case (char)_fatal:
      let(&prntStr, "?Fatal error"); break;
  }
  if (lineNum) {
    let(&prntStr, cat(prntStr, " on line ", str(lineNum), NULL));
    if (fileName)
      let(&prntStr, cat(prntStr, " of file \"", fileName, "\"", NULL));
  } else {
    if (fileName)
      let(&prntStr, cat(prntStr, " in file \"", fileName, "\"", NULL));
  }
  if (statementNum) {
    let(&prntStr, cat(prntStr, " at statement ", str(statementNum), NULL));
    if (statement[statementNum].labelName[0]) {
      let(&prntStr, cat(prntStr, ", label \"",
          statement[statementNum].labelName, "\"", NULL));
    }
    let(&prntStr, cat(prntStr, ", type \"$", chr(statement[statementNum].type),
        "\"", NULL));
  }
  printLongLine(cat(prntStr, ":", NULL), "", " ");
  if (line1) printLongLine(line1, "", "");
  if (line1 && column && tokenLength) {
    let(&errorPointer,"");
    for (j=0; j<column-1; j++) {
      /* Make sure that tabs on the line with the error are accounted for so
         that the error pointer lines up correctly */
      if (line1[j] == '\t') let (&errorPointer,cat(errorPointer,"\t",NULL));
      else let(&errorPointer,cat(errorPointer," ",NULL));
    }
    for (j=0; j<tokenLength; j++)
      let(&errorPointer,cat(errorPointer,"^",NULL));
    printLongLine(errorPointer, "", "");
  }
  printLongLine(error,""," ");
  if (severity == 2) errorCount++;

  /* ???Should there be a limit? */
  /* if (errorCount > 1000) {
    print2("\n"); print2("?Too many errors - aborting MetaMath.\n");
    exit(0);
  } */

  if (severity == 3) {
    print2("Aborting MetaMath.\n");
    exit(0);
  }
  let(&errorPointer,"");
  let(&tmpStr,"");
  let(&prntStr,"");
  let(&error,"");
  if (line1) let(&line1,"");
}




/* Opens files with error message; opens output files with
   backup of previous version.   Mode must be "r" or "w". */
FILE *fSafeOpen(vstring fileName, vstring mode)
{
  FILE *fp;
  vstring prefix = "";
  vstring postfix = "";
  vstring bakName = "";
  vstring newBakName = "";
  long v;

  if (!strcmp(mode, "r")) {
    fp = fopen(fileName, "r");
    if (!fp) {
      print2("?Sorry, couldn't open the file \"%s\".\n", fileName);
    }
    return (fp);
  }

  if (!strcmp(mode, "w")) {
    /* See if the file already exists. */
    fp = fopen(fileName, "r");

    if (fp) {
      fclose(fp);

#define VERSIONS 9
      /* The file exists.  Rename it. */

#if defined __WATCOMC__ /* MSDOS */
      /* Make sure file name before extension is 8 chars or less */
      i = instr(1, fileName, ".");
      if (i) {
        let(&prefix, left(fileName, i - 1));
        let(&postfix, right(fileName, i));
      } else {
        let(&prefix, fileName);
        let(&postfix, "");
      }
      let(&prefix, cat(left(prefix, 5), "~", NULL));
      let(&postfix, cat("~", postfix, NULL));
      if (0) goto skip_backup; /* Prevent compiler warning */

#elif defined __GNUC__ /* Assume unix */
      let(&prefix, cat(fileName, "~", NULL));
      let(&postfix, "");

#elif defined THINK_C /* Assume Macintosh */
      let(&prefix, cat(fileName, "~", NULL));
      let(&postfix, "");

#elif defined VAXC /* Assume VMS */
      /* For debugging on VMS: */
      /* let(&prefix, cat(fileName, "-", NULL));
         let(&postfix, "-"); */
      /* Normal: */
      goto skip_backup;

#else /* Unknown; assume unix standard */
      /*if (1) goto skip_backup;*/  /* [if no backup desired] */
      let(&prefix, cat(fileName, "~", NULL));
      let(&postfix, "");

#endif


      /* See if the lowest version already exists. */
      let(&bakName, cat(prefix, str(1), postfix, NULL));
      fp = fopen(bakName, "r");
      if (fp) {
        fclose(fp);
        /* The lowest version already exists; rename all to lower versions. */

        /* If version VERSIONS exists, delete it. */
        let(&bakName, cat(prefix, str(VERSIONS), postfix, NULL));
        fp = fopen(bakName, "r");
        if (fp) {
          fclose(fp);
          remove(bakName);
        }

        for (v = VERSIONS - 1; v >= 1; v--) {
          let(&bakName, cat(prefix, str(v), postfix, NULL));
          fp = fopen(bakName, "r");
          if (!fp) continue;
          fclose(fp);
          let(&newBakName, cat(prefix, str(v + 1), postfix, NULL));
          rename(bakName, newBakName);
        }

      }
      let(&bakName, cat(prefix, str(1), postfix, NULL));
      rename(fileName, bakName);

      /***
      printLongLine(cat("The file \"", fileName,
          "\" already exists.  The old file is being renamed to \"",
          bakName, "\".", NULL), "  ", " ");
      ***/
    } /* End if file already exists */
   /*skip_backup:*/

    fp = fopen(fileName, "w");
    if (!fp) {
      print2("?Sorry, couldn't open the file \"%s\".\n", fileName);
    }

    let(&prefix, "");
    let(&postfix, "");
    let(&bakName, "");
    let(&newBakName, "");

    return (fp);
  } /* End if mode = "w" */

  bug(1510); /* Illegal mode */
  return(NULL);

}


/* Renames a file with backup of previous version.  If non-zero
   is returned, there was an error. */
int fSafeRename(vstring oldFileName, vstring newFileName)
{
  int error = 0;
  int i;
  FILE *fp;
  /* Open the new file to force renaming of existing ones */
  fp = fSafeOpen(newFileName, "w");
  if (!fp) error = -1;
  /* Delete the file just created */
  if (!error) {
    error = fclose(fp);
    if (error) print2("?Empty \"%s\" couldn't be closed.\n", newFileName);
  }
  if (!error) {
    error = remove(newFileName);
    /* On Windows 95, the first attempt may not succeed. */
    if (error) {
      for (i = 2; i < 1000; i++) {
        error = remove(newFileName);
        if (!error) break;
      }
      if (!error)
        print2("OS WARNING: File delete succeeded only after %i attempts.", i);
    }

    if (error) print2("?Empty \"%s\" couldn't be deleted.\n", newFileName);
  }
  /* Rename the old one to it */
  if (!error) {
    error = rename(oldFileName, newFileName);
    if (error) print2("?Rename of \"%s\" to \"%s\" failed.\n", oldFileName,
        newFileName);
  }
  if (error) {
    print2("?Sorry, couldn't rename the file \"%s\" to \"%s\".\n", oldFileName,
        newFileName);
    print2("\"%s\" may be empty; try recovering from \"%s\".\n", newFileName,
        oldFileName);
  }
  return error;
}


/* Finds the name of the first file of the form filePrefix +
   nnn + ".tmp" that does not exist.  THE CALLER MUST DEALLOCATE
   THE RETURNED STRING [i.e. assign function return directly
   to a local empty vstring with = and not with let(), e.g.
        let(&str1, "");
        str1 = fTmpName("zz~list");  ] */
vstring fGetTmpName(vstring filePrefix)
{
  FILE *fp;
  vstring fname = "";
  static long counter = 0;
  while (1) {
    counter++;
    let(&fname, cat(filePrefix, str(counter), ".tmp", NULL));
    fp = fopen(fname, "r");
    if (!fp) break;
    if (counter > 1000) {
      print2("Warning: too many %snnn.tmp files - will reuse %s\n",
          filePrefix, fname);
      break;
    }
  }
  return fname; /* Caller must deallocate! */
}


/* Added 10/10/02 */
/* This function returns a character string containing the entire contents of
   an ASCII file, or Unicode file with only ASCII characters.   On some
   systems it is faster than reading the file line by line.  The caller
   must deallocate the returned string.  If a NULL is returned, the file
   could not be opened or had a non-ASCII Unicode character or some other
   problem.   If verbose is 0, error and warning messages are suppressed. */
vstring readFileToString(vstring fileName, char verbose) {
  FILE *input_fp;
  long fileBufSize;
  long charCount;
  char *fileBuf;
  long i, j;

  /* Find out the upper limit of the number of characters in the file. */
  /* Do this by opening the file in binary and seeking to the end. */
  input_fp = fopen(fileName, "rb");
  if (!input_fp) {
    if (verbose) print2("?Sorry, couldn't open the file \"%s\".\n", fileName);
    return (NULL);
  }
#ifndef SEEK_END
/* An older GCC compiler didn't have this ANSI standard constant defined. */
#define SEEK_END 2
#endif
  if (fseek(input_fp, 0, SEEK_END)) bug(1511);
  fileBufSize = ftell(input_fp);

  /* Close and reopen the input file in text mode */
  /* Text mode is needed for VAX, DOS, etc. with non-Unix end-of-lines */
  fclose(input_fp);
  input_fp = fopen(fileName, "r");
  if (!input_fp) bug(1512);

  /* Allocate space for the entire input file */
  fileBufSize = fileBufSize + 10;
            /* Add a factor for unknown text formats (just a guess) */
  fileBuf = malloc(fileBufSize * sizeof(char));
  if (!fileBuf) {
    if (verbose) print2(
        "?Sorry, there was not enough memory to read the file \"%s\".\n",
        fileName);
    fclose(input_fp);
    return (NULL);
  }

  /* Put the entire input file into the buffer as a giant character string */
  charCount = fread(fileBuf, sizeof(char), fileBufSize - 2, input_fp);
  if (!feof(input_fp)) {
    print2("Note:  This bug will occur if there is a disk file read error.\n");
    /* If this bug occurs (due to obscure future format such as compressed
       text files) we'll have to add a realloc statement. */
    bug(1513);
  }
  fclose(input_fp);

  fileBuf[charCount] = 0;

  /* See if it's Unicode */
  /* This only handles the case where all chars are in the ASCII subset */
  if (charCount > 1) {
    if (fileBuf[0] == '\377' && fileBuf[1] == '\376') {
      /* Yes, so strip out null high-order bytes */
      if (2 * (charCount / 2) != charCount) {
        if (verbose) print2(
"?Sorry, there are an odd number of characters (%ld) %s \"%s\".\n",
            charCount, "in Unicode file", fileName);
        free(fileBuf);
        return (NULL);
      }
      i = 0; /* ASCII character position */
      j = 2; /* Unicode character position */
      while (j < charCount) {
        if (fileBuf[j + 1] != 0) {
          if (verbose) print2(
              "?Sorry, the Unicode file \"%s\" %s %ld at byte %ld.\n",
              fileName, "has a non-ASCII \ncharacter code",
              (long)(fileBuf[j]) + ((long)(fileBuf[j + 1]) * 256), j);
          free(fileBuf);
          return (NULL);
        }
        if (fileBuf[j] == 0) {
          if (verbose) print2(
              "?Sorry, the Unicode file \"%s\" %s at byte %ld.\n",
              fileName, "has a null character", j);
          free(fileBuf);
          return (NULL);
        }
        fileBuf[i] = fileBuf[j];
        /* Suppress any carriage-returns */
        if (fileBuf[i] == '\r') {
          i--;
        }
        i++;
        j = j + 2;
      }
      fileBuf[i] = 0; /* ASCII string terminator */
      charCount = i;
    }
  }

  /* Make sure the file has no carriage-returns */
  if (strchr(fileBuf, '\r') != NULL) {
    if (verbose) print2(
       "?Warning: the file \"%s\" has carriage-returns.  Cleaning them up...\n",
        fileName);
    /* Clean up the file, e.g. DOS or Mac file on Unix */
    i = 0;
    j = 0;
    while (j <= charCount) {
      if (fileBuf[j] == '\r') {
        if (fileBuf[j + 1] == '\n') {
          /* DOS file - skip '\r' */
          j++;
        } else {
          /* Mac file - change '\r' to '\n' */
          fileBuf[j] = '\n';
        }
      }
      fileBuf[i] = fileBuf[j];
      i++;
      j++;
    }
    charCount = i - 1; /* nm 6-Feb-04 */
  }

  /* Make sure the last line is not a partial line */
  if (fileBuf[charCount - 1] != '\n') {
    if (verbose) print2(
        "?Warning: the last line in file \"%s\" is incomplete.\n",
        fileName);
    /* Add the end-of-line */
    fileBuf[charCount] = '\n';
    charCount++;
    fileBuf[charCount] = 0;
  }

  if (fileBuf[charCount] != 0) {  /* nm 6-Feb-04 */
    bug(1522); /* Keeping track of charCount went wrong somewhere */
  }

  /* Make sure there aren't null characters */
  i = strlen(fileBuf);
  if (charCount != i) {
    if (verbose) {
      print2(
          "?Warning: the file \"%s\" is not an ASCII file.\n",
          fileName);
      print2(
          "Its size is %ld characters with null at character %ld.\n",
          charCount, strlen(fileBuf));
    }
  }
/*E*/db = db + i;  /* For memory usage tracking (ignore stuff after null) */

  /******* For debugging
  print2("In binary mode the file has %ld bytes.\n", fileBufSize - 10);
  print2("In text mode the file has %ld bytes.\n", charCount);
  *******/
  return ((char *)fileBuf);
}