From 7742b5c671f28cf296cc57a6138e467c1a79bd05 Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <thierry.arnoux@gmx.net>
Date: Fri, 24 Dec 2021 14:53:12 +0800
Subject: [PATCH 1/9] Structured Typesetting (STS) generation

---
 .gitignore  |    2 +
 Makefile.am |    4 +-
 makefile    |   11 +
 metamath.c  |   87 ++++-
 mmcmdl.c    |   35 +-
 mmcmds.c    |   39 +-
 mmdata.c    |   76 ++++
 mmdata.h    |   13 +
 mmhlpa.c    |   18 +
 mmhlpb.c    |   19 +-
 mmhtbl.c    |  184 +++++++++
 mmhtbl.h    |   57 +++
 mmwsts.c    | 1069 +++++++++++++++++++++++++++++++++++++++++++++++++++
 mmwsts.h    |   38 ++
 mmwtex.c    |   39 +-
 mmwtex.h    |    5 +
 16 files changed, 1656 insertions(+), 40 deletions(-)
 create mode 100644 .gitignore
 create mode 100644 makefile
 create mode 100644 mmhtbl.c
 create mode 100644 mmhtbl.h
 create mode 100644 mmwsts.c
 create mode 100644 mmwsts.h

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 00000000..77ecc6d2
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+*.o
+metamath
diff --git a/Makefile.am b/Makefile.am
index d49c5d47..c8f773e8 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -15,7 +15,8 @@ noinst_HEADERS = \
 	mmveri.h \
 	mmvstr.h \
 	mmword.h \
-	mmwtex.h
+	mmwtex.h \
+	mmwsts.h
 
 metamath_SOURCES = \
 	metamath.c \
@@ -34,6 +35,7 @@ metamath_SOURCES = \
 	mmvstr.c \
 	mmword.c \
 	mmwtex.c \
+	mmwsts.c \
 	$(noinst_HEADERS)
 
 dist_pkgdata_DATA = \
diff --git a/makefile b/makefile
new file mode 100644
index 00000000..10bb970e
--- /dev/null
+++ b/makefile
@@ -0,0 +1,11 @@
+objects = metamath.o mmcmdl.o mmcmds.o mmdata.o mmhlpa.o mmhlpb.o mminou.o mmmaci.o mmpars.o mmpfas.o mmunif.o mmutil.o mmveri.o mmvstr.o \
+	mmword.o mmwtex.o mmhtbl.o mmwsts.o
+
+
+metamath: $(objects)
+	cc -o metamath $(CFLAGS) $(objects)
+
+%.o: %.c
+	cc -c $*.c -std=gnu99 $(CFLAGS)
+
+
diff --git a/metamath.c b/metamath.c
index 77fee4a1..b8ed3728 100644
--- a/metamath.c
+++ b/metamath.c
@@ -604,6 +604,7 @@
     mmutil.c - Miscellaneous I/O utilities (reserved for future use)
     mmveri.c - Proof verifier for source file
     mmvstr.c - BASIC-like string functions
+    mmwsts.c - Structured typesetting (MathML) generation
     mmwtex.c - LaTeX/HTML source generation
     mmword.c - File revision utility (for TOOLS> UPDATE) (not generally useful)
 */
@@ -638,6 +639,7 @@
 #include "mmunif.h"
 #include "mmword.h"
 #include "mmwtex.h"
+#include "mmwsts.h"
 #ifdef THINK_C
 #include "mmmaci.h"
 #endif
@@ -2289,14 +2291,25 @@ void command(int argc, char *argv[])
       htmlFlag = 1;
       /* If not specified, for backwards compatibility in scripts
          leave altHtmlFlag at current value */
+      /* 7-Jul-17 - MathML/STS handling */
       if (switchPos("/ HTML") != 0) {
-        if (switchPos("/ ALT_HTML") != 0) {
-          print2("?Please specify only one of / HTML and / ALT_HTML.\n");
+        if (switchPos("/ ALT_HTML") != 0 || switchPos("/ STS") != 0 ) {
+          print2("?Please specify only one of / HTML , / ALT_HTML and / STS.\n");
           continue;
         }
         altHtmlFlag = 0;
-      } else {
-        if (switchPos("/ ALT_HTML") != 0) altHtmlFlag = 1;
+      } else if (switchPos("/ ALT_HTML") != 0) {
+        if (switchPos ("/ STS") != 0) {
+          print2 ("?Please specify only one of / HTML , / ALT_HTML and / STS.\n");
+          continue;
+        }
+        altHtmlFlag = 1;
+            } else if (switchPos ("/ STS") != 0) {
+        stsFlag = 1;
+        let(&stsOutput, fullArg[5]);
+
+        /* Parse the STS rules corresponding to the expected output . */
+        parsetSTSRules(stsOutput);
       }
 
       if (2/*error*/ == readTexDefs(0 /* 1 = check errors only */,
@@ -2861,6 +2874,8 @@ void command(int argc, char *argv[])
         switchPos("/ HTML")
         || switchPos("/ BRIEF_HTML")
         || switchPos("/ ALT_HTML")
+      	/* 7-Jul-2017 added MathML/STS */
+        || switchPos("/ STS")
         || switchPos("/ BRIEF_ALT_HTML"))) {
       /* Special processing for the / HTML qualifiers - for each matching
          statement, a .html file is opened, the statement is output,
@@ -2873,6 +2888,8 @@ void command(int argc, char *argv[])
       i = 5;  /* # arguments with only / HTML or / ALT_HTML */
       if (noVersioning) i = i + 2;
       if (switchPos("/ TIME")) i = i + 2;
+      /* 7-Jul-2017 added MathML/STS */
+      if (switchPos("/ STS")) i = i + 1;
       if (rawArgs != i) {
         printLongLine(cat("?The HTML qualifiers may not be combined with",
             " others except / NO_VERSIONING and / TIME.\n", NULL), "  ", " ");
@@ -2925,6 +2942,15 @@ void command(int argc, char *argv[])
         altHtmlFlag = 0;
       }
 
+      /* 7-Jul-2017 added MathML/STS */
+      if (switchPos("/ STS")) {
+        stsFlag = 1;
+        let(&stsOutput, fullArg[5]);
+
+        /* Parse the STS rules corresponding to the expected output. */
+        parsetSTSRules(stsOutput);
+      }
+
       q = 0;
 
       /* Special feature:  if the match statement starts with "*", we
@@ -2996,20 +3022,32 @@ void command(int argc, char *argv[])
             let(&texFileName, cat(statement[showStatement].labelName, ".html",
                 NULL));
         }
-        print2("Creating HTML file \"%s\"...\n", texFileName);
-        texFilePtr = fSafeOpen(texFileName, "w",    /* 17-Jul-2019 nm */
-            noVersioning /*noVersioningFlag*/);
-        /****** old code before 17-Jul-2019 *******
-        if (switchPos("/ NO_VERSIONING") == 0) {
-          texFilePtr = fSafeOpen(texFileName, "w", 0/@noVersioningFlag@/);
-        } else {
-          /@ 6-Jul-2008 nm Added / NO_VERSIONING @/
-          /@ Don't create the backup versions ~1, ~2,... @/
-          texFilePtr = fopen(texFileName, "w");
-          if (!texFilePtr) print2("?Could not open the file \"%s\".\n",
-              texFileName);
+        /* 29-Sep-17 Thierry Arnoux - Post processing (for pre-rendering) */
+        if(stsFlag && strlen(postProcess) != 0) {
+          vstring pipeCommand = "";
+          print2("Creating and processing HTML file \"%s\"...\n", texFileName);
+          let(&pipeCommand, cat(postProcess, " > ", texFileName, NULL));
+          texFilePtr = popen(pipeCommand, "w");
+          if (!texFilePtr) print2("?Could not execute the command \"%s\".\n",
+	          pipeCommand);
+          let(&pipeCommand, "");
+        }
+        else {
+          print2("Creating HTML file \"%s\"...\n", texFileName);
+          texFilePtr = fSafeOpen(texFileName, "w",    /* 17-Jul-2019 nm */
+              noVersioning /*noVersioningFlag*/);
+          /****** old code before 17-Jul-2019 *******
+          if (switchPos("/ NO_VERSIONING") == 0) {
+            texFilePtr = fSafeOpen(texFileName, "w", 0/@noVersioningFlag@/);
+          } else {
+            /@ 6-Jul-2008 nm Added / NO_VERSIONING @/
+            /@ Don't create the backup versions ~1, ~2,... @/
+            texFilePtr = fopen(texFileName, "w");
+            if (!texFilePtr) print2("?Could not open the file \"%s\".\n",
+                texFileName);
+          }
+          ********* end of old code before 17-Jul-2019 *******/
         }
-        ********* end of old code before 17-Jul-2019 *******/
         if (!texFilePtr) goto htmlDone; /* Couldn't open it (err msg was
             provided) */
         texFileOpenFlag = 1;
@@ -3144,7 +3182,10 @@ void command(int argc, char *argv[])
                   if (!instr(1, str3, cat(" ", str1, " ", NULL))) {
                     let(&str3, cat(str3, " ", str1, " ", NULL));
                     let(&str2, "");
-                    str2 = tokenToTex(mathToken[(statement[i].mathString)[j]
+                    /* 27 Jul 2017 tar For MathML/STS */
+                    if(stsFlag) str2 = stsToken((statement[i].mathString)[j], i);
+                    else
+                      str2 = tokenToTex(mathToken[(statement[i].mathString)[j]
                         ].tokenName, i/*stmt# for error msgs*/);
                     /* 2/9/02  Skip any tokens (such as |- in QL Explorer) that
                        may be suppressed */
@@ -3294,7 +3335,8 @@ void command(int argc, char *argv[])
        ABORT_S:
         /*** Close the html file ***/
         printTexTrailer(1 /*texHeaderFlag*/);
-        fclose(texFilePtr);
+        if(stsFlag && strlen(postProcess) != 0) pclose(texFilePtr);
+        else fclose(texFilePtr);
         texFileOpenFlag = 0;
         let(&texFileName,"");
 
@@ -7913,6 +7955,13 @@ void command(int argc, char *argv[])
       continue;
     }
 
+    if (cmdMatches("VERIFY STS")) {
+      /* 12-Dec-17 - Go through all non-definition axioms,
+       * and check whether there is a corresponding STS scheme */
+      verifySts(fullArg[2]);
+      continue;
+    }
+
     print2("?This command has not been implemented.\n");
     continue;
 
diff --git a/mmcmdl.c b/mmcmdl.c
index 6208154f..627715ee 100644
--- a/mmcmdl.c
+++ b/mmcmdl.c
@@ -90,7 +90,7 @@ flag processCommandLine(void)
           "MARKUP|ASSIGN|REPLACE|MATCH|UNIFY|LET|INITIALIZE|DELETE|IMPROVE|",
           /* 11-Sep-2016 nm Added EXPAND */
           "MINIMIZE_WITH|EXPAND|UNDO|REDO|SAVE|DEMO|INVOKE|CLI|EXPLORE|TEX|",
-          "LATEX|HTML|COMMENTS|MORE|",
+          "LATEX|HTML|STS|COMMENTS|MORE|",
           "TOOLS|MIDI|$|<$>", NULL))) goto pclbad;
       if (cmdMatches("HELP OPEN")) {
         /*if (!getFullArg(2, "LOG|TEX|HTML|<LOG>")) goto pclbad;*/
@@ -124,7 +124,7 @@ flag processCommandLine(void)
         goto pclgood;
       }
       if (cmdMatches("HELP VERIFY")) {
-        if (!getFullArg(2, "PROOF|MARKUP|<PROOF>"))
+        if (!getFullArg(2, "PROOF|MARKUP|STS|<PROOF>"))
             goto pclbad;
         goto pclgood;
       }
@@ -570,8 +570,20 @@ flag processCommandLine(void)
             if (!getFullArg(i, cat(
                 "FULL|COMMENT|TEX|OLD_TEX|HTML|ALT_HTML|TIME|BRIEF_HTML",
                 /* 12-May-2009 sa Added MNEMONICS */
-                "|BRIEF_ALT_HTML|MNEMONICS|NO_VERSIONING|<FULL>", NULL)))
+                "|BRIEF_ALT_HTML|MNEMONICS|NO_VERSIONING|<FULL>"
+                /* 7-Jul-2017 added MATHML/STS */
+                "|STS", NULL)))
               goto pclbad;
+            if (lastArgMatches("STS")) {
+              i++;
+              if (strlen(stsOutput)) {
+              if (!getFullArg(i,cat("* Using which output mode <",stsOutput,">? ",NULL)))
+                goto pclbad;
+                        } else {
+              if (!getFullArg(i,"* Using which output mode <mathml>? "))
+                goto pclbad;
+              }
+            }
           } else {
             break;
           }
@@ -1345,7 +1357,7 @@ flag processCommandLine(void)
 
     if (cmdMatches("VERIFY")) {
       if (!getFullArg(1,
-          "PROOF|MARKUP|<PROOF>"))
+          "PROOF|MARKUP|STS|<PROOF>"))
         goto pclbad;
       if (cmdMatches("VERIFY PROOF")) {
         if (sourceHasBeenRead == 0) {
@@ -1405,6 +1417,21 @@ flag processCommandLine(void)
 
         goto pclgood;
       }
+
+      if (cmdMatches("VERIFY STS")) {
+        if (statements == 0) {
+          print2("?No source file has been read in.  Use READ first.\n");
+          goto pclbad;
+        }
+        if (strlen(stsOutput)) {
+          if (!getFullArg(2,cat("* Using which output mode <",stsOutput,">? ",NULL)))
+            goto pclbad;
+        } else {
+          if (!getFullArg(2,"* Using which output mode <mathml>? "))
+            goto pclbad;
+        }
+        goto pclgood;
+      }
     }
 
     if (cmdMatches("DBG")) {
diff --git a/mmcmds.c b/mmcmds.c
index ed7cb81d..b5167a2f 100644
--- a/mmcmds.c
+++ b/mmcmds.c
@@ -24,6 +24,7 @@
 #include "mmpfas.h"
 #include "mmunif.h" /* 26-Sep-2010 nm For bracketMatchInit, minSubstLen */
                     /* 1-Oct-2017 nm ...and firstConst */
+#include "mmwsts.h" /* 27 Jul 2017 tar For MathML/STS */
 
 /* 12-Nov-2018 nm */
 /* Local prototypes */
@@ -342,10 +343,11 @@ void typeStatement(long showStmt,
             }
             htmlDistinctVarsCommaFlag = 1;
             let(&str2, "");
-            str2 = tokenToTex(mathToken[nmbrTmpPtr1[k]].tokenName, showStmt);
+            /* 27 Jul 2017 tar For MathML/STS */
+            if(stsFlag) str2 = stsToken(nmbrTmpPtr1[k], showStmt);
+            else str2 = tokenToTex(mathToken[nmbrTmpPtr1[k]].tokenName, showStmt);
                  /* tokenToTex allocates str2; we must deallocate it */
             let(&htmlDistinctVars, cat(htmlDistinctVars, str2, NULL));
-
           }
           nmbrLet(&nmbrDDList, nmbrAddElement(nmbrDDList, nmbrTmpPtr1[k]));
         }
@@ -361,7 +363,9 @@ void typeStatement(long showStmt,
             }
             htmlDistinctVarsCommaFlag = 1;
             let(&str2, "");
-            str2 = tokenToTex(mathToken[nmbrTmpPtr2[k]].tokenName, showStmt);
+            /* 27 Jul 2017 tar For MathML/STS */
+            if(stsFlag) str2 = stsToken(nmbrTmpPtr2[k], showStmt);
+            else str2 = tokenToTex(mathToken[nmbrTmpPtr2[k]].tokenName, showStmt);
                  /* tokenToTex allocates str2; we must deallocate it */
             let(&htmlDistinctVars, cat(htmlDistinctVars, str2, NULL));
 
@@ -620,11 +624,15 @@ void typeStatement(long showStmt,
           } else {
             if (htmlFlg && texFlag) {
               let(&str2, "");
-              str2 = tokenToTex(mathToken[nmbrTmpPtr1[k]].tokenName, showStmt);
+              /* 27 Jul 2017 tar For MathML/STS */
+      	      if(stsFlag) str2 = stsToken(nmbrTmpPtr1[k], showStmt);
+	            else str2 = tokenToTex(mathToken[nmbrTmpPtr1[k]].tokenName, showStmt);
                    /* tokenToTex allocates str2; we must deallocate it */
               let(&str1, cat(str1, " &nbsp; ", str2, NULL));
               let(&str2, "");
-              str2 = tokenToTex(mathToken[nmbrTmpPtr2[k]].tokenName, showStmt);
+              /* 27 Jul 2017 tar For MathML/STS */
+              if(stsFlag) str2 = stsToken(nmbrTmpPtr2[k], showStmt);
+              else str2 = tokenToTex(mathToken[nmbrTmpPtr2[k]].tokenName, showStmt);
               let(&str1, cat(str1, ",", str2, NULL));
             }
           }
@@ -1301,7 +1309,9 @@ vstring htmlDummyVars(long showStmt)
               /* tokenToTex allocates str1; must deallocate it first */
               let(&str1, "");
               /* Convert token to htmldef/althtmldef string */
-              str1 = tokenToTex(mathToken[dummyVar].tokenName,
+              /* 27 Jul 2017 tar For MathML/STS */
+              if(stsFlag) str1 = stsToken(dummyVar, showStmt);
+              else  str1 = tokenToTex(mathToken[dummyVar].tokenName,
                   showStmt);
               let(&htmlDummyVarList, cat(htmlDummyVarList, " ", str1, NULL));
               break; /* Found a match, so stop further checking */
@@ -1482,7 +1492,9 @@ vstring htmlAllowedSubst(long showStmt)
     if (found == 0) continue; /* All set vars have $d with this wff or class */
 
     let(&str1, "");
-    str1 = tokenToTex(mathToken[wffOrClassVar].tokenName, showStmt);
+    /* 27 Jul 2017 tar For MathML/STS */
+    if(stsFlag) str1 = stsToken(wffOrClassVar, showStmt);
+    else str1 = tokenToTex(mathToken[wffOrClassVar].tokenName, showStmt);
          /* tokenToTex allocates str1; we must deallocate it eventually */
     countInfo++;
     let(&htmlAllowedList, cat(htmlAllowedList, " &nbsp; ",
@@ -1491,7 +1503,9 @@ vstring htmlAllowedSubst(long showStmt)
     for (j = 0; j < setVars; j++) {
       if (setVarDVFlag[j] == 'N') {
         let(&str1, "");
-        str1 = tokenToTex(mathToken[setVar[j]].tokenName, showStmt);
+        /* 27 Jul 2017 tar For MathML/STS */
+        if(stsFlag) str1 = stsToken(setVar[j], showStmt);
+        else str1 = tokenToTex(mathToken[setVar[j]].tokenName, showStmt);
         let(&htmlAllowedList, cat(htmlAllowedList,
             (first == 0) ? "," : "", str1, NULL));
         if (first == 0) countInfo++;
@@ -2437,9 +2451,12 @@ void typeProof(long statemNum,
                       && (!strcmp(statement[stmt].labelName, "cmpt")
                           || !strcmp(statement[stmt].labelName, "cmpt2")))
                   ) {
-                tmpStr1 =
-                    tokenToTex(mathToken[(statement[stmt].mathString)[i]
-                    ].tokenName, stmt);
+                /* 27 Jul 2017 tar For MathML/STS */
+                if(stsFlag) tmpStr1 =
+                  stsToken((statement[stmt].mathString)[i], stmt);
+                else tmpStr1 =
+                  tokenToTex(mathToken[(statement[stmt].mathString)[i]
+                  ].tokenName, stmt);
                 /* 14-Jan-2016 nm */
                 let(&tmpStr1, cat(
                     (altHtmlFlag ? cat("<SPAN ", htmlFont, ">", NULL) : ""),
diff --git a/mmdata.c b/mmdata.c
index 4770b4e8..6df6a659 100644
--- a/mmdata.c
+++ b/mmdata.c
@@ -1061,6 +1061,39 @@ int nmbrEq(nmbrString *s,nmbrString *t)
 }
 
 
+/* Compute a hash of a string */
+/* This simply computes a XOR of the first numbers */
+int nmbrHash(nmbrString *s)
+{
+  static long salt[] = { 4938, 48977, 6897, 7293, 2663, 7925, 2999, 12238,
+      40033, 14038, 10699, 29746, 56108, 34526, 63576, 52053, 61949, 41177, 43740, 22822
+ };
+  long i;
+  long hash = 0;
+  i = -1;
+  while (i < 13 && s[i] != -1) {
+    hash ^= ( s[i] + salt[i] ) << i;
+    i++;
+  }
+  return hash;
+}
+
+
+/* Compare two sub-strings */
+/* Unlike strcmp, this returns a 1 if the strings are equal
+   and 0 otherwise. */
+/* Only the token is compared.  The whiteSpace string is
+   ignored. */
+int nmbrSubEq(nmbrString *s,long sstart, nmbrString *t, long tstart, long len)
+{
+  long i;
+  if (sstart - 1 + len > nmbrLen(s)
+   || tstart - 1 + len > nmbrLen(t)) return 0;
+  for (i = 0; s[sstart-1+i] == t[tstart-1+i] && i<len; i++);
+  return i == len;
+}
+
+
 /* Extract sin from character position start to stop into sout */
 nmbrString *nmbrSeg(nmbrString *sin, long start, long stop)
 {
@@ -1130,6 +1163,34 @@ nmbrString *nmbrSpace(long n)
   return (sout);
 }
 
+/* Search for the nth occurrence of string2 in string1 */
+long nmbrInstrN(long start_position, long occ, nmbrString *string1,
+  nmbrString *string2, long start2, long length2)
+{
+  if (start_position < 1) start_position = 1;
+  start_position--;
+  for(; occ > 0;occ--) {
+    long ls1, i, j;
+    ls1 = nmbrLen(string1);
+    if(start_position++ >= ls1) return 0;
+    for (i = start_position - 1; i <= ls1 - length2; i++) {
+      flag found = 1;
+      for (j = 0; j < length2; j++) {
+        if (string1[i+j] != string2[start2-1+j]) {
+          found = 0;
+          break;
+        }
+      }
+      if (found) {
+	start_position = i+1;
+	break;
+      }
+    }
+    if (i == ls1 - length2 + 1) return 0;
+  }
+  return start_position;
+}
+
 /* Search for string2 in string1 starting at start_position */
 long nmbrInstr(long start_position,nmbrString *string1,
   nmbrString *string2)
@@ -1508,6 +1569,21 @@ nmbrString *nmbrAddElement(nmbrString *g, long element)
 }
 
 
+/* Add a single number to start of a nmbrString - faster than nmbrCat */
+nmbrString *nmbrUnshiftElement(nmbrString *g, long element)
+{
+  long length;
+  nmbrString *v;
+  length = nmbrLen(g);
+  v = nmbrTempAlloc(length + 2); /* Allow for end of string */
+  nmbrCpy(v+1, g);
+  v[0] = element;
+  v[length + 1] = *NULL_NMBRSTRING; /* End of string */
+/*E*/if(db9)getPoolStats(&i1,&j1_,&k1); if(db9)printf("bbg2: pool %ld stat %ld\n",poolTotalFree,i1+j1_);
+  return(v);
+}
+
+
 /* Get the set union of two math token strings (presumably
    variable lists) */
 nmbrString *nmbrUnion(nmbrString *m1, nmbrString *m2)
diff --git a/mmdata.h b/mmdata.h
index adbec398..08b68784 100644
--- a/mmdata.h
+++ b/mmdata.h
@@ -274,6 +274,10 @@ long nmbrLen(nmbrString *s);
 long nmbrAllocLen(nmbrString *s);
 void nmbrZapLen(nmbrString *s, long length);
 
+/* Search for the nth occurrence of string2 in string1 */
+long nmbrInstrN(long start, long occ,nmbrString *string1,
+  nmbrString *string2, long start2, long length2);
+
 /* Search for string2 in string 1 starting at start_position */
 long nmbrInstr(long start, nmbrString *sin, nmbrString *s);
 
@@ -285,6 +289,12 @@ long nmbrRevInstr(long start_position,nmbrString *string1,
 /* 1 if strings are equal, 0 otherwise */
 int nmbrEq(nmbrString *sout,nmbrString *sin);
 
+/* Compute a hash of a string */
+int nmbrHash(nmbrString *s);
+
+/* 1 if substrings are equal, 0 otherwise */
+int nmbrSubEq(nmbrString *s,long sstart, nmbrString *t, long tstart, long len);
+
 /* Converts mString to a vstring with one space between tokens */
 vstring nmbrCvtMToVString(nmbrString *s);
 
@@ -310,6 +320,9 @@ long nmbrElementIn(long start, nmbrString *g, long element);
 /* Add a single number to end of a nmbrString - faster than nmbrCat */
 nmbrString *nmbrAddElement(nmbrString *g, long element);
 
+/* Add a single number to start of a nmbrString - faster than nmbrCat */
+nmbrString *nmbrUnshiftElement(nmbrString *g, long element);
+
 /* Get the set union of two math token strings (presumably
    variable lists) */
 nmbrString *nmbrUnion(nmbrString *m1,nmbrString *m2);
diff --git a/mmhlpa.c b/mmhlpa.c
index 67bdf53a..950e4df4 100644
--- a/mmhlpa.c
+++ b/mmhlpa.c
@@ -790,6 +790,24 @@ H("\"exthtmlhome\" is used instead of that assigned to \"htmltitle\" and");
 H("\"htmlhome\" respectively.");
 H("");
 
+/* 13-Jan-2018 tar Added STS */
+printHelp = !strcmp(saveHelpCmd, "HELP STS");
+H("To create an HTML output file for a $a or $p statement, use");
+H("    SHOW STATEMENT <label> / STS <format>");
+H("The output and usage of that command is similar to the / HTML qualifier.");
+H("However the way the formula is generated differs. Symbols are not mapped");
+H("one-to-one with their HTML representation, instead, the statements are");
+H("matched against patterns. Those patterns are provided in a file named");
+H("    <source>-<format>.MMTS");
+H("Where <source> is the name of the main Metamath file loaded using READ.");
+H("The generic format for the rules in the MMTS definition file is");
+H("    $s <pattern> $: <translation> $.");
+H("Where <pattern> is the pattern to be matched, and <translation> the");
+H("rendered string. If any variable present in <pattern> appears in");
+H("<translation> between hash symbols (#), the corresponding sub-string");
+H("will be recursively matched.");
+H("");
+
 printHelp = !strcmp(saveHelpCmd, "HELP LATEX");
 H("See HELP TEX.");
 H("");
diff --git a/mmhlpb.c b/mmhlpb.c
index 1558eca0..ac5f5b25 100644
--- a/mmhlpb.c
+++ b/mmhlpb.c
@@ -162,7 +162,8 @@ printHelp = !strcmp(saveHelpCmd, "HELP SHOW STATEMENT");
 H(
 "Syntax:  SHOW STATEMENT <label-match> [/ COMMENT] [/ FULL] [/ TEX]");
 H("             [/ OLD_TEX] [/ HTML] [/ ALT_HTML] [/ BRIEF_HTML]");
-H("             [/ BRIEF_ALT_HTML] [/ NO_VERSIONING] [/ MNEMONICS]");
+H("             [/ BRIEF_ALT_HTML] [/ STS <format>] [/ NO_VERSIONING]");
+H("             [/ MNEMONICS]");
 H("");
 H("This command provides information about a statement.  Only statements");
 H("that have labels ($f, $e, $a, and $p) may be specified. <label-match>");
@@ -192,6 +193,12 @@ H("        creates a Web page for the statement.  It may not be used with");
 H("        any other qualifier.  See HELP HTML for more information.");
 H("    / ALT_HTML, / BRIEF_HTML, / BRIEF_ALT_HTML - See HELP HTML for more");
 H("        information on these.");
+/* 13-Jan-2018 tar Added STS */
+H("    / STS This qualifier invokes the HTML mode of SHOW STATEMENT, for");
+H("        creating a Web page for the statement. However it does not so by");
+H("        mapping symbols one-to-one with their HTML representation, but");
+H("        uses an approach based on the structure of the statement.");
+H("        See HELP STS for more information.");
 H("    / NO_VERSIONING - When used with / HTML or the 3 HTML qualifiers");
 H("        above, a backup file suffixed with ~1 is not created (i.e. the");
 H("        previous version is overwritten).");
@@ -691,6 +698,16 @@ H("see the 21-Dec-2017 entry in http://us.metamath.org/mpeuni/mmnotes.txt .");
 H("");
 
 
+printHelp = !strcmp(saveHelpCmd, "HELP VERIFY STS");
+H("Syntax:  VERIFY STS <format>");
+H("");
+H("This command error-checks that the STS rules definition covers all syntax");
+H("defined in the Metamath source file loaded. It runs through all non");
+H("definitional axioms and prints a warning on those which do not have ");
+H("corresponding STS rules. ");
+H("");
+
+
 printHelp = !strcmp(saveHelpCmd, "HELP SUBMIT");
 H("Syntax:  SUBMIT <filename> [/ SILENT]");
 H("");
diff --git a/mmhtbl.c b/mmhtbl.c
new file mode 100644
index 00000000..e6d9f8fc
--- /dev/null
+++ b/mmhtbl.c
@@ -0,0 +1,184 @@
+/*****************************************************************************/
+/*        Copyright (C) 2017  Thierry Arnoux                                 */
+/*            License terms:  GNU General Public License                     */
+/*****************************************************************************/
+/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
+
+/* This module manages hash tables. */
+
+#include <stdlib.h>
+#include "mmhtbl.h"
+#include "mminou.h"
+
+/* Static buffer for the linked lists */
+#define NB_LINKEDITEMS 50000L
+#define NO_LINKEDITEM -1
+linked *linkedItems;
+int free_linkedItem;
+flag htinit_done = 0;
+
+void htinit() {
+  if(htinit_done) return;
+  free_linkedItem = 0;
+  size_t linkedItemsSize = NB_LINKEDITEMS * sizeof(linked);
+  linkedItems = malloc(linkedItemsSize);
+  if (linkedItems == NULL) outOfMemory("#511 (linked items)");
+  for(int i=0; i<NB_LINKEDITEMS-1 ; i++) linkedItems[i].next = i+1;
+  linkedItems[NB_LINKEDITEMS-1].next = NO_LINKEDITEM;
+  htinit_done = 1;
+}
+
+/* Creates a new hashtable.
+   Returns the hashtable created. */
+hashtable htcreate(vstring name, int bucket_count, void *no_obj,
+		  hashFunc *hashF, eqFunc *eqF, letFunc *letF,
+		  freeFunc *freeF, eqFunc *dumpF) {
+  htinit();
+
+  /* Allocate space for the bucket pointers */
+  int *buckets = malloc(bucket_count * sizeof(int));
+  if (!buckets) outOfMemory("#512 (hashtable buckets)");
+
+  /* Each bucket initially contains an empty list */
+  for(int i=0; i<bucket_count ; i++) buckets[i] = NO_LINKEDITEM;
+
+  /* Create and fill the structure */
+  hashtable ht;
+  ht.name = name;
+  ht.bucket_count = bucket_count;
+  ht.buckets = buckets;
+  ht.no_obj = no_obj;
+  ht.hashFunc = hashF;
+  ht.eqFunc = eqF;
+  ht.letFunc = letF;
+  ht.freeFunc = freeF;
+  ht.dumpFunc = dumpF;
+  ht.entries = 0;
+  ht.gets = 0;
+  ht.founds = 0;
+  ht.biggest_bucket_size = 0;
+  return ht;
+}
+
+/* Deletes a hashtable.
+   Cleans up the hashtable, returning linked items and freeing objects and keys. */
+void htdelete(hashtable *hashtable) {
+  /* for each bucket */
+  for(int bucket = 0;bucket<hashtable->bucket_count;bucket++) {
+    /* Go through the linked list and free each key/object */
+    int *pli = &hashtable->buckets[bucket];
+    while(*pli != NO_LINKEDITEM) {
+      hashtable->freeFunc(&linkedItems[*pli].key, &linkedItems[*pli].object);
+      pli = &linkedItems[*pli].next;
+    }
+    /* Then put the whole linked list on the free list */
+    if(hashtable->buckets[bucket] != NO_LINKEDITEM) {
+      int old_free = free_linkedItem;
+      free_linkedItem = hashtable->buckets[bucket];
+      *pli = old_free;
+    }
+  }
+}
+
+/* Puts a new object in the hashtable.
+   Returns 1 if successful, 0 otherwise. */
+flag htput(hashtable *hashtable, void *key, void *object) {
+  /* First we need a free linked item */
+  int linkedItem = free_linkedItem;
+  if(linkedItem == NO_LINKEDITEM) return 0;
+  free_linkedItem = linkedItems[linkedItem].next;
+
+  /* Store object and key */
+  hashtable->letFunc(&linkedItems[linkedItem].key,
+		     &linkedItems[linkedItem].object, key, object);
+  hashtable->entries++;
+
+  /* Compute the bucket */
+  unsigned int bucket = hashtable->hashFunc(key) % hashtable->bucket_count;
+
+  /* Insert at the beginning of the list */
+  linkedItems[linkedItem].next = hashtable->buckets[bucket];
+  hashtable->buckets[bucket] = linkedItem;
+  return 1;
+}
+
+/* Gets an object from the hashtable, based on its key.
+   Returns the object pointer if successful, NULL otherwise. */
+void *htget(hashtable *hashtable, void *key) {
+  hashtable->gets++;
+  /* Compute the bucket */
+  unsigned int bucket = hashtable->hashFunc(key) % hashtable->bucket_count;
+  int bucket_size = 0;
+
+  /* Look for the key */
+  int li = hashtable->buckets[bucket];
+  while(li != NO_LINKEDITEM) {
+    if(hashtable->eqFunc(linkedItems[li].key, key)) {
+      /* Found it, return the associated object */
+      hashtable->founds++;
+      return linkedItems[li].object;
+    }
+    li = linkedItems[li].next;
+    bucket_size++;
+  }
+  /* For stats only */
+  if(bucket_size > hashtable->biggest_bucket_size) {
+    hashtable->biggest_bucket_size = bucket_size;
+    hashtable->biggest_bucket = bucket;
+  }
+
+  /* Object was not found */
+  return hashtable->no_obj;
+}
+
+flag htremove(hashtable *hashtable, void *key) {
+  /* Compute the bucket */
+  unsigned int bucket = hashtable->hashFunc(key) % hashtable->bucket_count;
+
+  /* Look for the key */
+  int *pli = &hashtable->buckets[bucket];
+  while(*pli != NO_LINKEDITEM) {
+    if(!hashtable->eqFunc(linkedItems[*pli].key, key)) {
+      /* Found it, free the object and remove it from the chain */
+      hashtable->freeFunc(&linkedItems[*pli].key, &linkedItems[*pli].object);
+      int old_free = free_linkedItem;
+      free_linkedItem = *pli;
+      *pli = linkedItems[*pli].next;
+      linkedItems[*pli].next = old_free;
+      hashtable->entries--;
+      return 1;
+    }
+    pli = &linkedItems[*pli].next;
+  };
+
+  /* Object was not found */
+  return 0;
+}
+
+/*  Returns the hashtable load factor in percent */
+int htlf(hashtable *hashtable) {
+  return 100 * hashtable->entries / hashtable->bucket_count;
+}
+
+/* Dumps stats about the hash table */
+void htstats(hashtable *hashtable) {
+  int empty_buckets = 0;
+  for(int bucket=0;bucket<hashtable->bucket_count;bucket++) empty_buckets+=hashtable->buckets[bucket] == NO_LINKEDITEM;
+  printf("Hashtable %s: %d entries, load factor=%d%%, %d used buckets, %d%% misses, biggest bucket=%d\n", hashtable->name, hashtable->entries,
+	 htlf(hashtable), (hashtable->bucket_count - empty_buckets), (100-(100*hashtable->founds/hashtable->gets)),
+	 hashtable->biggest_bucket_size);
+}
+
+/* Dumpts the whole table */
+void htdump(hashtable *hashtable) {
+  print2("Hashtable %s:\n", hashtable->name);
+  //for(int bucket=0;bucket<hashtable->bucket_count;bucket++) {
+  int bucket = hashtable->biggest_bucket;
+  {
+    int li = hashtable->buckets[bucket];
+    while(li != NO_LINKEDITEM) {
+      hashtable->dumpFunc(linkedItems[li].key, linkedItems[li].object);
+      li = linkedItems[li].next;
+    }
+  }
+}
diff --git a/mmhtbl.h b/mmhtbl.h
new file mode 100644
index 00000000..87f68ea1
--- /dev/null
+++ b/mmhtbl.h
@@ -0,0 +1,57 @@
+/*****************************************************************************/
+/*        Copyright (C) 2012  NORMAN MEGILL  nm at alum.mit.edu              */
+/*            License terms:  GNU General Public License                     */
+/*****************************************************************************/
+/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
+
+#ifndef MMHTBL_H_
+#define MMHTBL_H_
+
+#include <stdio.h>
+#include "mmutil.h"
+#include "mmvstr.h"
+#include "mmdata.h"
+
+typedef int (hashFunc)(void *);
+typedef int (eqFunc)(void *, void *);
+typedef void (letFunc)(void **, void **, void *, void*);
+typedef void (freeFunc)(void *, void *);
+
+struct linked_struct {
+  void *object;
+  void *key;
+  int next;
+};
+
+typedef struct linked_struct linked;
+
+struct hashtable_struct {
+  vstring name;
+  int bucket_count;
+  int *buckets;
+  int entries;
+  int gets;
+  int founds;
+  int biggest_bucket;
+  int biggest_bucket_size;
+  void *no_obj;
+  hashFunc *hashFunc;
+  eqFunc *eqFunc;
+  letFunc *letFunc;
+  freeFunc *freeFunc;
+  eqFunc *dumpFunc;
+};
+
+typedef struct hashtable_struct hashtable;
+
+hashtable htcreate(vstring name, int bucket_count, void *no_obj,
+		   hashFunc *hashF, eqFunc *eqF, letFunc *letF,
+		   freeFunc *freeF, eqFunc *dumpF);
+void htdelete(hashtable *hashtable);
+flag htput(hashtable *hashtable, void *key, void *object);
+void *htget(hashtable *hashtable, void *key);
+flag htremove(hashtable *hashtable, void *key);
+void htstats(hashtable *hashtable);
+void htdump(hashtable *hashtable);
+
+#endif /* MMHTBL_H_ */
diff --git a/mmwsts.c b/mmwsts.c
new file mode 100644
index 00000000..920dcdde
--- /dev/null
+++ b/mmwsts.c
@@ -0,0 +1,1069 @@
+/*****************************************************************************/
+/*        Copyright (C) 2017  Thierry Arnoux                                 */
+/*            License terms:  GNU General Public License                     */
+/*****************************************************************************/
+/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
+
+/* This module processes structured typesetting output. */
+
+#include <string.h>
+#include <stdio.h>
+#include <limits.h>
+#include <stdlib.h>
+#include <ctype.h>
+#include <stdarg.h>
+#include "mmutil.h"
+#include "mmvstr.h"
+#include "mmdata.h"
+#include "mminou.h"
+#include "mmpars.h" /* For rawSourceError and mathSrchCmp and lookupLabel */
+#include "mmcmdl.h" /* For texFileName */
+#include "mmwsts.h"
+#include "mmwtex.h" /* For texDefsRead */
+#include "mmhtbl.h" /* For caching results */
+
+#define STS_MAX_TYPES 10		/* basic types. For set.mm, there are 4 (|-,wff,class,set) */
+#define STS_MAX_RECURSION 50	/* max depth of a formula (heuristic to avoid loops) */
+#define STS_MAX_SCHEME_VAR 20	/* max variables per schemes */
+#define STS_MAX_TOKEN_REUSE 20
+#define STS_MAX_LEN_FOR_CACHE 20 /* put only formulas of up to 20 tokens into cache */
+#define STS_CACHE_BUCKETS 50000	 /* size of a cache hash bucket */
+
+/* The structure containing the structured typesetting replacement schemes */
+struct stsScheme_struct {
+  char type; /* 'i' for identifier, 's' for scheme. */
+  nmbrString *scheme; /* The scheme */
+  vstring typesetting; /* The typesetting to be displayed */
+  int varCount; /* The number of variables in the scheme */
+};
+
+/* The structure containing information about the STS variable tokens */
+struct stsVar_struct {
+  long stsType; /* type of the token in the STS (must be a constant tokenId) */
+  long stsSchemeId; /* number of the schemed in which this variable is defined + 1. */
+  vstring anchor; /* anchor for the STS, or "" if not allocated yet */
+  flag isTerminal; /* whether or not this is one of the terminal type constants */
+};
+
+/* Current output format for STS */
+vstring stsFormat = "";
+
+/* STS header to be added to the HTML HEAD element of each generated page */
+vstring stsHeader = "";
+
+/* Prefix/Suffix for the output of each formula when in-text (in comments) */
+vstring stsInText[2] = { "", "" };
+
+/* Prefix/Suffix for the output of each formula when displayed (in proofs) */
+vstring stsDisplayed[2] = { "", "" };
+
+/* The pointer containing the structured typesetting replacement schemes */
+struct stsScheme_struct *stsScheme = NULL;
+long stsSchemes = 0;
+
+/* The pointer containing the structured typesetting replacement schemes */
+struct stsVar_struct *stsVar = NULL;
+long stsVars = 0;
+
+/* The basic types used for parsing tokens or comments */
+nmbrString *stsTerminalTypes = NULL_NMBRSTRING;
+
+/* debug trace levels for STS */
+flag dbs1 = 0; /* shows top-level calls to STS printing */
+flag dbs3 = 0; /* shows substitution results */
+flag dbs5 = 0; /* shows all substitutions tried */
+flag dbs7 = 0; /* shows details of substitution "unification" */
+flag dbs9 = 0; /* shows details of substring searches in "unification" */
+flag stsUseCache = 0; /* store generation results into cache */
+
+/**/
+void debugOn() {
+  dbs1 = 1; /* shows top-level calls to STS printing */
+  dbs3 = 1; /* shows substitution results */
+  dbs5 = 1; /* shows all substitutions tried */
+  dbs7 = 0; /* shows details of substitution "unification" */
+  dbs9 = 0; /* shows details of substring searches in "unification" */
+}
+
+/**/
+void debugOff() {
+  dbs1 = 0; /* shows top-level calls to STS printing */
+  dbs3 = 0; /* shows substitution results */
+  dbs5 = 0; /* shows all substitutions tried */
+  dbs7 = 0; /* shows details of substitution "unification" */
+  dbs9 = 0; /* shows details of substring searches in "unification" */
+}
+
+
+vstring stsChunkName(char c) {
+  switch(c) {
+  case 'i': return "identifier";
+  case 's': return "scheme";
+  case 'd': return "display code";
+  case 't': return "text code";
+  case 'h': return "header code";
+  case 'c': return "command line";
+  case 'u': return "terminal types";
+  default: return "unknown chunk";
+  }
+}
+
+/* Cache to speed up conversions */
+hashtable stsCache;
+
+/* Math symbol comparison for bsearch */
+/* Here, key is pointer to a character string. */
+/* Here we search only the global tokens, those
+ * which endStatement is the last statement */
+int mathSrchGlbCmp(const void *key, const void *data)
+{
+  /* Returns -1 if key < data, 1 if key > data */
+  int ret = strcmp(key, mathToken[ *((long *)data) ].tokenName);
+  if(ret != 0) return ret;
+
+  /* We have found two identical entries.
+   * However we shall return 0 (match) only if the token is global. */
+  if(mathToken[ *((long *)data) ].endStatement == statements) return 0;
+
+  /* Find the direction in which the target token is */
+  for(long *ptr = (long*)data; !strcmp(key, mathToken[ *ptr ].tokenName); ptr++)
+    if(mathToken[ *ptr ].endStatement == statements) return 1;
+  return -1;
+}
+
+/* Similar to mmpars's parseMathTokens, this is a general-purpose
+ * function to parse a math token string. However this version does
+ * not allow to skip spaces. */
+nmbrString *parseMathStrict(vstring text)
+{
+  /* The result */
+  nmbrString *mathString = NULL_NMBRSTRING;
+  long mathStringLen = 0;
+
+  /* Temporary working space */
+  long wrkLen;
+  nmbrString *wrkNmbrPtr;
+
+  long i;
+  char *fbPtr;
+  long textLen, tokenLen_;
+  long *mathKeyPtr; /* bsearch returned value */
+
+  /* Make sure that mathTokens has been initialized */
+  if (!mathTokens) bug(1717);
+
+  textLen = (long)strlen(text);
+
+  /* Initialize temporary working space for parsing tokens */
+  /* Assume the worst case of one token per 2 text characters */
+  wrkLen = textLen/2+1;
+  wrkNmbrPtr = malloc((size_t)wrkLen * sizeof(nmbrString));
+  if (!wrkNmbrPtr) outOfMemory("#502 (wrkNmbrPtr)");
+
+  /* Scan the math section for tokens */
+  fbPtr = text;
+  while (1) {
+    fbPtr = fbPtr + whiteSpaceLen(fbPtr);
+    tokenLen_ = tokenLen(fbPtr);
+    if (!tokenLen_) break; /* Done scanning source line */
+
+    fbPtr[tokenLen_] = 0; /* End token - There's no come back */
+    //printf("Searching for %s\n", fbPtr);
+    mathKeyPtr = (long *)bsearch(fbPtr, mathKey,
+	(size_t)mathTokens, sizeof(long), mathSrchGlbCmp);
+    if (!mathKeyPtr) {
+      /* Unknown token, escape. */
+      print2("?Unknown token %s\n", fbPtr);
+      free(wrkNmbrPtr);
+      return NULL_NMBRSTRING;
+    }
+    wrkNmbrPtr[mathStringLen] = *mathKeyPtr;
+    mathStringLen++;
+    fbPtr = fbPtr + tokenLen_ + 1; /* Move on to next token */
+    if(fbPtr >= text + textLen) break;
+  }
+
+  /* Assign mathString */
+  nmbrLet(&mathString, nmbrSpace(mathStringLen));
+  for (i = 0; i < mathStringLen; i++)
+    mathString[i] = wrkNmbrPtr[i];
+  if (mathStringLen) nmbrMakeTempAlloc(mathString); /* Flag for dealloc*/
+  free(wrkNmbrPtr);
+  return mathString;
+}
+
+/* Store a couple key/object into the cache */
+void stsStoreCache(nmbrString **tKey, vstring *tObject, nmbrString *sKey, vstring sObject) {
+  *tKey = NULL_NMBRSTRING;
+  nmbrLet(tKey, sKey);
+
+  *tObject = "";
+  let(tObject, sObject);
+}
+
+/* Free a couple key/object from the cache */
+void stsFreeCache(nmbrString **key, vstring *object) {
+  nmbrLet(key, NULL_NMBRSTRING);
+  let(object, NULL);
+}
+
+/* Dump a couple key/object from the cache */
+void stsDumpCache(nmbrString *key, vstring object) {
+//  printf("- %s -> %s\n", nmbrCvtMToVString(key), object);
+  printf("- (%d) %s [%s]\n", nmbrHash(key), nmbrCvtMToVString(key), nmbrCvtAnyToVString(key));
+}
+
+/* Parse a file containing the structured typesetting rules. */
+int parsetSTSRules(vstring format) {
+  vstring inputFn = "";
+  vstring chunk = "";
+  char chunkType = 0;
+  flag ots = outputToString;
+  outputToString = 0;
+
+  /* If the same format was already parsed, nothing to do. */
+  if(strcmp(stsFormat, format) == 0) {
+    return 0;
+  }
+  /* Format is invalid until fully parsed. */
+  let(&stsFormat, "");
+
+  /* Create a cache for exported statements to speed up */
+  if(stsUseCache) {
+    stsCache = htcreate(format, STS_CACHE_BUCKETS, "", (hashFunc*)&nmbrHash, (eqFunc*)&nmbrEq,
+			(letFunc*)&stsStoreCache, (freeFunc*)&stsFreeCache,
+			(eqFunc*)&stsDumpCache);
+  }
+
+  /* Build the name of the MMTS file to load */
+  let(&inputFn, cat(rootDirectory ,
+      left(input_fn, instr(1,input_fn,".mm")-1), "-", format, ".mmts", NULL));
+
+  FILE *sts_fp = fSafeOpen(inputFn, "r", 1);
+  if(!sts_fp) return 0; /* Error message is provided by fSafeOpen */
+
+  /* Determine file size */
+  #ifndef SEEK_END
+  /* An older GCC compiler didn't have this ANSI standard constant defined. */
+  #define SEEK_END 2
+  #endif
+  if (fseek(sts_fp, 0, SEEK_END)) bug(5701);
+  long fileBufSize = ftell(sts_fp);
+  /*E*/if(db5)print2("In binary mode the file has %ld bytes.\n",fileBufSize);
+
+  /* Allocate space for the entire input file */
+  fileBufSize = fileBufSize + 10; /* Add a factor for unknown text formats */
+  char *fileBuf = malloc((size_t)fileBufSize);
+  if (!fileBuf) outOfMemory("#501 (fileBuf)");
+
+  if (fseek(sts_fp, 0, SEEK_SET)) bug(5702);
+  /* Put the entire input file into the buffer as a giant character string */
+  long charCount = (long)fread(fileBuf, sizeof(char), (size_t)fileBufSize - 2,
+			       sts_fp);
+  if (!feof(sts_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(5703);
+  }
+  fclose(sts_fp);
+  fileBuf[charCount] = 0; /* End of string */
+
+  /* Initialize the STS Schemes list */
+  stsScheme = malloc((size_t)MAX_MATHTOKENS * sizeof(struct stsScheme_struct));
+  if (!stsScheme) {
+    print2("*** FATAL ***  Could not allocate stsScheme space\n");
+    bug(5001);
+    }
+  stsSchemes = 0;
+
+  /* Initialize and clear the STS Variable list */
+  stsVar = calloc((size_t)MAX_MATHTOKENS, sizeof(struct stsVar_struct));
+  if (!stsVar) {
+    print2("*** FATAL ***  Could not allocate stsVar space\n");
+    bug(5002);
+    }
+
+  /* Actual parsing starts */
+  print2("Reading structured typesetting from \"%s\"...\n", inputFn);
+
+  /* Look for $[ and $] 'include' statement start and end */
+  char *fbPtr = fileBuf;
+  char *startPtr = NULL;
+  long lineNum = 1;
+  flag insideComment = 0; /* 1 = inside $( $) comment */
+  flag insideChunk = 0;  /* 1 = inside $s $: scheme */
+  flag insideTypeSet = 0; /* 1 = inside $: $. typeset */
+  while (1) {
+    /* Find a keyword or newline */
+    char tmpch = fbPtr[0];
+    if (!tmpch) { /* End of file */
+      if (insideComment) {
+        rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum - 1, inputFn,*/
+         "The last comment in the file is incomplete.  \"$)\" was expected.");
+	if (insideChunk) {
+          rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+              cat("The last ", stsChunkName(chunkType),
+		  " in the file is incomplete.", NULL));
+        }
+        if (insideTypeSet) {
+          rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+              "The last typesetting in the file is incomplete.");
+        }
+      }
+      break;
+    }
+    if (tmpch != '$') {
+      if (tmpch == '\n') {
+        lineNum++;
+      } else {
+          if (!isgraph((unsigned char)tmpch) && !isspace((unsigned char)tmpch)) {
+            rawSourceError(fileBuf, fbPtr, 1, /*lineNum, inputFn,*/
+                cat("Illegal character (ASCII code ",
+                str((double)((unsigned char)tmpch)),
+                " decimal).",NULL));
+        }
+      }
+      fbPtr++;
+      continue;
+    }
+
+    /* Detect missing whitespace around keywords (per current Metamath
+     * language spec) */
+    if (fbPtr > fileBuf) {  /* If this '$' is not the 1st file character */
+      if (isgraph((unsigned char)(fbPtr[-1]))) {
+        /* The character before the '$' is not white space */
+        if (!insideComment || fbPtr[1] == ')') {
+          /* Inside comments, we only care about the "$)" keyword */
+          rawSourceError(fileBuf, fbPtr, 2, /*lineNum, inputFn,*/
+              "A keyword must be preceded by white space.");
+        }
+      }
+    }
+    fbPtr++;
+    if (fbPtr[0]) {  /* If the character after '$' is not end of file (which
+                        would be an error anyway, but detected elsewhere) */
+      if (isgraph((unsigned char)(fbPtr[1]))) {
+        /* The character after the character after the '$' is not white
+           space (nor end of file) */
+        if (!insideComment || fbPtr[0] == ')') {
+          /* Inside comments, we only care about the "$)" keyword */
+          rawSourceError(fileBuf, fbPtr + 1, 1, /*lineNum, inputFn,*/
+              "A keyword must be followed by white space.");
+          }
+      }
+    }
+
+    switch (fbPtr[0]) {
+      case '(': /* Start of comment */
+        if (insideComment) {
+          rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+              "Nested comments are not allowed.");
+        }
+        insideComment = 1;
+        continue;
+
+      case ')': /* End of comment */
+        if (!insideComment) {
+          rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+              "A comment terminator was found outside of a comment.");
+        }
+        insideComment = 0;
+        continue;
+
+      case 'd': /* Start of display code */
+      case 't': /* Start of text code */
+      case 'h': /* Start of header code */
+      case 'c': /* Start of command line */
+      case 'i': /* Start of identifier */
+      case 's': /* Start of scheme */
+      case 'u': /* Start of terminal type */
+	if (insideComment) continue;
+	if (insideChunk) {
+          rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+              cat("A scheme start was found within a ",
+		  stsChunkName(chunkType), ".", NULL));
+        }
+        if (insideTypeSet) {
+          rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+              cat("A ",stsChunkName(fbPtr[0]),
+		  " start was found within a typeset.", NULL));
+        }
+        chunkType = fbPtr[0];
+        startPtr = fbPtr + 1;
+        insideChunk = 1;
+	continue;
+
+      case ':': /* Start of typesetting */
+	if (insideComment) continue;
+        if (!insideChunk || (chunkType != 's' && chunkType != 'i')) {
+          rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+              "A scheme end was found outside of a scheme.");
+        }
+        if (insideTypeSet) {
+          rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+              "A scheme end was found within a typeset.");
+        }
+        vstring text = mid(startPtr, 0, fbPtr - startPtr - 1);
+        //print2("end scheme line %ld! %s\n", lineNum, text);
+        stsScheme[stsSchemes].type = chunkType;
+        stsScheme[stsSchemes].scheme = NULL_NMBRSTRING;
+	// parseMathTokens is too permissive. Wrote own token parser.
+        //nmbrLet(&(stsScheme[stsSchemes].scheme), parseMathTokens(text, statements));
+        nmbrLet(&(stsScheme[stsSchemes].scheme), parseMathStrict(text));
+
+        int l = nmbrLen(stsScheme[stsSchemes].scheme);
+        if(l < 2) {
+          if(l == 0)
+	    rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+		"Empty scheme or unknown token.");
+          else
+	    rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+		"A scheme shall contain at least 2 tokens.");
+          chunkType = '$'; // invalid chunk type, so that the scheme is skipped.
+          startPtr = fbPtr + 1;
+          insideChunk = 0;
+	  insideTypeSet = 1;
+	  stsSchemes--;
+	  continue;
+          }
+
+        /* Store the number of variables in the scheme (each shall be different)  */
+        stsScheme[stsSchemes].varCount = 0;
+        for(int i=0;i<l;i++)
+          if(mathToken[stsScheme[stsSchemes].scheme[i]].tokenType == var_)
+            stsScheme[stsSchemes].varCount++;
+
+        /* Store the variable "type" (wff, set or class for set.mm)  */
+        if(chunkType == 'i') {
+          if(l != 2)
+            rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+                "An identifier definition shall contain exactly 2 tokens.");
+          long index = stsScheme[stsSchemes].scheme[1];
+          stsVar[index].stsType = stsScheme[stsSchemes].scheme[0];
+          stsVar[index].stsSchemeId = stsSchemes + 1;
+          stsVar[index].anchor = "";
+
+          if(mathToken[stsVar[index].stsType].tokenType != con_)
+            rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+                "An identifier definition shall start with a constant.");
+          if(mathToken[index].tokenType != var_)
+            rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+                "An identifier definition shall end with a variable.");
+	    //print2("Token %s has type %s\n", mathToken[index].tokenName, mathToken[stsVar[index].stsType].tokenName);
+        }
+
+        startPtr = fbPtr + 1;
+        insideChunk = 0;
+	insideTypeSet = 1;
+	continue;
+
+      case '.': /* End of chunk/typesetting */
+	if (insideComment) continue;
+	if (!insideChunk && !insideTypeSet) {
+          rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+              "A chunk/typeset end was found outside a chunk or typeset.");
+	}
+	insideChunk = 0;
+	switch(chunkType) {
+	  case 'i':
+	  case 's':
+	    /* End of typesetting, record the new scheme. */
+	    if(!insideTypeSet) {
+	      rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+		  cat("A typeset end was found within a ",
+		      stsChunkName(chunkType), ".", NULL));
+	    }
+	    stsScheme[stsSchemes].typesetting = "";
+	    let(&(stsScheme[stsSchemes].typesetting), mid(startPtr, 2, fbPtr - startPtr - 3));
+	    /* Record the schemeId */
+	    if(nmbrLen(stsScheme[stsSchemes].scheme) == 2
+	       && stsVar[stsScheme[stsSchemes].scheme[1]].stsSchemeId == 0)
+		stsVar[stsScheme[stsSchemes].scheme[1]].stsSchemeId = stsSchemes + 1;
+//	    for(int i=1;i<=nmbrLen(stsScheme[stsSchemes].scheme);i++)
+//	      if(stsVar[stsScheme[stsSchemes].scheme[i]].stsSchemeId == 0)
+//		stsVar[stsScheme[stsSchemes].scheme[i]].stsSchemeId = stsSchemes + 1;
+	    stsSchemes++;
+	    insideTypeSet = 0;
+	    continue;
+
+	  case 'd':
+	  case 't':
+	    /* End of the display/text chunk */
+	    let(&chunk, mid(startPtr, 2, fbPtr - startPtr - 3));
+	    long pos = instr(1, chunk, "###");
+	    if(pos == 0) {
+	      rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+		  "Display/text chunk shall contain ###, which will be replaced"
+		  " by the generated formula in the generated HTML file.");
+	      let(&chunk, "");
+	      continue;
+	    }
+	    long end = pos + 3;
+	    vstring *target;
+	    if(chunkType == 'd') target = stsDisplayed;
+	    if(chunkType == 't') target = stsInText;
+	    let(&(target[0]), left(chunk, pos-1));
+	    let(&(target[1]), mid(chunk, end, len(chunk)-end+1));
+	    let(&chunk, "");
+	    continue;
+
+	  case 'h':
+	    /* End of the header chunk */
+	    let(&stsHeader, mid(startPtr, 2, fbPtr - startPtr - 3));
+	    continue;
+
+	  case 'c':
+	    /* End of the command line chunk */
+	    let(&postProcess, mid(startPtr, 2, fbPtr - startPtr - 3));
+	    continue;
+
+	  case 'u':
+	    /* End of terminal types list chunk */
+	    {
+	      vstring text = mid(startPtr, 2, fbPtr - startPtr - 3);
+	      nmbrLet(&stsTerminalTypes, parseMathStrict(text));
+	      for(int i=0;i<nmbrLen(stsTerminalTypes);i++) stsVar[stsTerminalTypes[i]].isTerminal = 1;
+	      continue;
+	    }
+
+	  case '$':
+	    /* Error handling for incorrect schemes */
+	    insideTypeSet = 0;
+	    continue;
+	}
+    }
+  }
+
+  print2("%ld typesetting statements were read from \"%s\".\n", stsSchemes, inputFn);
+  /* Format is invalid */
+  let(&stsFormat, format);
+
+  if (!errorCount) {
+    print2("No errors were found.\n");
+  } else {
+    if (errorCount == 1) {
+      print2("One error was found.\n");
+    } else {
+      print2("%ld errors were found.\n", (long)errorCount);
+    }
+  }
+
+  /* Free vstrings and memory */
+  let(&inputFn, "");
+  free(fileBuf);
+
+  /* Return back to outputting in a string */
+  outputToString = ots;
+
+  texDefsRead = 1;
+  return 1;
+}
+
+/* initialize a table with the brackets (of set.mm) */
+char *bracketsOpnStr = "( { [ [. [_ <.";
+char *bracketsClsStr = ") } ] ]. ]_ >.";
+nmbrString *bracketsOpn = NULL_NMBRSTRING, *bracketsCls = NULL_NMBRSTRING;
+
+/* Returns whether or not a nmbrString is balanced in terms of brackets */
+flag nmbrBalanced(nmbrString *str, long start, long len) {
+  /* TODO we could use the global bracketMatchOn to detect if we are in set.mm */
+  /*if(!bracketMatchOn) return 1;*/
+  if(bracketsOpn == NULL_NMBRSTRING) {
+    nmbrLet(&bracketsOpn, parseMathTokens(bracketsOpnStr, statements));
+    nmbrLet(&bracketsCls, parseMathTokens(bracketsClsStr, statements));
+  }
+  long brackets = nmbrLen(bracketsOpn);
+  for(int i = 0;i<brackets; i++) {
+    long open = bracketsOpn[i];
+    long close = bracketsCls[i];
+    long pairingMismatches = 0; /* Counter of parens: + for "(" and - for ")" */
+    for(int j=0; j<len; j++) {
+      if(str[start-1+j] == open) pairingMismatches ++;
+      if(str[start-1+j] == close) pairingMismatches --;
+    }
+    if(pairingMismatches != 0) {
+      if(dbs7) print2("Bracket mismatch for %s%s in %s (mismatch=%ld)\n",
+		      mathToken[open].tokenName,
+		      mathToken[close].tokenName,
+		      nmbrCvtMToVString(nmbrMid(str, start, len)),
+		      pairingMismatches);
+      return 0;
+    }
+  }
+  return 1;
+}
+
+/* Buffer the anchors for the variables - this trades a bit of static memory for a bit of processing speed */
+vstring getAnchor(long tokenId) {
+  vstring anchor = stsVar[tokenId].anchor;
+  if(strlen(anchor) == 0 ) {
+    let(&anchor, cat("#", mathToken[tokenId].tokenName, "#", NULL));
+    stsVar[tokenId].anchor = anchor;
+  }
+  return anchor;
+}
+
+/* Attempts to unify the given mathString (taken as constant) with the
+ * scheme (expected to contain variables).
+ * varToken, varStart, varLen and state are assumed to be preallocated
+ * with enough space for all variables (stsScheme[i].varCount).
+ * If the unification is successful,
+ * - varPos will contain an array with the position of each variable in the scheme
+ * - varStart will contain an array with the start of each variable substitution within mathString
+ * - varLen will contain an array with the length of each variable substitution within mathString
+ * - state will contain an array of (number of variables - 1) elements with the indices of the next substitution, if any.
+ * Return value:
+ * - 0 if the unification fails,
+ * - 1 if the unification is successful and there are no more possible unifications
+ * - 3 if the unification is successful and there are possibly more unifcations
+ */
+/* Note that variables must be assigned at least one token. */
+flag unifySts(nmbrString *mathString, nmbrString *scheme, nmbrString *varPos, nmbrString *varStart, nmbrString *varLen, nmbrString *state) {
+  int varCount = 0;
+  int lastVarNextOcc = -1; /* The last variable with a next possible occurrence, to prepare the next state */
+  long lenString = nmbrLen(mathString);
+  long lenScheme = nmbrLen(scheme);
+  flag balanced; /* Whether or not the last substitution found was bracket-balanced */
+
+  /* Pruning : skip if shorter than scheme */
+  if(lenString < lenScheme) return 0;
+
+  /* Count the number of variables in the scheme, and note their positions */
+  for(int i=0;i<lenScheme;i++)
+    if(mathToken[scheme[i]].tokenType == var_)
+      varPos[varCount++] = i+1;
+  if(varCount > STS_MAX_SCHEME_VAR) bug(5003);
+
+  /* Repeat until we found a bracket-balanced variable substitution */
+  do {
+    lastVarNextOcc = -1;
+    /* Handle separately the trivial cases where there are no or one variable. */
+    switch(varCount) {
+      case 0:
+	/* No variable : match the two strings */
+	return nmbrEq(scheme, mathString);
+
+//      case 1:
+//	/* One variable: match the start and end, assign the rest */
+//	varStart[0] = varPos[0];
+//	varLen[0] = lenString - lenScheme + 1;
+//	if(!nmbrSubEq(scheme, 1, mathString, 1, varStart[0]-1)) return 0;
+//	if(!nmbrSubEq(scheme, varPos[0]+1, mathString, varPos[0] + varLen[0], lenScheme - varPos[0])) return 0;
+//	if(dbs7) print2("Found unification for %s : %s (start=%ld, len=%ld)\n",mathToken[scheme[varPos[0]-1]].tokenName, nmbrCvtMToVString(nmbrMid(mathString, varStart[0], varLen[0])), varStart[0], varLen[0]);
+//	return 1;
+
+      default:
+	/* Two variables or more: first match the prefix and the suffix */
+	varStart[0] = varPos[0];
+	if(!nmbrSubEq(scheme, 1, mathString, 1, varStart[0]-1)) return 0;
+	if(!nmbrSubEq(scheme, varPos[varCount-1]+1, mathString, lenString - (lenScheme - varPos[varCount-1] - 1), lenScheme - varPos[varCount-1])) return 0;
+
+	/* Then, for each additional variable, */
+	for(int i=0;i<varCount-1;i++) {
+	  if(state[i] < 1) state[i] = 1;
+	  long conLength = varPos[i+1]-varPos[i]-1;
+	  if(dbs9) print2("Searching %ld's occurrence of %s in %s starting from %ld\n", state[i], nmbrCvtMToVString(nmbrMid(scheme, varPos[i]+1, conLength)), nmbrCvtMToVString(mathString), varStart[i]+1);
+	  long position = nmbrInstrN(varStart[i]+1, state[i], mathString, scheme, varPos[i]+1, conLength);
+	  if(dbs9) print2("Found pos %ld\n", position);
+	  if(position == 0) return 0;
+	  // note if there is a next occurrence
+	  if(nmbrInstrN(varStart[i]+1, state[i]+1, mathString, scheme, varPos[i]+1, conLength) > 0)
+	    lastVarNextOcc = i;
+	  varLen[i] = position - varStart[i];
+	  varStart[i+1] = position + conLength;
+	}
+	varLen[varCount-1] = lenString - (lenScheme - varPos[varCount-1]) - varStart[varCount-1] + 1;
+	if(dbs7) for(int i=0;i<varCount;i++) print2("Found unification for %s : %s (start=%ld, len=%ld)\n",mathToken[scheme[varPos[i]-1]].tokenName, nmbrCvtMToVString(nmbrMid(mathString, varStart[i], varLen[i])), varStart[i], varLen[i]);
+	break;
+    }
+
+    /* Check that brackets are balanced in all substitutions */
+    balanced = 1;
+    for(int i = 0; i<varCount; i++)
+      balanced &= nmbrBalanced(mathString, varStart[i], varLen[i]);
+
+    /* Compute next state */
+    if(lastVarNextOcc >= 0) {
+      state[lastVarNextOcc]++;
+      for(int i=lastVarNextOcc+1;i<varCount-1;i++)
+        state[i] = 1;
+        if(dbs7) print2("Next state is %s\n",nmbrCvtAnyToVString(state));
+    }
+  }
+  while(lastVarNextOcc >= 0 && !balanced);
+  if(!balanced) return 0; /* Failure, no substitution found was balanced */
+  if(lastVarNextOcc >= 0) return 3; /* Success, with other possible substitutions */
+  return 1; /* Success */
+}
+
+
+/* Builds a structured typesetting output, for the math string (hypothesis or
+   conclusion) that is passed in.
+   Returns 1 if successful, 0 otherwise. */
+/* Warning: The caller must deallocate the returned vstring. */
+flag getSTSLongMathRec(vstring *mmlLine, nmbrString *mathString, long statemNum, int recursionLevel) {
+  flag result = 0;
+  flag success = 0;
+  long stsIndex = 0;
+  long lenString = nmbrLen(mathString);
+  if(dbs3) print2("%sPrinting \"%s\"!\n", space(recursionLevel), nmbrCvtMToVString(mathString));
+  static flag recursionError = 0;
+
+  if(recursionLevel > STS_MAX_RECURSION) {
+    print2("Maximum recursion level reached when printing %s!\n", nmbrCvtMToVString(mathString));
+    print2("Check your MMTS rules for possible circular references.\n");
+    recursionError = 1;
+    return 0;
+  }
+
+  // Pruning - if matching a single token (type + token), simply look it up.
+  if(lenString == 2 && mathToken[mathString[1]].tokenType == con_) {
+    stsIndex = stsVar[mathString[1]].stsSchemeId;
+    if(stsIndex == 0) {
+      //print2("Did not find token for %s.\n", nmbrCvtMToVString(mathString));
+      return 0;
+    }
+    if(nmbrEq(stsScheme[stsIndex - 1].scheme, mathString)) {
+	let(mmlLine, stsScheme[stsIndex - 1].typesetting);
+	return 1;
+    }
+  }
+
+  // Caching - try to retrieve result from cache
+  if(stsUseCache && lenString < STS_MAX_LEN_FOR_CACHE) {
+    let(mmlLine, htget(&stsCache, mathString));
+    if(strlen(*mmlLine)) {
+      return 1;
+    }
+  }
+
+  for(stsIndex = 0;(result == 0 || success == 0) && stsIndex < stsSchemes;stsIndex++) {
+    if(dbs5) let(mmlLine, ""); // this frees the temp alloc...
+
+    /* Pruning - check the type token */
+    if(stsScheme[stsIndex].scheme[0] != mathString[0]) continue;
+
+    /* Pruning : skip if shorter than scheme */
+    if(lenString < nmbrLen(stsScheme[stsIndex].scheme)) continue;
+
+    /* Identifier schemes must be fully matched, and there is no substitution */
+    if(stsScheme[stsIndex].type == 'i') {
+      if(nmbrEq(stsScheme[stsIndex].scheme, mathString)) {
+	let(mmlLine, stsScheme[stsIndex].typesetting);
+	return 1;
+      } else continue;
+    }
+
+    /* This case was handled above - skip it here */
+    if(nmbrLen(stsScheme[stsIndex].scheme) == 2
+	&& mathToken[stsScheme[stsIndex].scheme[1]].tokenType == con_) {
+      continue;
+    }
+
+    /* Since the number of variables in substitution schemes is very limited
+     * (at most 3 in current state), we're allocating the different arrays
+     * needed for unification fixed length, on the stack.
+     * Adding pool format only for easier printing.
+     */
+    nmbrString stateVectorV[STS_MAX_SCHEME_VAR+4];
+    nmbrString varPosV[STS_MAX_SCHEME_VAR+4];
+    nmbrString varStartV[STS_MAX_SCHEME_VAR+4];
+    nmbrString varLenV[STS_MAX_SCHEME_VAR+4];
+    nmbrString *stateVector = stateVectorV+3, *varPos = varPosV+3, *varStart = varStartV+3, *varLen=varLenV+3;
+
+    long varCount = stsScheme[stsIndex].varCount;
+    result = 3;
+    success = 0;
+
+    /* Initialize the state vector : first look for the first occurrences */
+    for(int i=0;i<varCount-1;i++) stateVector[i] = 1;
+    stateVector[varCount-1] = -1;
+    stateVector[-1] = sizeof(long) * (varCount-1+1);
+    stateVector[-2] = sizeof(long) * (varCount-1+1);
+
+    /* As long as there is a unification, but no next level substitution */
+    while((3 == result) && !success) {
+      /* Launch unification (Neither unify() nor assignVar() actually match our need. Wrote our own unification) */
+      if(dbs5) print2("%sTrying unification of \"%s\" and \"%s\" (state:<%s>)\n",
+		     space(recursionLevel),
+		     nmbrCvtMToVString(mathString),
+		     nmbrCvtMToVString(stsScheme[stsIndex].scheme),
+		     nmbrCvtAnyToVString(stateVector));
+      result = unifySts(mathString, stsScheme[stsIndex].scheme, varPos, varStart, varLen, stateVector);
+      if(dbs5) print2("%sResult is %d\n", space(recursionLevel), result);
+      if(result == 3 && dbs3) print2("Unification for %s is not unique!\n", nmbrCvtMToVString(mathString));
+      if(result != 0) {
+	let(mmlLine, stsScheme[stsIndex].typesetting);
+
+	if(dbs5) print2("%sFound match with %s\n", space(recursionLevel), nmbrCvtMToVString(stsScheme[stsIndex].scheme));
+	success = 1; /* Be optimistic an assume next level substitutions will succeed */
+	for(int i=0;i<varCount && success;i++) {
+	  long varToken = stsScheme[stsIndex].scheme[varPos[i]-1];
+	  if(dbs5) print2("%sVariable %d : %s , from %ld len %ld (%s)\n", space(recursionLevel), i, mathToken[varToken].tokenName, varStart[i], varLen[i], mathToken[stsVar[varToken].stsType].tokenName);
+
+	  /* Build the new math string */
+	  nmbrString *newMathString = NULL_NMBRSTRING;
+	  nmbrLet(&newMathString, nmbrUnshiftElement(
+	      nmbrMid(mathString, varStart[i], varLen[i]),
+	      stsVar[varToken].stsType));
+	  if(dbs5) print2("%sSubstitution : %s\n", space(recursionLevel), nmbrCvtMToVString(newMathString));
+
+	  /* Try unification - recursively */
+	  vstring substitution = "";
+	  success &= getSTSLongMathRec(&substitution, newMathString, statemNum, recursionLevel+1);
+
+	  /* deallocate new math string */
+	  nmbrLet(&newMathString, NULL_NMBRSTRING);
+
+	  if(success) {
+	    vstring anchor = getAnchor(varToken);
+	    long pos = instr(1, *mmlLine, anchor);
+	    while(pos != 0) {
+	      long end = pos + len(anchor);
+	      let(mmlLine, cat(left(*mmlLine, pos-1), substitution, mid(*mmlLine, end, len(*mmlLine)-end+1), NULL));
+	      pos = instr(pos + len(substitution), *mmlLine, anchor);
+	    }
+	  } /* end of if block on next substitution success */
+	  /* Deallocate local strings */
+	  let(&substitution, "");
+	  if(!success && recursionError) {
+	    //print2("When unifying %s with scheme %s (token type %s)\n", nmbrCvtMToVString(mathString), nmbrCvtMToVString(stsScheme[stsIndex].scheme), mathToken[stsVar[varToken].stsType].tokenName);
+	    return 0;
+	  }
+	} /* end of for loop on variable substitutions */
+      } /* end of if block on unification success */
+      /* Stop if all next level substitutions succeeded */
+      if(success) break;
+    } /* end of while loop on unifications */
+    /* Stop at the first successful unification */
+    if(success) break;
+  } /* end of for loop on  schemes */
+
+  /* Caching - store result if successful */
+  if(stsUseCache && success && (lenString > 2 || mathToken[mathString[1]].tokenType != con_) && lenString < STS_MAX_LEN_FOR_CACHE) {
+    htput(&stsCache, mathString, *mmlLine);
+  }
+
+  if(result == 0 || success == 0) {
+    /* failure */
+    if(dbs5 || dbs3) print2("%sNo unification found for %s\n", space(recursionLevel), nmbrCvtMToVString(mathString));
+    return 0;
+  } else {
+    /* success */
+    if(dbs5 || dbs3) print2("%sApplied scheme %s for %s, result is %s\n", space(recursionLevel), nmbrCvtMToVString(stsScheme[stsIndex].scheme), nmbrCvtMToVString(mathString), *mmlLine);
+    return 1;
+  }
+}
+
+int zzz=0;
+/* Returns a structured typesetting output, for the math string (hypothesis or
+   conclusion) that is passed in. */
+/* Warning: The caller must deallocate the returned vstring. */
+flag getSTSLongMath(vstring *mmlLine, nmbrString *mathString, flag displayed, long statemNum, flag textwarn) {
+  if(dbs1 || dbs3 || dbs5) outputToString = 0;
+  if(dbs1) print2("Printing \"%s\"!\n", nmbrCvtMToVString(mathString));
+  /* Call the recursive function - here we don't care about the return value. */
+  flag success = getSTSLongMathRec(mmlLine, mathString, statemNum, 0);
+  outputToString = 1;
+
+  if(!success) {
+//    // Try again with traces on
+//    outputToString = 0;
+//    debugOn();
+//    getSTSLongMathRec(mmlLine, mathString, statemNum, 0);
+//    debugOff();
+
+    /* Return a generic error message */
+    if(textwarn)
+      let(mmlLine, cat("No typesetting for: ",
+			nmbrCvtMToVString(mathString),NULL));
+    else
+      let(mmlLine, cat("No typesetting for: <code>",
+			nmbrCvtMToVString(mathString),"</code>",NULL));
+  }
+  else {
+    /* Add the HTML container */
+    vstring *xfix;
+    if(displayed) xfix = stsDisplayed; else xfix = stsInText;
+    let(mmlLine, cat(xfix[0], *mmlLine, xfix[1], NULL));
+  }
+
+  if(stsUseCache) {
+    outputToString = 0;
+    htstats(&stsCache);
+    if(++zzz%100==0)htdump(&stsCache);
+    outputToString = 1;
+  }
+  return success;
+}
+
+
+/* Returns the code to be included in the HTML head element
+ * for the given format */
+vstring getSTSHeader() {
+  return stsHeader;
+}
+
+/* Go through all non-definition axioms,
+ * and check whether there is a corresponding STS scheme.
+ * Prints a warning message for each missing declaration */
+void verifySts(vstring format) {
+  vstring texLine = "";
+  int warnCount = 0;
+  int checks = 0;
+
+  print2("Verifying axioms have %s STS schemes...\n", format);
+  if(strcmp(stsFormat, format)) {
+    if(!parsetSTSRules(format)) {
+      print2("?Aborting verify.\n");
+      return;
+    }
+  }
+
+  for(int statemNum=0;statemNum<statements;statemNum++) {
+    /* Skip non-axioms and definitions */
+    if(statement[statemNum].type != (char)a_) continue;
+    if(strncmp(statement[statemNum].labelName,"df-",3) == 0) continue;
+    if(strncmp(statement[statemNum].labelName,"ax-",3) == 0) continue;
+
+    flag success = getSTSLongMath(&texLine, statement[statemNum].mathString, 1, statemNum, 1);
+    outputToString = 0;
+    if(!success) {
+      print2("?Warning: %s\n", texLine);
+      warnCount++;
+    }
+    /* Get rid of the texLine */
+    let(&texLine, "");
+    checks++;
+  }
+
+  print2("%ld syntax axioms were checked.\n", checks);
+  if (!warnCount) {
+    print2("No warnings were found.\n");
+  } else {
+    if (warnCount == 1) {
+      print2("One warning was found.\n");
+    } else {
+      print2("%ld warnings were found.\n", (long)warnCount);
+    }
+  }
+}
+
+
+/* Returns the token ID for a given token */
+long tokenId(vstring token) {
+  void *mathKeyPtr; /* For binary search */
+  mathKeyPtr = (void *)bsearch(token, mathKey, (size_t)mathTokens,
+      sizeof(long), mathSrchCmp);
+  if (!mathKeyPtr) return -1;
+  return *((long *)mathKeyPtr);
+}
+
+/* Returns the HTML code string for a given token.
+ * With STS, we normally don't map isolated tokens, but full constructs.
+ * So this requires specific schemes to be added for single tokens when it
+ * is not defined as a variable or constant (e.g. for ' ( ' or ' -> ' )
+ * If it is not the case, this function will fall back to displaying the
+ * token in ASCII */
+/* *** Note: The caller must deallocate the returned string */
+vstring stsToken(long tokenId, long stateNum) {
+  vstring str2 = "";
+  if(stsVar == NULL) {
+    print2("Error: STS has not been initialized.");
+    exit(-1);
+  }
+
+  // Expect to find
+  long schemeId = stsVar[tokenId].stsSchemeId;
+  //printf("Printing token %s, schemeId = %ld\n", mathToken[tokenId].tokenName, schemeId);
+  //if(schemeId == 0)
+  //  printf("Var not found : %s\n", mathToken[tokenId].tokenName);
+  if(schemeId >= 1 && schemeId <= stsSchemes && stsVar[stsScheme[schemeId - 1].scheme[0]].isTerminal) {
+    /* If there is a single token scheme, build the token from the scheme itself. */
+    getSTSLongMath(&str2, stsScheme[schemeId - 1].scheme, 0, 0, 0);
+  }
+  else {
+    /* Otherwise fallback to metamath token in case token unavailable */
+    let(&str2, cat("<code style=\"color:red;\">",mathToken[tokenId].tokenName,"</code>", NULL));
+  }
+  return str2;
+}
+
+/*
+ * Converts a string of ASCII text using STS.
+ * This is used for comment sections in math mode.
+ * Each math token MUST be separated by white space.
+ */
+vstring asciiToMathSts(vstring text, long statemNum) {
+  vstring mmlLine = "";
+  nmbrString *orgString = NULL_NMBRSTRING;
+  nmbrString *mathString = NULL_NMBRSTRING;
+  flag result = 0;
+
+//  outputToString = 0;
+//  print2("Going to try %ld types!\n", stsTypes);
+//  dbs5=1;
+  /* 20-Jan-2019 tar - use "statements" as stateNum, since all tokens are valid. */
+  nmbrLet(&orgString, parseMathTokens(text, statements));
+  for(int i=0;!result && i<nmbrLen(stsTerminalTypes);i++) {
+    nmbrLet(&mathString, nmbrUnshiftElement(orgString, stsTerminalTypes[i])); // was 39
+    outputToString = 0;
+//    print2("Trying to print \"%s\"!\n", nmbrCvtMToVString(mathString));
+    result = getSTSLongMath(&mmlLine, mathString, 0, statemNum, 1);
+  }
+  if(!result) {
+    // In case we don't manage to parse the math string, we shall
+    // revert to token-by-token conversion.
+    let(&mmlLine, asciiMathToTexNoSts(text, statemNum));
+  }
+  nmbrLet(&mathString, NULL_NMBRSTRING);
+  nmbrLet(&orgString, NULL_NMBRSTRING);
+  return mmlLine;
+}
+
+
+//  print2("<style type=\"text/css\">\n");
+//  print2(".MathJax_SVG_Display { margin: .2em 0em !important }\n");
+//  print2(".MathJax_SVG_Display { float: left; width: inherit !important; }\n");
+//  print2(".i { float: left; }\n");
+//  print2(".hyp th,.stmt th,.proof th { border: 1px solid #CCC; }\n");
+//  print2(".hyp td,.stmt td,.proof td { border: 1px solid #CCC; }\n");
+//  print2(".proof tr:nth-child(even) { background-color: #F8FFFC; }\n");
+//  print2(".hyp tr:nth-child(even) { background-color: #F8FFFC; }\n");
+//  print2("tr.hant { background-color: #D0F0FF !important; }\n");
+//  print2("tr.hstmt { background-color: #C0D0FF !important; }\n");
+//  print2("tr.hdep { background-color: #F0F0FF !important; }\n");
+//  print2("</style>\n");
+//
+//  /* Highlight antecedents when hovering above a proof.*/
+//  print2("<script src=\"http://ajax.googleapis.com/ajax/libs/jquery/1.8.2/jquery.js\" type=\"text/javascript\"></script>\n");
+//  print2("<script src=\"../hant.js\" type=\"text/javascript\"></script>\n");
+//
+//  /* This can be used to control the display of the MathJax content.
+//   * Like alignment, line breaks, etc. */
+//  print2("<script type=\"text/x-mathjax-config\">\n");
+//  print2("MathJax.Hub.Config({\n");
+////      print2("  jax: [\"input/MathML\",\"output/SVG\"],\n");
+////      print2("  extensions: [\"mml2jax.js\"],\n");
+////      print2("  \"fast-preview\": { disabled: true },\n");
+//  print2("  SVG: { linebreaks: { width: \"container\", automatic: true }"
+////	  ", styles:{\".MathJax_Display\": { \"float\": \"left\" } }"
+//	  "}\n");
+//  print2("});</script>\n");
+//  print2("<script type=\"text/javascript\" src=\n");
+//  print2("\"https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/\n");
+//  print2("MathJax.js?config=MML_CHTML\"></script>\n");
+//  print2("<script type=\"text/javascript\" src=\"../mmmathml.js\"></script>\n");
+//  /*
+//  print2("<script type=\"text/x-mathjax-config;executed=true\">\n");
+//  print2("MathJax.Hub.Config({SVG:{styles:{\".MathJax_Display\": {\n");
+//  print2("\"float\": \"left\"\n");
+//  print2("}}}});</script>\n");
+//  */
+//  /*
+//  print2("<script type=\"text/x-mathjax-config;executed=true\">\n");
+//  print2("MathJax.Hub.Config({SVG:{styles:{\".MathJax_Display\": {\n");
+//  print2("\"float\": \"left\"\n");
+//  print2("}}}});</script>\n");
+//  */
diff --git a/mmwsts.h b/mmwsts.h
new file mode 100644
index 00000000..2f295f76
--- /dev/null
+++ b/mmwsts.h
@@ -0,0 +1,38 @@
+/*****************************************************************************/
+/*        Copyright (C) 2016  NORMAN MEGILL  nm at alum.mit.edu              */
+/*            License terms:  GNU General Public License                     */
+/*****************************************************************************/
+/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
+
+#ifndef METAMATH_MMVMML_H_
+#define METAMATH_MMVMML_H_
+
+#include "mmvstr.h"
+#include "mmdata.h"
+
+/* Parse an STS file */
+int parsetSTSRules(vstring format);
+
+/* Returns the HTML code for MathML, for the math string (hypothesis or
+   conclusion) that is passed in. */
+/* Warning: The caller must deallocate the returned vstring. */
+flag getSTSLongMath(vstring *mmlLine, nmbrString *mathString, flag displayed,
+		    long statemNum, flag textwarn);
+
+/* Returns the code to be included in the HTML head element
+ * for the given format */
+vstring getSTSHeader();
+
+/* Returns the token ID for a given token */
+long tokenId(vstring token);
+
+/* Returns the HTML code string  */
+vstring stsToken(long tokenId, long stateNum);
+
+/* Converts a string of ASCII text using STS. */
+vstring asciiToMathSts(vstring string, long statemNum);
+
+/* Check that there is an STS scheme for each syntax axiom. */
+void verifySts(vstring format);
+
+#endif /* METAMATH_MMVMML_H_ */
diff --git a/mmwtex.c b/mmwtex.c
index 843b56e3..bf5f346b 100644
--- a/mmwtex.c
+++ b/mmwtex.c
@@ -19,6 +19,7 @@
 #include "mmpars.h" /* For rawSourceError and mathSrchCmp and lookupLabel */
 #include "mmwtex.h"
 #include "mmcmdl.h" /* For texFileName */
+#include "mmwsts.h" /* For MathML/STS */
 
 /* 6/27/99 - Now, all LaTeX and HTML definitions are taken from the source
    file (read in the by READ... command).  In the source file, there should
@@ -32,6 +33,10 @@ flag htmlFlag = 0;  /* HTML flag: 0 = TeX, 1 = HTML */
 flag altHtmlFlag = 0;  /* Use "althtmldef" instead of "htmldef".  This is
     intended to allow the generation of pages with the Unicode font
     instead of the individual GIF files. */
+/* 19-Jul-2017 tar Added for STS/MathML output */
+flag stsFlag = 0; /* STS output (for "structural typesetting") */
+vstring stsOutput = ""; /* output mode chosen for STS (follows STS flag) */
+vstring postProcess = ""; /* command to pipe the output into (used for MathJax prerendering) */
 flag briefHtmlFlag = 0;  /* Output statement lists only, for statement display
                 in other HTML pages, such as the Proof Explorer home page */
 long extHtmlStmt = 0; /* At this statement and above, use the exthtmlxxx
@@ -706,7 +711,8 @@ flag readTexDefs(
 
   /* 26-Jun-2011 nm Added this check */
   /* Check to make sure all GIFs are present */
-  if (htmlFlag) {
+  if (htmlFlag
+      && !stsFlag) { /* 22-Mar-2018 Added for STS */
     for (i = 0; i < numSymbs; i++) {
       tmpPtr = texDefs[i].texEquiv;
       k = 0;
@@ -1185,6 +1191,18 @@ vstring tokenToTex(vstring mtoken, long statemNum /*for error msgs*/)
 /* Converts a comment section in math mode to TeX.  Each math token
    MUST be separated by white space.   TeX "$" does not surround the output. */
 vstring asciiMathToTex(vstring mathComment, long statemNum)
+{
+  /* 29-Sep-2017 Thierry Arnoux added for STS */
+  if(stsFlag) {
+    return asciiToMathSts(mathComment, statemNum);
+  } else {
+    return asciiMathToTexNoSts(mathComment, statemNum);
+  }
+}
+
+/* Converts a comment section in math mode to TeX.  Each math token
+   MUST be separated by white space.   TeX "$" does not surround the output. */
+vstring asciiMathToTexNoSts(vstring mathComment, long statemNum)
 {
 
   vstring tex;
@@ -1209,7 +1227,9 @@ vstring asciiMathToTex(vstring mathComment, long statemNum)
     let(&token, space(i));
     memcpy(token, srcptr, (size_t)i);
     srcptr = srcptr + i;
-    tex = tokenToTex(token, statemNum); /* Convert token to TeX */
+    /* 27 Jul 2017 tar For MathML/STS */
+    if(stsFlag) tex = stsToken(tokenId(token), statemNum);
+    else tex = tokenToTex(token, statemNum); /* Convert token to TeX */
               /* tokenToTex allocates tex; we must deallocate it */
 
     if (!htmlFlag) {
@@ -1553,6 +1573,9 @@ void printTexHeader(flag texHeaderFlag)
           "</TITLE>", NULL));
     }
     */
+    /* 7-Jul-17 tar - Added for MathML/STS */
+    if(stsFlag) printLongLine(getSTSHeader(), "", "\n");
+
     /* 4-Jun-06 nm - Put theorem name before "Metamath Proof Explorer" etc. */
     if (showStatement < extHtmlStmt) {
       print2("%s\n", cat("<TITLE>",
@@ -5934,6 +5957,12 @@ vstring getTexLongMath(nmbrString *mathString, long statemNum)
   vstring lastTex = "";
   flag alphnew, alphold, unknownnew, unknownold;
 
+  /* 7-Jul-2017 added for STS (Structured Typesetting) */
+  if(stsFlag) {
+    getSTSLongMath(&texLine, mathString, 1, statemNum, 0);
+    return texLine;
+  }
+
   if (!texDefsRead) bug(2322); /* TeX defs were not read */
   let(&texLine, "");
 
@@ -6151,7 +6180,8 @@ vstring getTexOrHtmlHypAndAssertion(long statemNum)
                  "\\quad\\&\\quad "
               ,NULL));
         } else {
-          if (altHtmlFlag) {
+          if (altHtmlFlag
+        	  || stsFlag) { /* 22-Mar-2018 Added for STS */
             /* Hard-coded for set.mm! */
             let(&texOrHtmlCode, cat(texOrHtmlCode,
                 /* 8/8/03 - Changed from Symbol to Unicode */
@@ -6183,7 +6213,8 @@ vstring getTexOrHtmlHypAndAssertion(long statemNum)
                  "\\quad\\Rightarrow\\quad "
           ,NULL));
     } else {
-      if (altHtmlFlag) {
+      if (altHtmlFlag
+      	  || stsFlag) { /* 22-Mar-2018 Added for STS */
         /* Hard-coded for set.mm! */
         let(&texOrHtmlCode, cat(texOrHtmlCode,
             /* 8/8/03 - Changed from Symbol to Unicode */
diff --git a/mmwtex.h b/mmwtex.h
index 75007db9..60ed9060 100644
--- a/mmwtex.h
+++ b/mmwtex.h
@@ -29,6 +29,10 @@ extern flag htmlFlag;  /* HTML flag: 0 = TeX, 1 = HTML */
 extern flag altHtmlFlag;  /* Use "althtmldef" instead of "htmldef".  This is
     intended to allow the generation of pages with the old Symbol font
     instead of the individual GIF files. */
+/* 19-Jul-2017 tar Added for STS/MathML output */
+extern flag stsFlag; /* STS output (for "structural typesetting") */
+extern vstring stsOutput; /* output mode chosen for STS (follows STS flag) */
+extern vstring postProcess; /* command to pipe the output into (used for MathJax prerendering) */
 extern flag briefHtmlFlag;  /* Output statement only, for statement display
                 in other HTML pages, such as the Proof Explorer home page */
 extern long extHtmlStmt; /* At this statement and above, use the exthtmlxxx
@@ -81,6 +85,7 @@ vstring tokenToTex(vstring mtoken, long statemNum);
 /* Converts a comment section in math mode to TeX.  Each math token
    MUST be separated by white space.   TeX "$" does not surround the output. */
 vstring asciiMathToTex(vstring mathComment, long statemNum);
+vstring asciiMathToTexNoSts(vstring mathComment, long statemNum);
 /* Gets the next section of a comment that is in the current mode (text,
    label, or math).  If 1st char. is not "$", text mode is assumed.
    mode = 0 means end of comment reached.  srcptr is left at 1st char.

From eedc22ff87aad59f3c5434195b536f9c56991ac5 Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <thierry.arnoux@gmx.net>
Date: Fri, 24 Dec 2021 15:21:40 +0800
Subject: [PATCH 2/9] Rename global variables (to adapt to change 0.187
 15-Aug-2020)

---
 mmwsts.c | 120 +++++++++++++++++++++++++++----------------------------
 1 file changed, 60 insertions(+), 60 deletions(-)

diff --git a/mmwsts.c b/mmwsts.c
index 920dcdde..40e0698e 100644
--- a/mmwsts.c
+++ b/mmwsts.c
@@ -19,7 +19,7 @@
 #include "mmpars.h" /* For rawSourceError and mathSrchCmp and lookupLabel */
 #include "mmcmdl.h" /* For texFileName */
 #include "mmwsts.h"
-#include "mmwtex.h" /* For texDefsRead */
+#include "mmwtex.h" /* For g_texDefsRead */
 #include "mmhtbl.h" /* For caching results */
 
 #define STS_MAX_TYPES 10		/* basic types. For set.mm, there are 4 (|-,wff,class,set) */
@@ -118,16 +118,16 @@ hashtable stsCache;
 int mathSrchGlbCmp(const void *key, const void *data)
 {
   /* Returns -1 if key < data, 1 if key > data */
-  int ret = strcmp(key, mathToken[ *((long *)data) ].tokenName);
+  int ret = strcmp(key, g_MathToken[ *((long *)data) ].tokenName);
   if(ret != 0) return ret;
 
   /* We have found two identical entries.
    * However we shall return 0 (match) only if the token is global. */
-  if(mathToken[ *((long *)data) ].endStatement == statements) return 0;
+  if(g_MathToken[ *((long *)data) ].endStatement == g_statements) return 0;
 
   /* Find the direction in which the target token is */
-  for(long *ptr = (long*)data; !strcmp(key, mathToken[ *ptr ].tokenName); ptr++)
-    if(mathToken[ *ptr ].endStatement == statements) return 1;
+  for(long *ptr = (long*)data; !strcmp(key, g_MathToken[ *ptr ].tokenName); ptr++)
+    if(g_MathToken[ *ptr ].endStatement == g_statements) return 1;
   return -1;
 }
 
@@ -147,10 +147,10 @@ nmbrString *parseMathStrict(vstring text)
   long i;
   char *fbPtr;
   long textLen, tokenLen_;
-  long *mathKeyPtr; /* bsearch returned value */
+  long *g_mathKeyPtr; /* bsearch returned value */
 
-  /* Make sure that mathTokens has been initialized */
-  if (!mathTokens) bug(1717);
+  /* Make sure that g_mathTokens has been initialized */
+  if (!g_mathTokens) bug(1717);
 
   textLen = (long)strlen(text);
 
@@ -169,15 +169,15 @@ nmbrString *parseMathStrict(vstring text)
 
     fbPtr[tokenLen_] = 0; /* End token - There's no come back */
     //printf("Searching for %s\n", fbPtr);
-    mathKeyPtr = (long *)bsearch(fbPtr, mathKey,
-	(size_t)mathTokens, sizeof(long), mathSrchGlbCmp);
-    if (!mathKeyPtr) {
+    g_mathKeyPtr = (long *)bsearch(fbPtr, g_mathKey,
+	(size_t)g_mathTokens, sizeof(long), mathSrchGlbCmp);
+    if (!g_mathKeyPtr) {
       /* Unknown token, escape. */
       print2("?Unknown token %s\n", fbPtr);
       free(wrkNmbrPtr);
       return NULL_NMBRSTRING;
     }
-    wrkNmbrPtr[mathStringLen] = *mathKeyPtr;
+    wrkNmbrPtr[mathStringLen] = *g_mathKeyPtr;
     mathStringLen++;
     fbPtr = fbPtr + tokenLen_ + 1; /* Move on to next token */
     if(fbPtr >= text + textLen) break;
@@ -218,8 +218,8 @@ int parsetSTSRules(vstring format) {
   vstring inputFn = "";
   vstring chunk = "";
   char chunkType = 0;
-  flag ots = outputToString;
-  outputToString = 0;
+  flag ots = g_outputToString;
+  g_outputToString = 0;
 
   /* If the same format was already parsed, nothing to do. */
   if(strcmp(stsFormat, format) == 0) {
@@ -236,8 +236,8 @@ int parsetSTSRules(vstring format) {
   }
 
   /* Build the name of the MMTS file to load */
-  let(&inputFn, cat(rootDirectory ,
-      left(input_fn, instr(1,input_fn,".mm")-1), "-", format, ".mmts", NULL));
+  let(&inputFn, cat(g_rootDirectory ,
+      left(g_input_fn, instr(1,g_input_fn,".mm")-1), "-", format, ".mmts", NULL));
 
   FILE *sts_fp = fSafeOpen(inputFn, "r", 1);
   if(!sts_fp) return 0; /* Error message is provided by fSafeOpen */
@@ -270,7 +270,7 @@ int parsetSTSRules(vstring format) {
   fileBuf[charCount] = 0; /* End of string */
 
   /* Initialize the STS Schemes list */
-  stsScheme = malloc((size_t)MAX_MATHTOKENS * sizeof(struct stsScheme_struct));
+  stsScheme = malloc((size_t)g_MAX_MATHTOKENS * sizeof(struct stsScheme_struct));
   if (!stsScheme) {
     print2("*** FATAL ***  Could not allocate stsScheme space\n");
     bug(5001);
@@ -278,7 +278,7 @@ int parsetSTSRules(vstring format) {
   stsSchemes = 0;
 
   /* Initialize and clear the STS Variable list */
-  stsVar = calloc((size_t)MAX_MATHTOKENS, sizeof(struct stsVar_struct));
+  stsVar = calloc((size_t)g_MAX_MATHTOKENS, sizeof(struct stsVar_struct));
   if (!stsVar) {
     print2("*** FATAL ***  Could not allocate stsVar space\n");
     bug(5002);
@@ -409,7 +409,7 @@ int parsetSTSRules(vstring format) {
         stsScheme[stsSchemes].type = chunkType;
         stsScheme[stsSchemes].scheme = NULL_NMBRSTRING;
 	// parseMathTokens is too permissive. Wrote own token parser.
-        //nmbrLet(&(stsScheme[stsSchemes].scheme), parseMathTokens(text, statements));
+        //nmbrLet(&(stsScheme[stsSchemes].scheme), parseMathTokens(text, g_statements));
         nmbrLet(&(stsScheme[stsSchemes].scheme), parseMathStrict(text));
 
         int l = nmbrLen(stsScheme[stsSchemes].scheme);
@@ -431,7 +431,7 @@ int parsetSTSRules(vstring format) {
         /* Store the number of variables in the scheme (each shall be different)  */
         stsScheme[stsSchemes].varCount = 0;
         for(int i=0;i<l;i++)
-          if(mathToken[stsScheme[stsSchemes].scheme[i]].tokenType == var_)
+          if(g_MathToken[stsScheme[stsSchemes].scheme[i]].tokenType == var_)
             stsScheme[stsSchemes].varCount++;
 
         /* Store the variable "type" (wff, set or class for set.mm)  */
@@ -444,13 +444,13 @@ int parsetSTSRules(vstring format) {
           stsVar[index].stsSchemeId = stsSchemes + 1;
           stsVar[index].anchor = "";
 
-          if(mathToken[stsVar[index].stsType].tokenType != con_)
+          if(g_MathToken[stsVar[index].stsType].tokenType != con_)
             rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
                 "An identifier definition shall start with a constant.");
-          if(mathToken[index].tokenType != var_)
+          if(g_MathToken[index].tokenType != var_)
             rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
                 "An identifier definition shall end with a variable.");
-	    //print2("Token %s has type %s\n", mathToken[index].tokenName, mathToken[stsVar[index].stsType].tokenName);
+	    //print2("Token %s has type %s\n", g_MathToken[index].tokenName, g_MathToken[stsVar[index].stsType].tokenName);
         }
 
         startPtr = fbPtr + 1;
@@ -539,13 +539,13 @@ int parsetSTSRules(vstring format) {
   /* Format is invalid */
   let(&stsFormat, format);
 
-  if (!errorCount) {
+  if (!g_errorCount) {
     print2("No errors were found.\n");
   } else {
-    if (errorCount == 1) {
+    if (g_errorCount == 1) {
       print2("One error was found.\n");
     } else {
-      print2("%ld errors were found.\n", (long)errorCount);
+      print2("%ld errors were found.\n", (long)g_errorCount);
     }
   }
 
@@ -554,9 +554,9 @@ int parsetSTSRules(vstring format) {
   free(fileBuf);
 
   /* Return back to outputting in a string */
-  outputToString = ots;
+  g_outputToString = ots;
 
-  texDefsRead = 1;
+  g_texDefsRead = 1;
   return 1;
 }
 
@@ -570,8 +570,8 @@ flag nmbrBalanced(nmbrString *str, long start, long len) {
   /* TODO we could use the global bracketMatchOn to detect if we are in set.mm */
   /*if(!bracketMatchOn) return 1;*/
   if(bracketsOpn == NULL_NMBRSTRING) {
-    nmbrLet(&bracketsOpn, parseMathTokens(bracketsOpnStr, statements));
-    nmbrLet(&bracketsCls, parseMathTokens(bracketsClsStr, statements));
+    nmbrLet(&bracketsOpn, parseMathTokens(bracketsOpnStr, g_statements));
+    nmbrLet(&bracketsCls, parseMathTokens(bracketsClsStr, g_statements));
   }
   long brackets = nmbrLen(bracketsOpn);
   for(int i = 0;i<brackets; i++) {
@@ -584,8 +584,8 @@ flag nmbrBalanced(nmbrString *str, long start, long len) {
     }
     if(pairingMismatches != 0) {
       if(dbs7) print2("Bracket mismatch for %s%s in %s (mismatch=%ld)\n",
-		      mathToken[open].tokenName,
-		      mathToken[close].tokenName,
+		      g_MathToken[open].tokenName,
+		      g_MathToken[close].tokenName,
 		      nmbrCvtMToVString(nmbrMid(str, start, len)),
 		      pairingMismatches);
       return 0;
@@ -598,7 +598,7 @@ flag nmbrBalanced(nmbrString *str, long start, long len) {
 vstring getAnchor(long tokenId) {
   vstring anchor = stsVar[tokenId].anchor;
   if(strlen(anchor) == 0 ) {
-    let(&anchor, cat("#", mathToken[tokenId].tokenName, "#", NULL));
+    let(&anchor, cat("#", g_MathToken[tokenId].tokenName, "#", NULL));
     stsVar[tokenId].anchor = anchor;
   }
   return anchor;
@@ -631,7 +631,7 @@ flag unifySts(nmbrString *mathString, nmbrString *scheme, nmbrString *varPos, nm
 
   /* Count the number of variables in the scheme, and note their positions */
   for(int i=0;i<lenScheme;i++)
-    if(mathToken[scheme[i]].tokenType == var_)
+    if(g_MathToken[scheme[i]].tokenType == var_)
       varPos[varCount++] = i+1;
   if(varCount > STS_MAX_SCHEME_VAR) bug(5003);
 
@@ -650,7 +650,7 @@ flag unifySts(nmbrString *mathString, nmbrString *scheme, nmbrString *varPos, nm
 //	varLen[0] = lenString - lenScheme + 1;
 //	if(!nmbrSubEq(scheme, 1, mathString, 1, varStart[0]-1)) return 0;
 //	if(!nmbrSubEq(scheme, varPos[0]+1, mathString, varPos[0] + varLen[0], lenScheme - varPos[0])) return 0;
-//	if(dbs7) print2("Found unification for %s : %s (start=%ld, len=%ld)\n",mathToken[scheme[varPos[0]-1]].tokenName, nmbrCvtMToVString(nmbrMid(mathString, varStart[0], varLen[0])), varStart[0], varLen[0]);
+//	if(dbs7) print2("Found unification for %s : %s (start=%ld, len=%ld)\n",g_MathToken[scheme[varPos[0]-1]].tokenName, nmbrCvtMToVString(nmbrMid(mathString, varStart[0], varLen[0])), varStart[0], varLen[0]);
 //	return 1;
 
       default:
@@ -674,7 +674,7 @@ flag unifySts(nmbrString *mathString, nmbrString *scheme, nmbrString *varPos, nm
 	  varStart[i+1] = position + conLength;
 	}
 	varLen[varCount-1] = lenString - (lenScheme - varPos[varCount-1]) - varStart[varCount-1] + 1;
-	if(dbs7) for(int i=0;i<varCount;i++) print2("Found unification for %s : %s (start=%ld, len=%ld)\n",mathToken[scheme[varPos[i]-1]].tokenName, nmbrCvtMToVString(nmbrMid(mathString, varStart[i], varLen[i])), varStart[i], varLen[i]);
+	if(dbs7) for(int i=0;i<varCount;i++) print2("Found unification for %s : %s (start=%ld, len=%ld)\n",g_MathToken[scheme[varPos[i]-1]].tokenName, nmbrCvtMToVString(nmbrMid(mathString, varStart[i], varLen[i])), varStart[i], varLen[i]);
 	break;
     }
 
@@ -718,7 +718,7 @@ flag getSTSLongMathRec(vstring *mmlLine, nmbrString *mathString, long statemNum,
   }
 
   // Pruning - if matching a single token (type + token), simply look it up.
-  if(lenString == 2 && mathToken[mathString[1]].tokenType == con_) {
+  if(lenString == 2 && g_MathToken[mathString[1]].tokenType == con_) {
     stsIndex = stsVar[mathString[1]].stsSchemeId;
     if(stsIndex == 0) {
       //print2("Did not find token for %s.\n", nmbrCvtMToVString(mathString));
@@ -757,7 +757,7 @@ flag getSTSLongMathRec(vstring *mmlLine, nmbrString *mathString, long statemNum,
 
     /* This case was handled above - skip it here */
     if(nmbrLen(stsScheme[stsIndex].scheme) == 2
-	&& mathToken[stsScheme[stsIndex].scheme[1]].tokenType == con_) {
+	&& g_MathToken[stsScheme[stsIndex].scheme[1]].tokenType == con_) {
       continue;
     }
 
@@ -800,7 +800,7 @@ flag getSTSLongMathRec(vstring *mmlLine, nmbrString *mathString, long statemNum,
 	success = 1; /* Be optimistic an assume next level substitutions will succeed */
 	for(int i=0;i<varCount && success;i++) {
 	  long varToken = stsScheme[stsIndex].scheme[varPos[i]-1];
-	  if(dbs5) print2("%sVariable %d : %s , from %ld len %ld (%s)\n", space(recursionLevel), i, mathToken[varToken].tokenName, varStart[i], varLen[i], mathToken[stsVar[varToken].stsType].tokenName);
+	  if(dbs5) print2("%sVariable %d : %s , from %ld len %ld (%s)\n", space(recursionLevel), i, g_MathToken[varToken].tokenName, varStart[i], varLen[i], g_MathToken[stsVar[varToken].stsType].tokenName);
 
 	  /* Build the new math string */
 	  nmbrString *newMathString = NULL_NMBRSTRING;
@@ -828,7 +828,7 @@ flag getSTSLongMathRec(vstring *mmlLine, nmbrString *mathString, long statemNum,
 	  /* Deallocate local strings */
 	  let(&substitution, "");
 	  if(!success && recursionError) {
-	    //print2("When unifying %s with scheme %s (token type %s)\n", nmbrCvtMToVString(mathString), nmbrCvtMToVString(stsScheme[stsIndex].scheme), mathToken[stsVar[varToken].stsType].tokenName);
+	    //print2("When unifying %s with scheme %s (token type %s)\n", nmbrCvtMToVString(mathString), nmbrCvtMToVString(stsScheme[stsIndex].scheme), g_MathToken[stsVar[varToken].stsType].tokenName);
 	    return 0;
 	  }
 	} /* end of for loop on variable substitutions */
@@ -841,7 +841,7 @@ flag getSTSLongMathRec(vstring *mmlLine, nmbrString *mathString, long statemNum,
   } /* end of for loop on  schemes */
 
   /* Caching - store result if successful */
-  if(stsUseCache && success && (lenString > 2 || mathToken[mathString[1]].tokenType != con_) && lenString < STS_MAX_LEN_FOR_CACHE) {
+  if(stsUseCache && success && (lenString > 2 || g_MathToken[mathString[1]].tokenType != con_) && lenString < STS_MAX_LEN_FOR_CACHE) {
     htput(&stsCache, mathString, *mmlLine);
   }
 
@@ -861,15 +861,15 @@ int zzz=0;
    conclusion) that is passed in. */
 /* Warning: The caller must deallocate the returned vstring. */
 flag getSTSLongMath(vstring *mmlLine, nmbrString *mathString, flag displayed, long statemNum, flag textwarn) {
-  if(dbs1 || dbs3 || dbs5) outputToString = 0;
+  if(dbs1 || dbs3 || dbs5) g_outputToString = 0;
   if(dbs1) print2("Printing \"%s\"!\n", nmbrCvtMToVString(mathString));
   /* Call the recursive function - here we don't care about the return value. */
   flag success = getSTSLongMathRec(mmlLine, mathString, statemNum, 0);
-  outputToString = 1;
+  g_outputToString = 1;
 
   if(!success) {
 //    // Try again with traces on
-//    outputToString = 0;
+//    g_outputToString = 0;
 //    debugOn();
 //    getSTSLongMathRec(mmlLine, mathString, statemNum, 0);
 //    debugOff();
@@ -890,10 +890,10 @@ flag getSTSLongMath(vstring *mmlLine, nmbrString *mathString, flag displayed, lo
   }
 
   if(stsUseCache) {
-    outputToString = 0;
+    g_outputToString = 0;
     htstats(&stsCache);
     if(++zzz%100==0)htdump(&stsCache);
-    outputToString = 1;
+    g_outputToString = 1;
   }
   return success;
 }
@@ -921,14 +921,14 @@ void verifySts(vstring format) {
     }
   }
 
-  for(int statemNum=0;statemNum<statements;statemNum++) {
+  for(int statemNum=0;statemNum<g_statements;statemNum++) {
     /* Skip non-axioms and definitions */
-    if(statement[statemNum].type != (char)a_) continue;
-    if(strncmp(statement[statemNum].labelName,"df-",3) == 0) continue;
-    if(strncmp(statement[statemNum].labelName,"ax-",3) == 0) continue;
+    if(g_Statement[statemNum].type != (char)a_) continue;
+    if(strncmp(g_Statement[statemNum].labelName,"df-",3) == 0) continue;
+    if(strncmp(g_Statement[statemNum].labelName,"ax-",3) == 0) continue;
 
-    flag success = getSTSLongMath(&texLine, statement[statemNum].mathString, 1, statemNum, 1);
-    outputToString = 0;
+    flag success = getSTSLongMath(&texLine, g_Statement[statemNum].mathString, 1, statemNum, 1);
+    g_outputToString = 0;
     if(!success) {
       print2("?Warning: %s\n", texLine);
       warnCount++;
@@ -954,7 +954,7 @@ void verifySts(vstring format) {
 /* Returns the token ID for a given token */
 long tokenId(vstring token) {
   void *mathKeyPtr; /* For binary search */
-  mathKeyPtr = (void *)bsearch(token, mathKey, (size_t)mathTokens,
+  mathKeyPtr = (void *)bsearch(token, g_mathKey, (size_t)g_mathTokens,
       sizeof(long), mathSrchCmp);
   if (!mathKeyPtr) return -1;
   return *((long *)mathKeyPtr);
@@ -976,16 +976,16 @@ vstring stsToken(long tokenId, long stateNum) {
 
   // Expect to find
   long schemeId = stsVar[tokenId].stsSchemeId;
-  //printf("Printing token %s, schemeId = %ld\n", mathToken[tokenId].tokenName, schemeId);
+  //printf("Printing token %s, schemeId = %ld\n", g_MathToken[tokenId].tokenName, schemeId);
   //if(schemeId == 0)
-  //  printf("Var not found : %s\n", mathToken[tokenId].tokenName);
+  //  printf("Var not found : %s\n", g_MathToken[tokenId].tokenName);
   if(schemeId >= 1 && schemeId <= stsSchemes && stsVar[stsScheme[schemeId - 1].scheme[0]].isTerminal) {
     /* If there is a single token scheme, build the token from the scheme itself. */
     getSTSLongMath(&str2, stsScheme[schemeId - 1].scheme, 0, 0, 0);
   }
   else {
     /* Otherwise fallback to metamath token in case token unavailable */
-    let(&str2, cat("<code style=\"color:red;\">",mathToken[tokenId].tokenName,"</code>", NULL));
+    let(&str2, cat("<code style=\"color:red;\">",g_MathToken[tokenId].tokenName,"</code>", NULL));
   }
   return str2;
 }
@@ -1001,14 +1001,14 @@ vstring asciiToMathSts(vstring text, long statemNum) {
   nmbrString *mathString = NULL_NMBRSTRING;
   flag result = 0;
 
-//  outputToString = 0;
+//  g_outputToString = 0;
 //  print2("Going to try %ld types!\n", stsTypes);
 //  dbs5=1;
-  /* 20-Jan-2019 tar - use "statements" as stateNum, since all tokens are valid. */
-  nmbrLet(&orgString, parseMathTokens(text, statements));
+  /* 20-Jan-2019 tar - use "g_statements" as stateNum, since all tokens are valid. */
+  nmbrLet(&orgString, parseMathTokens(text, g_statements));
   for(int i=0;!result && i<nmbrLen(stsTerminalTypes);i++) {
     nmbrLet(&mathString, nmbrUnshiftElement(orgString, stsTerminalTypes[i])); // was 39
-    outputToString = 0;
+    g_outputToString = 0;
 //    print2("Trying to print \"%s\"!\n", nmbrCvtMToVString(mathString));
     result = getSTSLongMath(&mmlLine, mathString, 0, statemNum, 1);
   }

From 9202215194cb63616f446d08e621f31d1f127f3f Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <thierry.arnoux@gmx.net>
Date: Sat, 25 Dec 2021 21:54:55 +0800
Subject: [PATCH 3/9] Delete makefile, formatting.

---
 Makefile.am |  2 ++
 makefile    | 11 -----------
 metamath.c  |  2 +-
 mmhlpb.c    |  1 +
 4 files changed, 4 insertions(+), 12 deletions(-)
 delete mode 100644 makefile

diff --git a/Makefile.am b/Makefile.am
index d6a0c3b6..ab6f774c 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -16,6 +16,7 @@ noinst_HEADERS = \
 	mmvstr.h \
 	mmword.h \
 	mmwtex.h \
+	mmhtbl.h \
 	mmwsts.h
 
 metamath_SOURCES = \
@@ -35,6 +36,7 @@ metamath_SOURCES = \
 	mmvstr.c \
 	mmword.c \
 	mmwtex.c \
+	mmhtbl.c \
 	mmwsts.c \
 	$(noinst_HEADERS)
 
diff --git a/makefile b/makefile
deleted file mode 100644
index 10bb970e..00000000
--- a/makefile
+++ /dev/null
@@ -1,11 +0,0 @@
-objects = metamath.o mmcmdl.o mmcmds.o mmdata.o mmhlpa.o mmhlpb.o mminou.o mmmaci.o mmpars.o mmpfas.o mmunif.o mmutil.o mmveri.o mmvstr.o \
-	mmword.o mmwtex.o mmhtbl.o mmwsts.o
-
-
-metamath: $(objects)
-	cc -o metamath $(CFLAGS) $(objects)
-
-%.o: %.c
-	cc -c $*.c -std=gnu99 $(CFLAGS)
-
-
diff --git a/metamath.c b/metamath.c
index 30e8db37..bc3688b1 100644
--- a/metamath.c
+++ b/metamath.c
@@ -2389,7 +2389,7 @@ void command(int argc, char *argv[])
           continue;
         }
         g_altHtmlFlag = 1;
-            } else if (switchPos ("/ STS") != 0) {
+      } else if (switchPos ("/ STS") != 0) {
         stsFlag = 1;
         let(&stsOutput, g_fullArg[5]);
 
diff --git a/mmhlpb.c b/mmhlpb.c
index de5ebe39..9214ba7a 100644
--- a/mmhlpb.c
+++ b/mmhlpb.c
@@ -42,6 +42,7 @@ H("For a summary of comment markup, type HELP VERIFY MARKUP.");
 H("For help getting started, type HELP DEMO.");
 H("For help exploring the data base, type HELP EXPLORE.");
 H("For help creating a LaTeX file, type HELP TEX.");
+H("For help with structured typesetting, type HELP STS.");
 H("For help creating Web pages, type HELP HTML.");
 H("For help proving new theorems, type HELP PROOF_ASSISTANT.");
 H("For a list of help topics, type HELP ? (to force an error message).");

From 991bd6cb47029d2c95d4ad5fa3a3d5ebb26ddc67 Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <thierry.arnoux@gmx.net>
Date: Sat, 25 Dec 2021 23:56:19 +0800
Subject: [PATCH 4/9] Double-space after periods in help texts.

---
 mmhlpa.c | 6 +++---
 mmhlpb.c | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/mmhlpa.c b/mmhlpa.c
index 15e514df..2c280802 100644
--- a/mmhlpa.c
+++ b/mmhlpa.c
@@ -810,15 +810,15 @@ g_printHelp = !strcmp(saveHelpCmd, "HELP STS");
 H("To create an HTML output file for a $a or $p statement, use");
 H("    SHOW STATEMENT <label> / STS <format>");
 H("The output and usage of that command is similar to the / HTML qualifier.");
-H("However the way the formula is generated differs. Symbols are not mapped");
+H("However the way the formula is generated differs.  Symbols are not mapped");
 H("one-to-one with their HTML representation, instead, the statements are");
-H("matched against patterns. Those patterns are provided in a file named");
+H("matched against patterns.  Those patterns are provided in a file named");
 H("    <source>-<format>.MMTS");
 H("Where <source> is the name of the main Metamath file loaded using READ.");
 H("The generic format for the rules in the MMTS definition file is");
 H("    $s <pattern> $: <translation> $.");
 H("Where <pattern> is the pattern to be matched, and <translation> the");
-H("rendered string. If any variable present in <pattern> appears in");
+H("rendered string.  If any variable present in <pattern> appears in");
 H("<translation> between hash symbols (#), the corresponding sub-string");
 H("will be recursively matched.");
 H("");
diff --git a/mmhlpb.c b/mmhlpb.c
index 9214ba7a..5242d4b1 100644
--- a/mmhlpb.c
+++ b/mmhlpb.c
@@ -196,7 +196,7 @@ H("    / ALT_HTML, / BRIEF_HTML, / BRIEF_ALT_HTML - See HELP HTML for more");
 H("        information on these.");
 /* 13-Jan-2018 tar Added STS */
 H("    / STS This qualifier invokes the HTML mode of SHOW STATEMENT, for");
-H("        creating a Web page for the statement. However it does not so by");
+H("        creating a Web page for the statement.  However it does not so by");
 H("        mapping symbols one-to-one with their HTML representation, but");
 H("        uses an approach based on the structure of the statement.");
 H("        See HELP STS for more information.");

From 1a66907bddef31e64f19c78cd1b8a604b947d46d Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <thierry.arnoux@gmx.net>
Date: Sun, 26 Dec 2021 02:37:45 +0800
Subject: [PATCH 5/9] More help text formatting

---
 mmhlpb.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mmhlpb.c b/mmhlpb.c
index 5242d4b1..afee425b 100644
--- a/mmhlpb.c
+++ b/mmhlpb.c
@@ -722,7 +722,7 @@ g_printHelp = !strcmp(saveHelpCmd, "HELP VERIFY STS");
 H("Syntax:  VERIFY STS <format>");
 H("");
 H("This command error-checks that the STS rules definition covers all syntax");
-H("defined in the Metamath source file loaded. It runs through all non");
+H("defined in the Metamath source file loaded.  It runs through all non-");
 H("definitional axioms and prints a warning on those which do not have ");
 H("corresponding STS rules. ");
 H("");

From f3ae0fa7684d19d1d71c65caae7f883e4bad39aa Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <thierry.arnoux@gmx.net>
Date: Sun, 26 Dec 2021 23:10:04 +0800
Subject: [PATCH 6/9] Typo: parsetSTSRules -> parseSTSRules

---
 metamath.c | 4 ++--
 mmwsts.c   | 4 ++--
 mmwsts.h   | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/metamath.c b/metamath.c
index bc3688b1..4bd6d9e7 100644
--- a/metamath.c
+++ b/metamath.c
@@ -2394,7 +2394,7 @@ void command(int argc, char *argv[])
         let(&stsOutput, g_fullArg[5]);
 
         /* Parse the STS rules corresponding to the expected output . */
-        parsetSTSRules(stsOutput);
+        parseSTSRules(stsOutput);
       }
 
       if (2/*error*/ == readTexDefs(0 /* 1 = check errors only */,
@@ -3033,7 +3033,7 @@ void command(int argc, char *argv[])
         let(&stsOutput, g_fullArg[5]);
 
         /* Parse the STS rules corresponding to the expected output. */
-        parsetSTSRules(stsOutput);
+        parseSTSRules(stsOutput);
       }
 
       q = 0;
diff --git a/mmwsts.c b/mmwsts.c
index 40e0698e..3b5bbf1a 100644
--- a/mmwsts.c
+++ b/mmwsts.c
@@ -214,7 +214,7 @@ void stsDumpCache(nmbrString *key, vstring object) {
 }
 
 /* Parse a file containing the structured typesetting rules. */
-int parsetSTSRules(vstring format) {
+int parseSTSRules(vstring format) {
   vstring inputFn = "";
   vstring chunk = "";
   char chunkType = 0;
@@ -915,7 +915,7 @@ void verifySts(vstring format) {
 
   print2("Verifying axioms have %s STS schemes...\n", format);
   if(strcmp(stsFormat, format)) {
-    if(!parsetSTSRules(format)) {
+    if(!parseSTSRules(format)) {
       print2("?Aborting verify.\n");
       return;
     }
diff --git a/mmwsts.h b/mmwsts.h
index 2f295f76..dfc9095e 100644
--- a/mmwsts.h
+++ b/mmwsts.h
@@ -11,7 +11,7 @@
 #include "mmdata.h"
 
 /* Parse an STS file */
-int parsetSTSRules(vstring format);
+int parseSTSRules(vstring format);
 
 /* Returns the HTML code for MathML, for the math string (hypothesis or
    conclusion) that is passed in. */

From 2a870d8c593c86f8652532db4e7cd2b99ec3088f Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <thierry.arnoux@gmx.net>
Date: Sun, 26 Dec 2021 23:20:32 +0800
Subject: [PATCH 7/9] Update comments in metamath.c

---
 metamath.c | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/metamath.c b/metamath.c
index 4bd6d9e7..6b00cfbe 100644
--- a/metamath.c
+++ b/metamath.c
@@ -20,6 +20,7 @@
                memory management; converts between proof formats
     mmhlpa.c - The help file, part 1.
     mmhlpb.c - The help file, part 2.
+    mmhtbl.c - Hashtable implementation
     mminou.c - Basic input and output interface
     mmmaci.c - THINK C Macintosh interface (obsolete)
     mmpars.c - Parses the source file
@@ -29,6 +30,7 @@
     mmveri.c - Proof verifier for source file
     mmvstr.c - BASIC-like string functions
     mmwtex.c - LaTeX/HTML source generation
+    mmwsts.c - STS source generation
     mmword.c - File revision utility (for TOOLS> UPDATE) (not generally useful)
 */
 
@@ -57,7 +59,16 @@
 
 
 
-#define MVERSION "0.198 7-Aug-2021"
+#define MVERSION "0.199 24-Dec-2021"
+/* 0.199 tar 24-Dec-2021 mmwsts.c and others - Merge STS source generation code
+   originally developped in July 2017.  STS stands for Structured TypeSetting and
+   can be used to generate MathML, which can in turn be postprocessed by MathJAX
+   to output mathematical typesetting (this includes indices, exponents, summands
+   and integrals with sets specifed below the sign, square roots with overhangs,
+   fraction bars, sized parentheses, etc.)  The code introduces a new / STS flag
+   as a third alternative to / HTML and / ALT_HTML for HTML page generation, and
+   a / VERIFY STS option to only check the integrity of the external STS command
+   file.  */
 /* 0.198 nm 7-Aug-2021 mmpars.c - Fix cosmetic bug in WRITE SOURCE ... /REWRAP
    that prevented end of sentence (e.g. period) from appearing in column 79,
    thus causing some lines to be shorter than necessary. */
@@ -2973,7 +2984,7 @@ void command(int argc, char *argv[])
       i = 5;  /* # arguments with only / HTML or / ALT_HTML */
       if (noVersioning) i = i + 2;
       if (switchPos("/ TIME")) i = i + 2;
-      /* 7-Jul-2017 added MathML/STS */
+      /* 7-Jul-2017 added MathML/STS : one more argument for STS */
       if (switchPos("/ STS")) i = i + 1;
       if (g_rawArgs != i) {
         printLongLine(cat("?The HTML qualifiers may not be combined with",

From c5925cb375eaad45e4b1e77e6b469d3704077095 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sat, 8 Jan 2022 04:28:46 -0500
Subject: [PATCH 8/9] fix compile errors/warnings

---
 metamath.c |  1 +
 mmhtbl.c   |  2 +-
 mmhtbl.h   |  8 ++++----
 mmwsts.c   | 41 +++++++++++++++++++++++++++++------------
 4 files changed, 35 insertions(+), 17 deletions(-)

diff --git a/metamath.c b/metamath.c
index 9d595e76..83c5b15f 100644
--- a/metamath.c
+++ b/metamath.c
@@ -713,6 +713,7 @@
 #include "mmpfas.h"
 #include "mmunif.h"
 #include "mmword.h"
+#include "mmwsts.h"
 #include "mmwtex.h"
 
 void command(int argc, char *argv[]);
diff --git a/mmhtbl.c b/mmhtbl.c
index e6d9f8fc..a3fb499f 100644
--- a/mmhtbl.c
+++ b/mmhtbl.c
@@ -32,7 +32,7 @@ void htinit() {
    Returns the hashtable created. */
 hashtable htcreate(vstring name, int bucket_count, void *no_obj,
 		  hashFunc *hashF, eqFunc *eqF, letFunc *letF,
-		  freeFunc *freeF, eqFunc *dumpF) {
+		  freeFunc *freeF, dumpFunc *dumpF) {
   htinit();
 
   /* Allocate space for the bucket pointers */
diff --git a/mmhtbl.h b/mmhtbl.h
index 87f68ea1..a0a4311a 100644
--- a/mmhtbl.h
+++ b/mmhtbl.h
@@ -8,14 +8,14 @@
 #define MMHTBL_H_
 
 #include <stdio.h>
-#include "mmutil.h"
 #include "mmvstr.h"
 #include "mmdata.h"
 
 typedef int (hashFunc)(void *);
 typedef int (eqFunc)(void *, void *);
 typedef void (letFunc)(void **, void **, void *, void*);
-typedef void (freeFunc)(void *, void *);
+typedef void (freeFunc)(void **, void **);
+typedef void (dumpFunc)(void *, void *);
 
 struct linked_struct {
   void *object;
@@ -39,14 +39,14 @@ struct hashtable_struct {
   eqFunc *eqFunc;
   letFunc *letFunc;
   freeFunc *freeFunc;
-  eqFunc *dumpFunc;
+  dumpFunc *dumpFunc;
 };
 
 typedef struct hashtable_struct hashtable;
 
 hashtable htcreate(vstring name, int bucket_count, void *no_obj,
 		   hashFunc *hashF, eqFunc *eqF, letFunc *letF,
-		   freeFunc *freeF, eqFunc *dumpF);
+		   freeFunc *freeF, dumpFunc *dumpF);
 void htdelete(hashtable *hashtable);
 flag htput(hashtable *hashtable, void *key, void *object);
 void *htget(hashtable *hashtable, void *key);
diff --git a/mmwsts.c b/mmwsts.c
index 3b5bbf1a..8a22b101 100644
--- a/mmwsts.c
+++ b/mmwsts.c
@@ -12,7 +12,6 @@
 #include <stdlib.h>
 #include <ctype.h>
 #include <stdarg.h>
-#include "mmutil.h"
 #include "mmvstr.h"
 #include "mmdata.h"
 #include "mminou.h"
@@ -192,8 +191,20 @@ nmbrString *parseMathStrict(vstring text)
   return mathString;
 }
 
+int stsCacheHash(void *s) {
+  return nmbrHash((nmbrString*)s);
+}
+
+int stsCacheEq(void *s, void *t) {
+  return nmbrEq((nmbrString*)s, (nmbrString*)t);
+}
+
 /* Store a couple key/object into the cache */
-void stsStoreCache(nmbrString **tKey, vstring *tObject, nmbrString *sKey, vstring sObject) {
+void stsStoreCache(void **tKey_, void **tObject_, void *sKey_, void *sObject_) {
+  nmbrString **tKey = (nmbrString **)tKey_;
+  vstring *tObject = (vstring *)tObject_;
+  nmbrString *sKey = (nmbrString *)sKey_;
+  vstring sObject = (vstring)sObject_;
   *tKey = NULL_NMBRSTRING;
   nmbrLet(tKey, sKey);
 
@@ -202,14 +213,19 @@ void stsStoreCache(nmbrString **tKey, vstring *tObject, nmbrString *sKey, vstrin
 }
 
 /* Free a couple key/object from the cache */
-void stsFreeCache(nmbrString **key, vstring *object) {
+void stsFreeCache(void **key_, void **object_) {
+  nmbrString **key = (nmbrString**)key_;
+  vstring *object = (vstring*)object_;
   nmbrLet(key, NULL_NMBRSTRING);
   let(object, NULL);
 }
 
 /* Dump a couple key/object from the cache */
-void stsDumpCache(nmbrString *key, vstring object) {
-//  printf("- %s -> %s\n", nmbrCvtMToVString(key), object);
+void stsDumpCache(void *key_, void *object_) {
+  nmbrString *key = (nmbrString*)key_;
+  (void)object_;
+  // vstring object = (vstring)object_;
+  // printf("- %s -> %s\n", nmbrCvtMToVString(key), object);
   printf("- (%d) %s [%s]\n", nmbrHash(key), nmbrCvtMToVString(key), nmbrCvtAnyToVString(key));
 }
 
@@ -230,9 +246,8 @@ int parseSTSRules(vstring format) {
 
   /* Create a cache for exported statements to speed up */
   if(stsUseCache) {
-    stsCache = htcreate(format, STS_CACHE_BUCKETS, "", (hashFunc*)&nmbrHash, (eqFunc*)&nmbrEq,
-			(letFunc*)&stsStoreCache, (freeFunc*)&stsFreeCache,
-			(eqFunc*)&stsDumpCache);
+    stsCache = htcreate(format, STS_CACHE_BUCKETS, "", stsCacheHash, stsCacheEq,
+			stsStoreCache, stsFreeCache, stsDumpCache);
   }
 
   /* Build the name of the MMTS file to load */
@@ -501,8 +516,9 @@ int parseSTSRules(vstring format) {
 	    }
 	    long end = pos + 3;
 	    vstring *target;
-	    if(chunkType == 'd') target = stsDisplayed;
-	    if(chunkType == 't') target = stsInText;
+	    if (chunkType == 'd') target = stsDisplayed;
+	    else if (chunkType == 't') target = stsInText;
+      else { bug(2410); continue; }
 	    let(&(target[0]), left(chunk, pos-1));
 	    let(&(target[1]), mid(chunk, end, len(chunk)-end+1));
 	    let(&chunk, "");
@@ -686,9 +702,9 @@ flag unifySts(nmbrString *mathString, nmbrString *scheme, nmbrString *varPos, nm
     /* Compute next state */
     if(lastVarNextOcc >= 0) {
       state[lastVarNextOcc]++;
-      for(int i=lastVarNextOcc+1;i<varCount-1;i++)
+      for (int i=lastVarNextOcc+1;i<varCount-1;i++)
         state[i] = 1;
-        if(dbs7) print2("Next state is %s\n",nmbrCvtAnyToVString(state));
+      if(dbs7) print2("Next state is %s\n",nmbrCvtAnyToVString(state));
     }
   }
   while(lastVarNextOcc >= 0 && !balanced);
@@ -968,6 +984,7 @@ long tokenId(vstring token) {
  * token in ASCII */
 /* *** Note: The caller must deallocate the returned string */
 vstring stsToken(long tokenId, long stateNum) {
+  (void)stateNum;
   vstring str2 = "";
   if(stsVar == NULL) {
     print2("Error: STS has not been initialized.");

From e5f602fb8f3941ed41f7aa572bd4bc7848435751 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sat, 8 Jan 2022 04:37:33 -0500
Subject: [PATCH 9/9] tabs -> spaces

---
 metamath.c |   2 +-
 mmdata.c   |   4 +-
 mmhtbl.c   |  10 +-
 mmhtbl.h   |   4 +-
 mmwsts.c   | 368 ++++++++++++++++++++++++++---------------------------
 mmwsts.h   |   2 +-
 mmwtex.c   |   6 +-
 7 files changed, 197 insertions(+), 199 deletions(-)

diff --git a/metamath.c b/metamath.c
index 83c5b15f..4113b36f 100644
--- a/metamath.c
+++ b/metamath.c
@@ -2690,7 +2690,7 @@ void command(int argc, char *argv[]) {
           let(&pipeCommand, cat(postProcess, " > ", g_texFileName, NULL));
           g_texFilePtr = popen(pipeCommand, "w");
           if (!g_texFilePtr) print2("?Could not execute the command \"%s\".\n",
-	          pipeCommand);
+            pipeCommand);
           let(&pipeCommand, "");
         } else {
           print2("Creating HTML file \"%s\"...\n", g_texFileName);
diff --git a/mmdata.c b/mmdata.c
index af5f4248..b63fe774 100644
--- a/mmdata.c
+++ b/mmdata.c
@@ -1150,8 +1150,8 @@ long nmbrInstrN(long start_position, long occ, nmbrString *string1,
         }
       }
       if (found) {
-	start_position = i+1;
-	break;
+        start_position = i+1;
+        break;
       }
     }
     if (i == ls1 - length2 + 1) return 0;
diff --git a/mmhtbl.c b/mmhtbl.c
index a3fb499f..992f10a1 100644
--- a/mmhtbl.c
+++ b/mmhtbl.c
@@ -31,8 +31,8 @@ void htinit() {
 /* Creates a new hashtable.
    Returns the hashtable created. */
 hashtable htcreate(vstring name, int bucket_count, void *no_obj,
-		  hashFunc *hashF, eqFunc *eqF, letFunc *letF,
-		  freeFunc *freeF, dumpFunc *dumpF) {
+                   hashFunc *hashF, eqFunc *eqF, letFunc *letF,
+                   freeFunc *freeF, dumpFunc *dumpF) {
   htinit();
 
   /* Allocate space for the bucket pointers */
@@ -90,7 +90,7 @@ flag htput(hashtable *hashtable, void *key, void *object) {
 
   /* Store object and key */
   hashtable->letFunc(&linkedItems[linkedItem].key,
-		     &linkedItems[linkedItem].object, key, object);
+                     &linkedItems[linkedItem].object, key, object);
   hashtable->entries++;
 
   /* Compute the bucket */
@@ -165,8 +165,8 @@ void htstats(hashtable *hashtable) {
   int empty_buckets = 0;
   for(int bucket=0;bucket<hashtable->bucket_count;bucket++) empty_buckets+=hashtable->buckets[bucket] == NO_LINKEDITEM;
   printf("Hashtable %s: %d entries, load factor=%d%%, %d used buckets, %d%% misses, biggest bucket=%d\n", hashtable->name, hashtable->entries,
-	 htlf(hashtable), (hashtable->bucket_count - empty_buckets), (100-(100*hashtable->founds/hashtable->gets)),
-	 hashtable->biggest_bucket_size);
+         htlf(hashtable), (hashtable->bucket_count - empty_buckets), (100-(100*hashtable->founds/hashtable->gets)),
+         hashtable->biggest_bucket_size);
 }
 
 /* Dumpts the whole table */
diff --git a/mmhtbl.h b/mmhtbl.h
index a0a4311a..70e2ff65 100644
--- a/mmhtbl.h
+++ b/mmhtbl.h
@@ -45,8 +45,8 @@ struct hashtable_struct {
 typedef struct hashtable_struct hashtable;
 
 hashtable htcreate(vstring name, int bucket_count, void *no_obj,
-		   hashFunc *hashF, eqFunc *eqF, letFunc *letF,
-		   freeFunc *freeF, dumpFunc *dumpF);
+                   hashFunc *hashF, eqFunc *eqF, letFunc *letF,
+                   freeFunc *freeF, dumpFunc *dumpF);
 void htdelete(hashtable *hashtable);
 flag htput(hashtable *hashtable, void *key, void *object);
 void *htget(hashtable *hashtable, void *key);
diff --git a/mmwsts.c b/mmwsts.c
index 8a22b101..1db2ed6b 100644
--- a/mmwsts.c
+++ b/mmwsts.c
@@ -21,12 +21,12 @@
 #include "mmwtex.h" /* For g_texDefsRead */
 #include "mmhtbl.h" /* For caching results */
 
-#define STS_MAX_TYPES 10		/* basic types. For set.mm, there are 4 (|-,wff,class,set) */
-#define STS_MAX_RECURSION 50	/* max depth of a formula (heuristic to avoid loops) */
-#define STS_MAX_SCHEME_VAR 20	/* max variables per schemes */
+#define STS_MAX_TYPES 10         /* basic types. For set.mm, there are 4 (|-,wff,class,set) */
+#define STS_MAX_RECURSION 50     /* max depth of a formula (heuristic to avoid loops) */
+#define STS_MAX_SCHEME_VAR 20    /* max variables per schemes */
 #define STS_MAX_TOKEN_REUSE 20
 #define STS_MAX_LEN_FOR_CACHE 20 /* put only formulas of up to 20 tokens into cache */
-#define STS_CACHE_BUCKETS 50000	 /* size of a cache hash bucket */
+#define STS_CACHE_BUCKETS 50000  /* size of a cache hash bucket */
 
 /* The structure containing the structured typesetting replacement schemes */
 struct stsScheme_struct {
@@ -169,7 +169,7 @@ nmbrString *parseMathStrict(vstring text)
     fbPtr[tokenLen_] = 0; /* End token - There's no come back */
     //printf("Searching for %s\n", fbPtr);
     g_mathKeyPtr = (long *)bsearch(fbPtr, g_mathKey,
-	(size_t)g_mathTokens, sizeof(long), mathSrchGlbCmp);
+      (size_t)g_mathTokens, sizeof(long), mathSrchGlbCmp);
     if (!g_mathKeyPtr) {
       /* Unknown token, escape. */
       print2("?Unknown token %s\n", fbPtr);
@@ -247,7 +247,7 @@ int parseSTSRules(vstring format) {
   /* Create a cache for exported statements to speed up */
   if(stsUseCache) {
     stsCache = htcreate(format, STS_CACHE_BUCKETS, "", stsCacheHash, stsCacheEq,
-			stsStoreCache, stsFreeCache, stsDumpCache);
+                        stsStoreCache, stsFreeCache, stsDumpCache);
   }
 
   /* Build the name of the MMTS file to load */
@@ -274,7 +274,7 @@ int parseSTSRules(vstring format) {
   if (fseek(sts_fp, 0, SEEK_SET)) bug(5702);
   /* Put the entire input file into the buffer as a giant character string */
   long charCount = (long)fread(fileBuf, sizeof(char), (size_t)fileBufSize - 2,
-			       sts_fp);
+                               sts_fp);
   if (!feof(sts_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
@@ -315,11 +315,11 @@ int parseSTSRules(vstring format) {
     if (!tmpch) { /* End of file */
       if (insideComment) {
         rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum - 1, inputFn,*/
-         "The last comment in the file is incomplete.  \"$)\" was expected.");
-	if (insideChunk) {
+          "The last comment in the file is incomplete.  \"$)\" was expected.");
+        if (insideChunk) {
           rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
               cat("The last ", stsChunkName(chunkType),
-		  " in the file is incomplete.", NULL));
+                  " in the file is incomplete.", NULL));
         }
         if (insideTypeSet) {
           rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
@@ -393,24 +393,24 @@ int parseSTSRules(vstring format) {
       case 'i': /* Start of identifier */
       case 's': /* Start of scheme */
       case 'u': /* Start of terminal type */
-	if (insideComment) continue;
-	if (insideChunk) {
+        if (insideComment) continue;
+        if (insideChunk) {
           rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
               cat("A scheme start was found within a ",
-		  stsChunkName(chunkType), ".", NULL));
+                  stsChunkName(chunkType), ".", NULL));
         }
         if (insideTypeSet) {
           rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
               cat("A ",stsChunkName(fbPtr[0]),
-		  " start was found within a typeset.", NULL));
+                  " start was found within a typeset.", NULL));
         }
         chunkType = fbPtr[0];
         startPtr = fbPtr + 1;
         insideChunk = 1;
-	continue;
+        continue;
 
       case ':': /* Start of typesetting */
-	if (insideComment) continue;
+        if (insideComment) continue;
         if (!insideChunk || (chunkType != 's' && chunkType != 'i')) {
           rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
               "A scheme end was found outside of a scheme.");
@@ -423,24 +423,24 @@ int parseSTSRules(vstring format) {
         //print2("end scheme line %ld! %s\n", lineNum, text);
         stsScheme[stsSchemes].type = chunkType;
         stsScheme[stsSchemes].scheme = NULL_NMBRSTRING;
-	// parseMathTokens is too permissive. Wrote own token parser.
+        // parseMathTokens is too permissive. Wrote own token parser.
         //nmbrLet(&(stsScheme[stsSchemes].scheme), parseMathTokens(text, g_statements));
         nmbrLet(&(stsScheme[stsSchemes].scheme), parseMathStrict(text));
 
         int l = nmbrLen(stsScheme[stsSchemes].scheme);
         if(l < 2) {
           if(l == 0)
-	    rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
-		"Empty scheme or unknown token.");
+            rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+                "Empty scheme or unknown token.");
           else
-	    rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
-		"A scheme shall contain at least 2 tokens.");
+            rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+                "A scheme shall contain at least 2 tokens.");
           chunkType = '$'; // invalid chunk type, so that the scheme is skipped.
           startPtr = fbPtr + 1;
           insideChunk = 0;
-	  insideTypeSet = 1;
-	  stsSchemes--;
-	  continue;
+          insideTypeSet = 1;
+          stsSchemes--;
+          continue;
           }
 
         /* Store the number of variables in the scheme (each shall be different)  */
@@ -465,89 +465,89 @@ int parseSTSRules(vstring format) {
           if(g_MathToken[index].tokenType != var_)
             rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
                 "An identifier definition shall end with a variable.");
-	    //print2("Token %s has type %s\n", g_MathToken[index].tokenName, g_MathToken[stsVar[index].stsType].tokenName);
+            //print2("Token %s has type %s\n", g_MathToken[index].tokenName, g_MathToken[stsVar[index].stsType].tokenName);
         }
 
         startPtr = fbPtr + 1;
         insideChunk = 0;
-	insideTypeSet = 1;
-	continue;
+        insideTypeSet = 1;
+        continue;
 
       case '.': /* End of chunk/typesetting */
-	if (insideComment) continue;
-	if (!insideChunk && !insideTypeSet) {
+        if (insideComment) continue;
+        if (!insideChunk && !insideTypeSet) {
           rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
               "A chunk/typeset end was found outside a chunk or typeset.");
-	}
-	insideChunk = 0;
-	switch(chunkType) {
-	  case 'i':
-	  case 's':
-	    /* End of typesetting, record the new scheme. */
-	    if(!insideTypeSet) {
-	      rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
-		  cat("A typeset end was found within a ",
-		      stsChunkName(chunkType), ".", NULL));
-	    }
-	    stsScheme[stsSchemes].typesetting = "";
-	    let(&(stsScheme[stsSchemes].typesetting), mid(startPtr, 2, fbPtr - startPtr - 3));
-	    /* Record the schemeId */
-	    if(nmbrLen(stsScheme[stsSchemes].scheme) == 2
-	       && stsVar[stsScheme[stsSchemes].scheme[1]].stsSchemeId == 0)
-		stsVar[stsScheme[stsSchemes].scheme[1]].stsSchemeId = stsSchemes + 1;
-//	    for(int i=1;i<=nmbrLen(stsScheme[stsSchemes].scheme);i++)
-//	      if(stsVar[stsScheme[stsSchemes].scheme[i]].stsSchemeId == 0)
-//		stsVar[stsScheme[stsSchemes].scheme[i]].stsSchemeId = stsSchemes + 1;
-	    stsSchemes++;
-	    insideTypeSet = 0;
-	    continue;
-
-	  case 'd':
-	  case 't':
-	    /* End of the display/text chunk */
-	    let(&chunk, mid(startPtr, 2, fbPtr - startPtr - 3));
-	    long pos = instr(1, chunk, "###");
-	    if(pos == 0) {
-	      rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
-		  "Display/text chunk shall contain ###, which will be replaced"
-		  " by the generated formula in the generated HTML file.");
-	      let(&chunk, "");
-	      continue;
-	    }
-	    long end = pos + 3;
-	    vstring *target;
-	    if (chunkType == 'd') target = stsDisplayed;
-	    else if (chunkType == 't') target = stsInText;
+        }
+        insideChunk = 0;
+        switch(chunkType) {
+          case 'i':
+          case 's':
+            /* End of typesetting, record the new scheme. */
+            if(!insideTypeSet) {
+              rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+                  cat("A typeset end was found within a ",
+                      stsChunkName(chunkType), ".", NULL));
+            }
+            stsScheme[stsSchemes].typesetting = "";
+            let(&(stsScheme[stsSchemes].typesetting), mid(startPtr, 2, fbPtr - startPtr - 3));
+            /* Record the schemeId */
+            if(nmbrLen(stsScheme[stsSchemes].scheme) == 2
+               && stsVar[stsScheme[stsSchemes].scheme[1]].stsSchemeId == 0)
+                stsVar[stsScheme[stsSchemes].scheme[1]].stsSchemeId = stsSchemes + 1;
+//            for(int i=1;i<=nmbrLen(stsScheme[stsSchemes].scheme);i++)
+//              if(stsVar[stsScheme[stsSchemes].scheme[i]].stsSchemeId == 0)
+//                stsVar[stsScheme[stsSchemes].scheme[i]].stsSchemeId = stsSchemes + 1;
+            stsSchemes++;
+            insideTypeSet = 0;
+            continue;
+
+          case 'd':
+          case 't':
+            /* End of the display/text chunk */
+            let(&chunk, mid(startPtr, 2, fbPtr - startPtr - 3));
+            long pos = instr(1, chunk, "###");
+            if(pos == 0) {
+              rawSourceError(fileBuf, fbPtr - 1, 2, /*lineNum, inputFn,*/
+                  "Display/text chunk shall contain ###, which will be replaced"
+                  " by the generated formula in the generated HTML file.");
+              let(&chunk, "");
+              continue;
+            }
+            long end = pos + 3;
+            vstring *target;
+            if (chunkType == 'd') target = stsDisplayed;
+            else if (chunkType == 't') target = stsInText;
       else { bug(2410); continue; }
-	    let(&(target[0]), left(chunk, pos-1));
-	    let(&(target[1]), mid(chunk, end, len(chunk)-end+1));
-	    let(&chunk, "");
-	    continue;
-
-	  case 'h':
-	    /* End of the header chunk */
-	    let(&stsHeader, mid(startPtr, 2, fbPtr - startPtr - 3));
-	    continue;
-
-	  case 'c':
-	    /* End of the command line chunk */
-	    let(&postProcess, mid(startPtr, 2, fbPtr - startPtr - 3));
-	    continue;
-
-	  case 'u':
-	    /* End of terminal types list chunk */
-	    {
-	      vstring text = mid(startPtr, 2, fbPtr - startPtr - 3);
-	      nmbrLet(&stsTerminalTypes, parseMathStrict(text));
-	      for(int i=0;i<nmbrLen(stsTerminalTypes);i++) stsVar[stsTerminalTypes[i]].isTerminal = 1;
-	      continue;
-	    }
-
-	  case '$':
-	    /* Error handling for incorrect schemes */
-	    insideTypeSet = 0;
-	    continue;
-	}
+            let(&(target[0]), left(chunk, pos-1));
+            let(&(target[1]), mid(chunk, end, len(chunk)-end+1));
+            let(&chunk, "");
+            continue;
+
+          case 'h':
+            /* End of the header chunk */
+            let(&stsHeader, mid(startPtr, 2, fbPtr - startPtr - 3));
+            continue;
+
+          case 'c':
+            /* End of the command line chunk */
+            let(&postProcess, mid(startPtr, 2, fbPtr - startPtr - 3));
+            continue;
+
+          case 'u':
+            /* End of terminal types list chunk */
+            {
+              vstring text = mid(startPtr, 2, fbPtr - startPtr - 3);
+              nmbrLet(&stsTerminalTypes, parseMathStrict(text));
+              for(int i=0;i<nmbrLen(stsTerminalTypes);i++) stsVar[stsTerminalTypes[i]].isTerminal = 1;
+              continue;
+            }
+
+          case '$':
+            /* Error handling for incorrect schemes */
+            insideTypeSet = 0;
+            continue;
+        }
     }
   }
 
@@ -600,10 +600,10 @@ flag nmbrBalanced(nmbrString *str, long start, long len) {
     }
     if(pairingMismatches != 0) {
       if(dbs7) print2("Bracket mismatch for %s%s in %s (mismatch=%ld)\n",
-		      g_MathToken[open].tokenName,
-		      g_MathToken[close].tokenName,
-		      nmbrCvtMToVString(nmbrMid(str, start, len)),
-		      pairingMismatches);
+                      g_MathToken[open].tokenName,
+                      g_MathToken[close].tokenName,
+                      nmbrCvtMToVString(nmbrMid(str, start, len)),
+                      pairingMismatches);
       return 0;
     }
   }
@@ -657,41 +657,41 @@ flag unifySts(nmbrString *mathString, nmbrString *scheme, nmbrString *varPos, nm
     /* Handle separately the trivial cases where there are no or one variable. */
     switch(varCount) {
       case 0:
-	/* No variable : match the two strings */
-	return nmbrEq(scheme, mathString);
+        /* No variable : match the two strings */
+        return nmbrEq(scheme, mathString);
 
 //      case 1:
-//	/* One variable: match the start and end, assign the rest */
-//	varStart[0] = varPos[0];
-//	varLen[0] = lenString - lenScheme + 1;
-//	if(!nmbrSubEq(scheme, 1, mathString, 1, varStart[0]-1)) return 0;
-//	if(!nmbrSubEq(scheme, varPos[0]+1, mathString, varPos[0] + varLen[0], lenScheme - varPos[0])) return 0;
-//	if(dbs7) print2("Found unification for %s : %s (start=%ld, len=%ld)\n",g_MathToken[scheme[varPos[0]-1]].tokenName, nmbrCvtMToVString(nmbrMid(mathString, varStart[0], varLen[0])), varStart[0], varLen[0]);
-//	return 1;
+//        /* One variable: match the start and end, assign the rest */
+//        varStart[0] = varPos[0];
+//        varLen[0] = lenString - lenScheme + 1;
+//        if(!nmbrSubEq(scheme, 1, mathString, 1, varStart[0]-1)) return 0;
+//        if(!nmbrSubEq(scheme, varPos[0]+1, mathString, varPos[0] + varLen[0], lenScheme - varPos[0])) return 0;
+//        if(dbs7) print2("Found unification for %s : %s (start=%ld, len=%ld)\n",g_MathToken[scheme[varPos[0]-1]].tokenName, nmbrCvtMToVString(nmbrMid(mathString, varStart[0], varLen[0])), varStart[0], varLen[0]);
+//        return 1;
 
       default:
-	/* Two variables or more: first match the prefix and the suffix */
-	varStart[0] = varPos[0];
-	if(!nmbrSubEq(scheme, 1, mathString, 1, varStart[0]-1)) return 0;
-	if(!nmbrSubEq(scheme, varPos[varCount-1]+1, mathString, lenString - (lenScheme - varPos[varCount-1] - 1), lenScheme - varPos[varCount-1])) return 0;
-
-	/* Then, for each additional variable, */
-	for(int i=0;i<varCount-1;i++) {
-	  if(state[i] < 1) state[i] = 1;
-	  long conLength = varPos[i+1]-varPos[i]-1;
-	  if(dbs9) print2("Searching %ld's occurrence of %s in %s starting from %ld\n", state[i], nmbrCvtMToVString(nmbrMid(scheme, varPos[i]+1, conLength)), nmbrCvtMToVString(mathString), varStart[i]+1);
-	  long position = nmbrInstrN(varStart[i]+1, state[i], mathString, scheme, varPos[i]+1, conLength);
-	  if(dbs9) print2("Found pos %ld\n", position);
-	  if(position == 0) return 0;
-	  // note if there is a next occurrence
-	  if(nmbrInstrN(varStart[i]+1, state[i]+1, mathString, scheme, varPos[i]+1, conLength) > 0)
-	    lastVarNextOcc = i;
-	  varLen[i] = position - varStart[i];
-	  varStart[i+1] = position + conLength;
-	}
-	varLen[varCount-1] = lenString - (lenScheme - varPos[varCount-1]) - varStart[varCount-1] + 1;
-	if(dbs7) for(int i=0;i<varCount;i++) print2("Found unification for %s : %s (start=%ld, len=%ld)\n",g_MathToken[scheme[varPos[i]-1]].tokenName, nmbrCvtMToVString(nmbrMid(mathString, varStart[i], varLen[i])), varStart[i], varLen[i]);
-	break;
+        /* Two variables or more: first match the prefix and the suffix */
+        varStart[0] = varPos[0];
+        if(!nmbrSubEq(scheme, 1, mathString, 1, varStart[0]-1)) return 0;
+        if(!nmbrSubEq(scheme, varPos[varCount-1]+1, mathString, lenString - (lenScheme - varPos[varCount-1] - 1), lenScheme - varPos[varCount-1])) return 0;
+
+        /* Then, for each additional variable, */
+        for(int i=0;i<varCount-1;i++) {
+          if(state[i] < 1) state[i] = 1;
+          long conLength = varPos[i+1]-varPos[i]-1;
+          if(dbs9) print2("Searching %ld's occurrence of %s in %s starting from %ld\n", state[i], nmbrCvtMToVString(nmbrMid(scheme, varPos[i]+1, conLength)), nmbrCvtMToVString(mathString), varStart[i]+1);
+          long position = nmbrInstrN(varStart[i]+1, state[i], mathString, scheme, varPos[i]+1, conLength);
+          if(dbs9) print2("Found pos %ld\n", position);
+          if(position == 0) return 0;
+          // note if there is a next occurrence
+          if(nmbrInstrN(varStart[i]+1, state[i]+1, mathString, scheme, varPos[i]+1, conLength) > 0)
+            lastVarNextOcc = i;
+          varLen[i] = position - varStart[i];
+          varStart[i+1] = position + conLength;
+        }
+        varLen[varCount-1] = lenString - (lenScheme - varPos[varCount-1]) - varStart[varCount-1] + 1;
+        if(dbs7) for(int i=0;i<varCount;i++) print2("Found unification for %s : %s (start=%ld, len=%ld)\n",g_MathToken[scheme[varPos[i]-1]].tokenName, nmbrCvtMToVString(nmbrMid(mathString, varStart[i], varLen[i])), varStart[i], varLen[i]);
+        break;
     }
 
     /* Check that brackets are balanced in all substitutions */
@@ -741,8 +741,8 @@ flag getSTSLongMathRec(vstring *mmlLine, nmbrString *mathString, long statemNum,
       return 0;
     }
     if(nmbrEq(stsScheme[stsIndex - 1].scheme, mathString)) {
-	let(mmlLine, stsScheme[stsIndex - 1].typesetting);
-	return 1;
+      let(mmlLine, stsScheme[stsIndex - 1].typesetting);
+      return 1;
     }
   }
 
@@ -766,14 +766,14 @@ flag getSTSLongMathRec(vstring *mmlLine, nmbrString *mathString, long statemNum,
     /* Identifier schemes must be fully matched, and there is no substitution */
     if(stsScheme[stsIndex].type == 'i') {
       if(nmbrEq(stsScheme[stsIndex].scheme, mathString)) {
-	let(mmlLine, stsScheme[stsIndex].typesetting);
-	return 1;
+        let(mmlLine, stsScheme[stsIndex].typesetting);
+        return 1;
       } else continue;
     }
 
     /* This case was handled above - skip it here */
     if(nmbrLen(stsScheme[stsIndex].scheme) == 2
-	&& g_MathToken[stsScheme[stsIndex].scheme[1]].tokenType == con_) {
+        && g_MathToken[stsScheme[stsIndex].scheme[1]].tokenType == con_) {
       continue;
     }
 
@@ -802,52 +802,52 @@ flag getSTSLongMathRec(vstring *mmlLine, nmbrString *mathString, long statemNum,
     while((3 == result) && !success) {
       /* Launch unification (Neither unify() nor assignVar() actually match our need. Wrote our own unification) */
       if(dbs5) print2("%sTrying unification of \"%s\" and \"%s\" (state:<%s>)\n",
-		     space(recursionLevel),
-		     nmbrCvtMToVString(mathString),
-		     nmbrCvtMToVString(stsScheme[stsIndex].scheme),
-		     nmbrCvtAnyToVString(stateVector));
+                     space(recursionLevel),
+                     nmbrCvtMToVString(mathString),
+                     nmbrCvtMToVString(stsScheme[stsIndex].scheme),
+                     nmbrCvtAnyToVString(stateVector));
       result = unifySts(mathString, stsScheme[stsIndex].scheme, varPos, varStart, varLen, stateVector);
       if(dbs5) print2("%sResult is %d\n", space(recursionLevel), result);
       if(result == 3 && dbs3) print2("Unification for %s is not unique!\n", nmbrCvtMToVString(mathString));
       if(result != 0) {
-	let(mmlLine, stsScheme[stsIndex].typesetting);
-
-	if(dbs5) print2("%sFound match with %s\n", space(recursionLevel), nmbrCvtMToVString(stsScheme[stsIndex].scheme));
-	success = 1; /* Be optimistic an assume next level substitutions will succeed */
-	for(int i=0;i<varCount && success;i++) {
-	  long varToken = stsScheme[stsIndex].scheme[varPos[i]-1];
-	  if(dbs5) print2("%sVariable %d : %s , from %ld len %ld (%s)\n", space(recursionLevel), i, g_MathToken[varToken].tokenName, varStart[i], varLen[i], g_MathToken[stsVar[varToken].stsType].tokenName);
-
-	  /* Build the new math string */
-	  nmbrString *newMathString = NULL_NMBRSTRING;
-	  nmbrLet(&newMathString, nmbrUnshiftElement(
-	      nmbrMid(mathString, varStart[i], varLen[i]),
-	      stsVar[varToken].stsType));
-	  if(dbs5) print2("%sSubstitution : %s\n", space(recursionLevel), nmbrCvtMToVString(newMathString));
-
-	  /* Try unification - recursively */
-	  vstring substitution = "";
-	  success &= getSTSLongMathRec(&substitution, newMathString, statemNum, recursionLevel+1);
-
-	  /* deallocate new math string */
-	  nmbrLet(&newMathString, NULL_NMBRSTRING);
-
-	  if(success) {
-	    vstring anchor = getAnchor(varToken);
-	    long pos = instr(1, *mmlLine, anchor);
-	    while(pos != 0) {
-	      long end = pos + len(anchor);
-	      let(mmlLine, cat(left(*mmlLine, pos-1), substitution, mid(*mmlLine, end, len(*mmlLine)-end+1), NULL));
-	      pos = instr(pos + len(substitution), *mmlLine, anchor);
-	    }
-	  } /* end of if block on next substitution success */
-	  /* Deallocate local strings */
-	  let(&substitution, "");
-	  if(!success && recursionError) {
-	    //print2("When unifying %s with scheme %s (token type %s)\n", nmbrCvtMToVString(mathString), nmbrCvtMToVString(stsScheme[stsIndex].scheme), g_MathToken[stsVar[varToken].stsType].tokenName);
-	    return 0;
-	  }
-	} /* end of for loop on variable substitutions */
+        let(mmlLine, stsScheme[stsIndex].typesetting);
+
+        if(dbs5) print2("%sFound match with %s\n", space(recursionLevel), nmbrCvtMToVString(stsScheme[stsIndex].scheme));
+        success = 1; /* Be optimistic an assume next level substitutions will succeed */
+        for(int i=0;i<varCount && success;i++) {
+          long varToken = stsScheme[stsIndex].scheme[varPos[i]-1];
+          if(dbs5) print2("%sVariable %d : %s , from %ld len %ld (%s)\n", space(recursionLevel), i, g_MathToken[varToken].tokenName, varStart[i], varLen[i], g_MathToken[stsVar[varToken].stsType].tokenName);
+
+          /* Build the new math string */
+          nmbrString *newMathString = NULL_NMBRSTRING;
+          nmbrLet(&newMathString, nmbrUnshiftElement(
+              nmbrMid(mathString, varStart[i], varLen[i]),
+              stsVar[varToken].stsType));
+          if(dbs5) print2("%sSubstitution : %s\n", space(recursionLevel), nmbrCvtMToVString(newMathString));
+
+          /* Try unification - recursively */
+          vstring substitution = "";
+          success &= getSTSLongMathRec(&substitution, newMathString, statemNum, recursionLevel+1);
+
+          /* deallocate new math string */
+          nmbrLet(&newMathString, NULL_NMBRSTRING);
+
+          if(success) {
+            vstring anchor = getAnchor(varToken);
+            long pos = instr(1, *mmlLine, anchor);
+            while(pos != 0) {
+              long end = pos + len(anchor);
+              let(mmlLine, cat(left(*mmlLine, pos-1), substitution, mid(*mmlLine, end, len(*mmlLine)-end+1), NULL));
+              pos = instr(pos + len(substitution), *mmlLine, anchor);
+            }
+          } /* end of if block on next substitution success */
+          /* Deallocate local strings */
+          let(&substitution, "");
+          if(!success && recursionError) {
+            //print2("When unifying %s with scheme %s (token type %s)\n", nmbrCvtMToVString(mathString), nmbrCvtMToVString(stsScheme[stsIndex].scheme), g_MathToken[stsVar[varToken].stsType].tokenName);
+            return 0;
+          }
+        } /* end of for loop on variable substitutions */
       } /* end of if block on unification success */
       /* Stop if all next level substitutions succeeded */
       if(success) break;
@@ -893,10 +893,10 @@ flag getSTSLongMath(vstring *mmlLine, nmbrString *mathString, flag displayed, lo
     /* Return a generic error message */
     if(textwarn)
       let(mmlLine, cat("No typesetting for: ",
-			nmbrCvtMToVString(mathString),NULL));
+                        nmbrCvtMToVString(mathString),NULL));
     else
       let(mmlLine, cat("No typesetting for: <code>",
-			nmbrCvtMToVString(mathString),"</code>",NULL));
+                        nmbrCvtMToVString(mathString),"</code>",NULL));
   }
   else {
     /* Add the HTML container */
@@ -1065,8 +1065,8 @@ vstring asciiToMathSts(vstring text, long statemNum) {
 ////      print2("  extensions: [\"mml2jax.js\"],\n");
 ////      print2("  \"fast-preview\": { disabled: true },\n");
 //  print2("  SVG: { linebreaks: { width: \"container\", automatic: true }"
-////	  ", styles:{\".MathJax_Display\": { \"float\": \"left\" } }"
-//	  "}\n");
+////          ", styles:{\".MathJax_Display\": { \"float\": \"left\" } }"
+//          "}\n");
 //  print2("});</script>\n");
 //  print2("<script type=\"text/javascript\" src=\n");
 //  print2("\"https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/\n");
diff --git a/mmwsts.h b/mmwsts.h
index dfc9095e..1a74f1b8 100644
--- a/mmwsts.h
+++ b/mmwsts.h
@@ -17,7 +17,7 @@ int parseSTSRules(vstring format);
    conclusion) that is passed in. */
 /* Warning: The caller must deallocate the returned vstring. */
 flag getSTSLongMath(vstring *mmlLine, nmbrString *mathString, flag displayed,
-		    long statemNum, flag textwarn);
+                    long statemNum, flag textwarn);
 
 /* Returns the code to be included in the HTML head element
  * for the given format */
diff --git a/mmwtex.c b/mmwtex.c
index 0bdb7c38..43183698 100644
--- a/mmwtex.c
+++ b/mmwtex.c
@@ -5055,8 +5055,7 @@ vstring getTexOrHtmlHypAndAssertion(long statemNum) {
                  "\\quad\\&\\quad "
               ,NULL));
         } else {
-          if (g_altHtmlFlag
-        	  || stsFlag) { /* 22-Mar-2018 Added for STS */
+          if (g_altHtmlFlag || stsFlag) {
             /* Hard-coded for set.mm! */
             let(&texOrHtmlCode, cat(texOrHtmlCode,
                 "<SPAN ", g_htmlFont, ">",
@@ -5086,8 +5085,7 @@ vstring getTexOrHtmlHypAndAssertion(long statemNum) {
                  "\\quad\\Rightarrow\\quad "
           ,NULL));
     } else {
-      if (g_altHtmlFlag
-      	  || stsFlag) { /* 22-Mar-2018 Added for STS */
+      if (g_altHtmlFlag || stsFlag) {
         /* Hard-coded for set.mm! */
         let(&texOrHtmlCode, cat(texOrHtmlCode,
             /* sans-serif to work around FF3 bug that produces