From 966cfac941dbe7dedd266b119861d2161a2409ab Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Thu, 3 Mar 2022 20:25:58 +0100
Subject: [PATCH 01/42] doc cmdInput (1)

---
 src/mminou.h | 75 +++++++++++++++++++++++++++++-----------------------
 1 file changed, 42 insertions(+), 33 deletions(-)

diff --git a/src/mminou.h b/src/mminou.h
index f1789e82..bbba6b0a 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -100,44 +100,48 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
  * \brief requests a line of text from the __stream__.
  *
  * If not suppressed, displays a prompt text on the screen.  Then reads a
- * single line from the __stream__.  Returns this line as a \a vstring.
+ * line from the __stream__.  This line may be interpreted as described further
+ * below, in which case the prompt is reprinted and the next line is read.
+ * Returns the first not interpreted line as a \a vstring.
  *
  * A line in the __stream__ is terminated by a LF character (0x0D) character
  * alone.  It is read, but removed from the result.  The maximum line length
  * without the LF is \a CMD_BUFFER_SIZE - 1.  Reaching EOF (end of file) is
  * equivalent to reading LF, if at least 1 byte was read before.  Note that the
  * NUL character can be part of the line.  Reading a NUL is not sufficiently
- * handled in the current implementation and may or may not cause an error
+ * supported in the current implementation and may or may not cause an error
  * message or even undefined behavior.
  *
  * Reading from an empty __stream__ (or one that is at EOF position) returns
  * NULL, not the empty string, and is formally signalled as an error.
  * Overflowing the buffer is also an error.  No truncated value is returned.
  *
- * This routine automatically handles input in a loop under following two
- * conditions:
+ * This routine interprets some input without returning it to the caller under
+ * following two conditions:
  *
- * 1. If scrolling is enabled, the input is interpreted.  A line consisting of
- * a single character b or B indicates the user wants to scroll back through
- * saved pages of output.  This is handled within this routine, as often as
- * requested and possible.
+ * 1. If scrolling is enabled, a line consisting of a single character b or B
+ * may indicate the user wants to scroll back through saved pages of output.
+ * This is handled within this routine, if possible.  If it cannot be served,
+ * the b or B is returned as common user input.
  *
- * 2. The user repetitively hits ENTER (only) while prompted in top level
- * context.  The prompt is simply replayed as often.  Entering an isolated 'b'
- * or 'B' is first directed to case 1, and only if it cannot be served there, 
- * the routine exits, returning the b or B to the caller. 
- *
- * No timeout is applied when waiting for user input from the console.
+ * 2. The user hits ENTER (only) while prompted in top level context.  The
+ * empty line is not returned.
+ * 
+ * No timeout is applied while waiting for user input from the console.
  *
  * Detected format errors result in following bug messages:
  *   - 1507: The first read character is NUL
  *   - 1508: line overflow, the last character is not NUL
  *   - 1519: padding of LF failed, or first read character was NUL
  *   - 1521: a NUL in first and second position was read
- *   - 1523: no prompt text when user is required to input something
+ *   - 1523: NULL instead of a prompt text when user input is required
  *   - 1525: missing terminating LF, not caused by an EOF.
  *
- *   A bug message need not result in an execution stop.
+ *   A bug message need not result in an execution stop.  It is not directed to
+ *   the metamath bug function to avoid stacking up calls (bug calling cmdInput
+ *   again for scrolling etc.).
+ *
+ * \todo clarify recursive call to print2 and the role of backFromCmdInput. 
  * \param[in] stream (not null) source to read the line from.  _stdin_ is
  *   common for user input from the console. 
  * \param[in] ask prompt text displayed on the screen before __stream__ is
@@ -163,32 +167,37 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
  *     \a backBuffer;
  *   - \a localScrollMode a value of 0 temporarily disables scrolling, despite
  *     the setting in \a g_scrollMode;
- *   - \a g_commandPrompt if its string matches ask, empty input is ignored.
+ *   - \a g_commandPrompt if this string matches ask, top level user input is
+ *     assumed.
  * \post
- *   \a db is updated and includes the length of the interpreted input.
- *   Some input is ignored by simply reprinting the prompt:
- *   - Empty strings in top command level;
- *   - Isolated 'b' or 'B' input, if scroll mode is active, supported and the
- *     \a backBuffer provides a saved page.
+ *   \a db is updated.
  * \warning the calling program must deallocate the returned string (if not
  *   null or empty).  Note that the result can be NULL.  This is outside of the
  *   usual behavior of a \a vstring type.
  * \warning the returned string need not be valid ASCII or UTF-8.
- * \bug If the first character read from __stream__ is NUL (e.g. a file is
- *   read), this will cause a print of an error message, but execution
- *   continues and in the wake may cause all kind of undefined behavior, like
- *   memory accesses beyond allocated buffers.
+ * \bug If a character read from __stream__ is NUL, this may sometimes cause a
+ *   print of an error message, but execution continues and in the wake may
+ *   cause all kind of undefined behavior, like memory accesses beyond
+ *   allocated buffers.
  */
 vstring cmdInput(FILE *stream, const char *ask);
 /*!
  * gets a line from either the terminal or the command file stream depending on
- * g_commandFileNestingLevel > 0.  It calls cmdInput().
- * \param ask text displayed before input prompt.  This can be located in
- *   \a tempAllocStack.  If this text contains more than \a g_screenWidth
- *   characters, it is wrapped preferably at space characters and split across
- *   multiple lines.  The final line leaves space for enough for a ten
- *   character user input
- * \return the entered input.
+ * g_commandFileNestingLevel > 0.  It calls cmdInput(), i.e some input lines
+ * may be interpreted and not returned to the caller.  The conditions for this
+ * are given in \a cmdInput, except that \a localScrollMode is fixed to 1.
+ * \param ask (not null) text displayed before input prompt.  This can be
+ *   located in \a tempAllocStack.  If this text contains more than
+ *   \a g_screenWidth characters, it is wrapped preferably at space characters
+ *   and split across multiple lines.  If the final line contains spaces in the
+ *   range from position 1 to \a g_screenWidth - 11, it is wrapped such, that
+ *   it leaves enough space for ten character user input.
+ *   \n
+ *   If the prompt needs to be displayed again, only the last line after
+ *   wrapping is reprinted.
+ * \return not interpreted input.
+ * \post
+ *   \a localScrollMode is set to 1
  * \warning the calling program must deallocate the returned string.
  */
 vstring cmdInput1(const char *ask);

From 50bd232618228177f9822d244ee84a8528a6f061 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Thu, 3 Mar 2022 20:34:38 +0100
Subject: [PATCH 02/42] copy preconditions of cmdInput to cmdInput1

---
 src/mminou.h | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/mminou.h b/src/mminou.h
index bbba6b0a..d0851dea 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -196,6 +196,19 @@ vstring cmdInput(FILE *stream, const char *ask);
  *   If the prompt needs to be displayed again, only the last line after
  *   wrapping is reprinted.
  * \return not interpreted input.
+ * \pre
+ *   The following variables are honored during execution and should be properly
+ *   set:
+ *   - \a commandFileSilentFlag value 1 suppresses prompts altogether, not only
+ *     those used for scrolling through long text;
+ *   - \a g_commandFileNestingLevel a value > 0 indicates a SUBMIT call is
+ *     executing, where scrolling prompts are suppressed;
+ *   - \a g_outputToString value 1 renders scrolling as pointless and disables it;
+ *   - \a backBuffer may contain text to display on scroll back operations;
+ *   - \a g_scrollMode value 1 enables scrolling back through text held in
+ *     \a backBuffer;
+ *   - \a g_commandPrompt if this string matches ask, top level user input is
+ *     assumed.
  * \post
  *   \a localScrollMode is set to 1
  * \warning the calling program must deallocate the returned string.

From 4804d23ccd33bcd7fdb3d3fe50010d0dbfdcf973 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Thu, 3 Mar 2022 21:04:21 +0100
Subject: [PATCH 03/42] fix description of return in cmdInput

---
 src/mminou.h | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/mminou.h b/src/mminou.h
index d0851dea..f65819eb 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -35,9 +35,9 @@ extern vstring g_printString;
 /* Global variables used by cmdInput() */
 /*!
  * \def MAX_COMMAND_FILE_NESTING
- * limits number of nested SUBMIT calls to 10.  A SUBMIT redirects the input
- * to file, which in turn may temporarily redirect input to another file, and
- * so on.
+ * limits number of nested SUBMIT calls.  A SUBMIT redirects the input to a
+ * file, which in turn may temporarily redirect input to another file, and so
+ * on.
  */
 #define MAX_COMMAND_FILE_NESTING 10
 /*!
@@ -152,8 +152,9 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
  *   It may be compared to \a g_commandPrompt.  If both match, it is inferred
  *   the user is in top level command mode, where empty input is not returned
  *   to the caller.
- * \return a \a vstring containing the read (or interpreted) line.  The result
- *   needs to be deallocated by the caller, if not empty or  NULL.
+ * \return a \a vstring containing the first read and not interpreted line.
+ *   NULL indicates an error condition.  The result needs to be deallocated by
+ *   the caller, if not empty or NULL.
  * \pre
  *   The following variables are honored during execution and should be properly
  *   set:
@@ -182,10 +183,10 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
  */
 vstring cmdInput(FILE *stream, const char *ask);
 /*!
- * gets a line from either the terminal or the command file stream depending on
- * g_commandFileNestingLevel > 0.  It calls cmdInput(), i.e some input lines
- * may be interpreted and not returned to the caller.  The conditions for this
- * are given in \a cmdInput, except that \a localScrollMode is fixed to 1.
+ * gets a line from either stdin or the command file stream depending on
+ * \a g_commandFileNestingLevel.  It uses \a cmdInput(), i.e some input
+ * lines may be interpreted and not returned to the caller.  The conditions for
+ * this are listed in \a cmdInput, except that \a localScrollMode is fixed to 1.
  * \param ask (not null) text displayed before input prompt.  This can be
  *   located in \a tempAllocStack.  If this text contains more than
  *   \a g_screenWidth characters, it is wrapped preferably at space characters

From 254c77c9c25aade07111fbe63e5db1a1281348e8 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Thu, 3 Mar 2022 21:18:02 +0100
Subject: [PATCH 04/42] document the role of CTRL-D in cmdInput

---
 src/mminou.h | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/mminou.h b/src/mminou.h
index f65819eb..373890f5 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -112,9 +112,10 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
  * supported in the current implementation and may or may not cause an error
  * message or even undefined behavior.
  *
- * Reading from an empty __stream__ (or one that is at EOF position) returns
- * NULL, not the empty string, and is formally signalled as an error.
- * Overflowing the buffer is also an error.  No truncated value is returned.
+ * Reading from an empty __stream__ (or one that is at EOF position, produced
+ * for example by CTRL-D on the console) returns NULL, not the empty string,
+ * and is formally signalled as an error.  Overflowing the buffer is also an
+ * error.  No truncated value is returned.
  *
  * This routine interprets some input without returning it to the caller under
  * following two conditions:

From 125f6528185389318fc916c3d91ea2dd44d68a0f Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 06:09:01 +0100
Subject: [PATCH 05/42] clarify some points

---
 src/mminou.c |  1 -
 src/mminou.h | 59 +++++++++++++++++++++++++++++-----------------------
 2 files changed, 33 insertions(+), 27 deletions(-)

diff --git a/src/mminou.c b/src/mminou.c
index 014f07d8..15fcb44a 100644
--- a/src/mminou.c
+++ b/src/mminou.c
@@ -651,7 +651,6 @@ vstring cmdInput(FILE *stream, const char *ask) {
   long i;
 
   while (1) { /* For "B" backup loop */
-// drucke prompt
     if (ask != NULL && !g_commandFileSilentFlag) {
       printf("%s", ask);
 #if __STDC__
diff --git a/src/mminou.h b/src/mminou.h
index 373890f5..1cf1ed0f 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -100,33 +100,33 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
  * \brief requests a line of text from the __stream__.
  *
  * If not suppressed, displays a prompt text on the screen.  Then reads a
- * line from the __stream__.  This line may be interpreted as described further
+ * line from the __stream__.  Some lines are interpreted as described further
  * below, in which case the prompt is reprinted and the next line is read.
  * Returns the first not interpreted line as a \a vstring.
  *
  * A line in the __stream__ is terminated by a LF character (0x0D) character
  * alone.  It is read, but removed from the result.  The maximum line length
- * without the LF is \a CMD_BUFFER_SIZE - 1.  Reaching EOF (end of file) is
- * equivalent to reading LF, if at least 1 byte was read before.  Note that the
- * NUL character can be part of the line.  Reading a NUL is not sufficiently
- * supported in the current implementation and may or may not cause an error
- * message or even undefined behavior.
+ * without the LF is \a CMD_BUFFER_SIZE - 1.  Reaching EOF (end of file,
+ * CTRL-D) is equivalent to reading LF, if at least 1 byte was read before.
+ * Note that the NUL character can be part of the line.  Reading a NUL is not
+ * sufficiently supported in the current implementation and may or may not
+ * cause an error message or even undefined behavior.
  *
- * Reading from an empty __stream__ (or one that is at EOF position, produced
- * for example by CTRL-D on the console) returns NULL, not the empty string,
- * and is formally signalled as an error.  Overflowing the buffer is also an
- * error.  No truncated value is returned.
+ * Reading from an empty __stream__ (or one that is at EOF position, on the
+ * console CTRL-D) returns NULL, not the empty string, and is formally
+ * signalled as an error.  Overflowing the buffer is also an error.  No
+ * truncated value is returned.
  *
  * This routine interprets some input without returning it to the caller under
  * following two conditions:
  *
  * 1. If scrolling is enabled, a line consisting of a single character b or B
- * may indicate the user wants to scroll back through saved pages of output.
- * This is handled within this routine, if possible.  If it cannot be served,
- * the b or B is returned as common user input.
+ * indicates the user wants to scroll back through saved pages of output.
+ * If it can be served, it is handled within this routine, else the b or B is
+ * returned as user input.
  *
- * 2. The user hits ENTER (only) while prompted in top level context.  The
- * empty line is not returned.
+ * 2. The user hits ENTER only while prompted in top level context.  The empty
+ * line is not returned.
  * 
  * No timeout is applied while waiting for user input from the console.
  *
@@ -159,10 +159,12 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
  * \pre
  *   The following variables are honored during execution and should be properly
  *   set:
- *   - \a commandFileSilentFlag value 1 suppresses prompts altogether, not only
- *     those used for scrolling through long text;
+ *   - \a g_commandFileSilentFlag value 1 suppresses all prompts, not only
+ *     those used for scrolling through long text.  It does not suppress error
+ *     messages;
  *   - \a g_commandFileNestingLevel a value > 0 indicates a SUBMIT call is
- *     executing, where scrolling prompts are suppressed;
+ *     executing, a read line is returned as is.  0 is seen as an interactive
+ *     mode, where read lines can be interpreted;
  *   - \a g_outputToString value 1 renders scrolling as pointless and disables it;
  *   - \a backBuffer may contain text to display on scroll back operations;
  *   - \a g_scrollMode value 1 enables scrolling back through text held in
@@ -170,7 +172,7 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
  *   - \a localScrollMode a value of 0 temporarily disables scrolling, despite
  *     the setting in \a g_scrollMode;
  *   - \a g_commandPrompt if this string matches ask, top level user input is
- *     assumed.
+ *     assumed, where empty lines are discarded.
  * \post
  *   \a db is updated.
  * \warning the calling program must deallocate the returned string (if not
@@ -195,24 +197,29 @@ vstring cmdInput(FILE *stream, const char *ask);
  *   range from position 1 to \a g_screenWidth - 11, it is wrapped such, that
  *   it leaves enough space for ten character user input.
  *   \n
- *   If the prompt needs to be displayed again, only the last line after
- *   wrapping is reprinted.
- * \return not interpreted input.
+ *   If the user is prompted again, only the last line of the wrapped text is
+ *   reprinted.
+ * \return not interpreted line.
  * \pre
  *   The following variables are honored during execution and should be properly
  *   set:
- *   - \a commandFileSilentFlag value 1 suppresses prompts altogether, not only
- *     those used for scrolling through long text;
+ *   - \a g_commandFileSilentFlag value 1 suppresses output and prompts, but
+ *     not all error messages;
  *   - \a g_commandFileNestingLevel a value > 0 indicates a SUBMIT call is
- *     executing, where scrolling prompts are suppressed;
+ *     executing, where a read line is returned as is. 0 is seen as interactive
+ *     mode, where read lines can be interpreted;
  *   - \a g_outputToString value 1 renders scrolling as pointless and disables it;
  *   - \a backBuffer may contain text to display on scroll back operations;
  *   - \a g_scrollMode value 1 enables scrolling back through text held in
  *     \a backBuffer;
+ *   - \a localScrollMode a value of 0 temporarily disables scrolling, despite
+ *     the setting in \a g_scrollMode;
  *   - \a g_commandPrompt if this string matches ask, top level user input is
- *     assumed.
+ *     assumed, and an empty line is usually discarded.
  * \post
  *   \a localScrollMode is set to 1
+ * \attention A CTRL_D can cause a return of an empty line, even if an
+ *   interactive mode is assumed
  * \warning the calling program must deallocate the returned string.
  */
 vstring cmdInput1(const char *ask);

From 60c1181a6ff3f115caa0559ecf019c4b03b7b986 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 11:20:10 +0100
Subject: [PATCH 06/42] better understand hyperlinking in doxygen

---
 src/metamath.c |   4 +-
 src/mmcmdl.h   |   4 +-
 src/mmdata.c   |  51 ++++++------
 src/mmdata.h   |  45 ++++++-----
 src/mminou.c   |   6 +-
 src/mminou.h   | 101 +++++++++++++----------
 src/mmvstr.c   |  45 ++++++-----
 src/mmvstr.h   | 213 +++++++++++++++++++++++++------------------------
 8 files changed, 244 insertions(+), 225 deletions(-)

diff --git a/src/metamath.c b/src/metamath.c
index 3d306e6e..970ce4c0 100644
--- a/src/metamath.c
+++ b/src/metamath.c
@@ -723,12 +723,12 @@ void command(int argc, char *argv[]);
 /*! \fn int main(int argc, char *argv[])
  * \brief entry point of the metamath program
  * \param argc int number of command line parameters
- * \param argv (char*)[] array of \a argc command line parameters, followed by NULL
+ * \param argv (char*)[] array of \p argc command line parameters, followed by NULL
  * \return success 0 else failure
  *
  * Running metamath
  *   ./metamath 'read set.mm' 'verify proof *'
- * will start main with \a argc set to 2, argv[0] to "read set.mm", argv[1]
+ * will start main with \p argc set to 2, argv[0] to "read set.mm", argv[1]
  * to "verify proof *" (both without quotes) and argv[2] to NULL.
  * Returning 0 indicates successful completion, anything else some kind of
  failure.
diff --git a/src/mmcmdl.h b/src/mmcmdl.h
index f997b770..ec802805 100644
--- a/src/mmcmdl.h
+++ b/src/mmcmdl.h
@@ -45,9 +45,9 @@ extern flag g_commandEcho; /* Echo full command */
 /*!
  * \brief indicates whether the user has turned MEMORY STATUS on.
  *
- * If the user issues SET MEMORY_STATUS ON this \a flag is set to 1.  It is
+ * If the user issues SET MEMORY_STATUS ON this \ref flag is set to 1.  It is
  * reset to 0 again on a SET MEMORY_STATUS OFF command.  When 1, certain
- * memory de/allocations are monitored - see \a db3.
+ * memory de/allocations are monitored - see \ref db3.
  */
 extern flag g_memoryStatus; /* Always show memory */
 
diff --git a/src/mmdata.c b/src/mmdata.c
index 91aa7a6c..4e138421 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -85,9 +85,10 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
  * During execution chunks of memory, either complete \ref block "blocks" or
  * \ref fragmentation "fragments" thereof, become free again.  The suballocator
  * adds them then to internal **pools** for reuse, one dedicated to totally
- * free blocks (\a memFreePool), the other to fragmented ones (\a memUsedPool).
- * We call these pools **free block array** and **used block array** in this
- * documentation.  Fully occupied blocks are not tracked by the suballocator.
+ * free blocks (\ref memFreePool), the other to fragmented ones
+ * (\ref memUsedPool).  We call these pools **free block array** and
+ * **used block array** in this documentation.  Fully occupied blocks are not
+ * tracked by the suballocator.
  *
  * Although the suballocator tries to avoid returning memory to the system, it
  * can do so under extreme memory constraints, or when built-in limits are
@@ -139,7 +140,7 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
  * offset -3:\n
  *   If this block has free space at the end (is \ref fragmentation
  *   "fragmented"), then it contains its index in the used blocks array, see
- *   \a memUsedPool.  A value of -1 indicates it is either fully occupied or
+ *   \ref memUsedPool.  A value of -1 indicates it is either fully occupied or
  *   totally free.  In any of these cases it is not kept in the used blocks
  *   array.
  */
@@ -152,8 +153,8 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
  * In Metamath a pool has no gaps in between.
  *
  * The \ref suballocation "suballocator" uses two pools:
- * - the **free block array** pointed to by \a memFreePool;
- * - the **used block array** pointed to by \a memUsedPool.
+ * - the **free block array** pointed to by \ref memFreePool;
+ * - the **used block array** pointed to by \ref memUsedPool.
  */
 
 /*! \page stack Temporary Allocated Memory
@@ -202,8 +203,8 @@ long poolAbsoluteMax = 1000000; /* Pools will be purged when this is reached */
 /*!
  * \var long poolTotalFree
  * contains the number of free space available in bytes, in both pools
- * \a memFreePool and \a memUsedPool, never counting the hidden headers at the
- * beginning of each block, see \ref block.
+ * \ref memFreePool and \ref memUsedPool, never counting the hidden headers at
+ * the beginning of each block, see \ref block.
  */
 long poolTotalFree = 0; /* Total amount of free space allocated in pool */
 /*E*/long i1,j1_,k1; /* 'j1' is a built-in function */
@@ -224,7 +225,7 @@ long poolTotalFree = 0; /* Total amount of free space allocated in pool */
  *
  * The used block array may only be partially occupied, in which case elements
  * at the end of the array are unused.  Its current usage is given by
- * \a memUsedPoolSize.  Its capacity is given by \a memUsedPoolMax.
+ * \ref memUsedPoolSize.  Its capacity is given by \ref memUsedPoolMax.
  *
  * \invariant Each block in the used blocks array has its index noted in its
  * hidden header, for backward reference.
@@ -241,9 +242,9 @@ void **memUsedPool = NULL;
  * The Metamath suballocator holds fragmented blocks in a used block array.
  * The number of occupied entries is kept in this variable.  Elements at the
  * end of the used block array may be unused.  The fill size is given by this
- * variable.  For further information see \a memUsedPool.
+ * variable.  For further information see \ref memUsedPool.
  *
- * \invariant memUsedPoolSize <= \a memUsedPoolMax.
+ * \invariant memUsedPoolSize <= \ref memUsedPoolMax.
  */
 long memUsedPoolSize = 0; /* Current # of partially filled arrays in use */
 /*!
@@ -253,11 +254,11 @@ long memUsedPoolSize = 0; /* Current # of partially filled arrays in use */
  *
  * The Metamath suballocator holds fragmented blocks in the used block
  * array.  This array may only partially be occupied.  Its total capacity is
- * kept in this variable.  For further information see \a memUsedPool.
+ * kept in this variable.  For further information see \ref memUsedPool.
  *
  * This variable may grow during a reallocation process.
  *
- * \invariant (memUsedPoolMax > 0) == (\a memUsedPool != 0)
+ * \invariant (memUsedPoolMax > 0) == (\ref memUsedPool != 0)
  */
 long memUsedPoolMax = 0; /* Maximum # of entries in 'in use' table (grows
                                as necessary) */
@@ -274,9 +275,9 @@ long memUsedPoolMax = 0; /* Maximum # of entries in 'in use' table (grows
  * The **free block array** contains only totally free \ref block "blocks".
  * This array may only be partially occupied, in which case the elements at the
  * end are the unused ones.  Its current fill size is given by
- * \a memFreePoolSize.  Its capacity is given by \a memFreePoolMax.
+ * \ref memFreePoolSize.  Its capacity is given by \ref memFreePoolMax.
  *
- * Fragmented blocks are kept in a separate \a memUsedPool.  The suballocator
+ * Fragmented blocks are kept in a separate \ref memUsedPool.  The suballocator
  * never tracks fully used blocks.
  */
 void **memFreePool = NULL;
@@ -288,9 +289,9 @@ void **memFreePool = NULL;
  * The Metamath suballocator holds free blocks in a free block array.  The
  * number of occupied entries is kept in this variable.  Elements at the end of
  * the free block array may not be used.  The fill size is given by this
- * variable.  For further information see \a memFreePool.
+ * variable.  For further information see \ref memFreePool.
  *
- * \invariant memFreePoolSize <= \a memFreePoolMax.
+ * \invariant memFreePoolSize <= \ref memFreePoolMax.
  */
 long memFreePoolSize = 0; /* Current # of available, allocated arrays */
 /*!
@@ -300,11 +301,11 @@ long memFreePoolSize = 0; /* Current # of available, allocated arrays */
  *
  * The Metamath suballocator holds free blocks in a **free block array**.  It
  * may only be partially occupied.  Its total capacity is kept in this variable.  For
- * further information see \a memFreePool.
+ * further information see \ref memFreePool.
  *
  * This variable may grow during a reallocation process.
  *
- * \invariant (memFreePoolMax > 0) == (\a memFreePool != 0)
+ * \invariant (memFreePoolMax > 0) == (\ref memFreePool != 0)
  */
 long memFreePoolMax = 0; /* Maximum # of entries in 'free' table (grows
                                as necessary) */
@@ -2414,10 +2415,10 @@ long g_pntrStartTempAllocStack = 0;   /* Where to start freeing temporary alloca
                                     special nested vstring functions) */
 /*!
  * \var pntrTempAllocStack
- * \brief a \ref stack "stack" of \a temp_pntrString.
+ * \brief a \ref stack "stack" of \ref temp_pntrString.
  *
- * Holds pointers to temporarily allocated data of type \a pntrString.  Such a
- * \ref stack "stack" contains strictly __local__ data of a function, not
+ * Holds pointers to temporarily allocated data of type \ref pntrString.  Such
+ * a \ref stack "stack" contains strictly __local__ data of a function, not
  * accessed from outer levels.
  */
 pntrString *pntrTempAllocStack[M_MAX_ALLOC_STACK];
@@ -2665,8 +2666,8 @@ void pntrZapLen(pntrString *s, long length) {
 /* Copy a string to another (pre-allocated) string */
 /* Dangerous for general purpose use */
 /*!
- * \brief copies a null pointer terminated \a pntrString to a destination
- * \a pntrString.
+ * \brief copies a null pointer terminated \ref pntrString to a destination
+ * \ref pntrString.
  *
  * This function determines the length of the source \p t by scanning for a
  * terminating null pointer element.  The destination \p s must have enough
@@ -2687,7 +2688,7 @@ void pntrZapLen(pntrString *s, long length) {
  *   - \p t is terminated by the first null pointer element.
  *   - the target array \p s must have enough free space to hold the source array
  *     \p t including the terminal null pointer.
- *   - \p s and \p t can overlap if \p t points to a later element than \a s
+ *   - \p s and \p t can overlap if \p t points to a later element than \p s
  *     (move left semantics)
  * \invariant
  *   If \p s is contained in a \ref block "block", its administrative header is
diff --git a/src/mmdata.h b/src/mmdata.h
index 48002cc7..edf0b98f 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -19,9 +19,9 @@
  * \brief bytes held by vstring instances outside of the stack of temporaries
  *
  * monitors the number of bytes (including the terminal NUL) currently used in
- * all \a vstring pointer variables OUTSIDE of the \a tempAllocStack.  Note:
- * This is NOT the number of bytes allocated, but the portion actually used!  A
- * few memory allocations are also included:
+ * all \ref vstring pointer variables OUTSIDE of the \ref tempAllocStack.
+ * Note: This is NOT the number of bytes allocated, but the portion actually
+ * used!  A few memory allocations are also included:
  * - command line buffers used to hold user input from a console;
  * - buffers used to read file contents in.
  *
@@ -34,8 +34,8 @@
  * \var db1
  * \brief bytes held by vstring instances inside of the stack of temporaries
  *
- * monitors the number of bytes currently pointed to by \a vstring pointers
- * INSIDE the \a tempAllocStack.  Note: This is NOT their capacity, but the
+ * monitors the number of bytes currently pointed to by \ref vstring pointers
+ * INSIDE the \ref tempAllocStack.  Note: This is NOT their capacity, but the
  * portion actually used!
  *
  * Not updated if NDEBUG (usually deactivates asserts in C code) is defined.
@@ -90,17 +90,17 @@ typedef char flag;
  * Obsolete.  Now fixed to 0.  Historically the metamath sources were also used
  * for other purposes than maintaining Metamath files.  One such application, a
  * standalone text processor, was LIST.EXE.  The sources still query this
- * \a flag occasionally, but its value is in fact fixed to 0 in metamath,
+ * \ref flag occasionally, but its value is in fact fixed to 0 in metamath,
  * meaning the LIST.EXE functionality is an integral part of metamath now.
  */
 extern flag g_listMode; /* 0 = metamath, 1 = list utility */
 /*!
  * \var g_toolsMode
  * Metamath has two modes of operation: In its primary mode it handles
- * mathematical contents like proofs.  In this mode \a g_toolsMode  is set to
+ * mathematical contents like proofs.  In this mode \ref g_toolsMode  is set to
  * 0.  This is the value assigned on startup.  A second mode is enabled after
  * executing the 'tools' command.  In this mode text files are processed using
- * high level commands.  It is indicated by a 1 in \a g_toolsMode.
+ * high level commands.  It is indicated by a 1 in \ref g_toolsMode.
  */
 extern flag g_toolsMode; /* In metamath mode:  0 = metamath, 1 = tools */
 
@@ -137,7 +137,7 @@ typedef nmbrString temp_nmbrString;
 
 /*!
  * \typedef temp_pntrString
- * \brief a single \a pntrString element for use in a \ref stack "stack".
+ * \brief a single \ref pntrString element for use in a \ref stack "stack".
  *
  * These elements are pushed onto and popped off a \ref stack 
  * "stack of temporary data".  Special commands can free all pointers on and
@@ -305,7 +305,8 @@ void memFreePoolPurge(flag untilOK);
  * Return the overall statistics about the pools \ref memFreePool
  * "free block array" and the \ref memUsedPool "used block array".  In MEMORY
  * STATUS mode ON, a diagnostic message compares the the contents of
- * \a poolTotalFree to the values found in this statistics.  They should not differ!
+ * \ref poolTotalFree to the values found in this statistics.  They should not
+ * differ!
  *
  * \attention This is NOT full memory usage, because completely used
  * \ref block "blocks" are not tracked!
@@ -369,7 +370,7 @@ extern struct nullNmbrStruct g_NmbrNull;
 
 /*!
  * \struct nullPntrStruct
- * describing a \ref block of \a pntrString containing only the null
+ * describing a \ref block of \ref pntrString containing only the null
  * pointer.  Besides this pointer it is accompanied with a header containing
  * the hidden administrative values of such \ref block "block".
  *
@@ -387,14 +388,14 @@ struct nullPntrStruct {
      */
     long poolLoc;
     /*!
-     * allocated size of the memory block containing the \a pntrString,
+     * allocated size of the memory block containing the \ref pntrString,
      * excluding any hidden administrative data.
      * Note: this is the number of bytes, not elements!  Fixed to the size of a
      * single void* instance.
      */
     long allocSize;
     /*!
-     * currently used size of the memory block containing the \a pntrString,
+     * currently used size of the memory block containing the \ref pntrString,
      * excluding any hidden administrative data.
      * Note: this is the number of bytes, not elements!  Fixed to the size of a
      * single pointer element.
@@ -408,9 +409,9 @@ struct nullPntrStruct {
 /*!
  * \var g_PntrNull
  * Global instance of a memory block structured like a
- * \a pntrString, fixed in size and containing always exactly one null pointer
+ * \ref pntrString, fixed in size and containing always exactly one null pointer
  * element, the terminating NULL.  This setup is recognized as an empty
- * \a pntrString.
+ * \ref pntrString.
  *
  * \attention mark as const
  */
@@ -418,15 +419,15 @@ extern struct nullPntrStruct g_PntrNull;
 /*!
  * \def NULL_PNTRSTRING
  * The address of a \ref block "block" containing an empty, not resizable
- * \a pntrString
- * stack.  Used to initialize \a pntrString variables .
+ * \ref pntrString
+ * stack.  Used to initialize \ref pntrString variables .
  */
 #define NULL_PNTRSTRING &(g_PntrNull.nullElement)
 /*!
  * \def pntrString_def
  *
- * declare a new \a pntrString variable and initialize it to point to a block
- * with an empty, not resizable \a pntrString.
+ * declare a new \ref pntrString variable and initialize it to point to a block
+ * with an empty, not resizable \ref pntrString.
  *
  * \param[in] x variable name
  * \pre The variable does not exist in the current scope.
@@ -592,7 +593,7 @@ long compressedProofSize(const nmbrString *proof, long statemNum);
 /*!
  * \var long g_pntrTempAllocStackTop
  *
- * Index of the current top af the \ref stack "stack" \a pntrTempAlloc.
+ * Index of the current top af the \ref stack "stack" \ref pntrTempAlloc.
  * New data is pushed from this location on if space available.
  *
  * \invariant always refers the null pointer element behind the valid data.
@@ -644,7 +645,7 @@ temp_pntrString *pntrPSpace(long n);
  * derived from administrative data in the surrounding block.
  *
  * \attention This is not the capacity of the array.
- * \param[in] s points to a element 0 of a \a pntrString  embedded in a block
+ * \param[in] s points to a element 0 of a \ref pntrString  embedded in a block
  * \return the number of pointers currently in use in the array pointed to by \p s.
  * \pre the array pointed to by s is the sole user of a \ref block "block".
  */
@@ -657,7 +658,7 @@ long pntrLen(const pntrString *s);
  * derived from administrative data in the surrounding block.  The result
  * excludes the terminal element reserved for a null pointer.
  *
- * \param[in] s points to a element 0 of a \a pntrString  embedded in a block
+ * \param[in] s points to a element 0 of a \ref pntrString embedded in a block
  * \return the maximal number of pointers that can be used in the array pointed
  * to by \p s.
  * \pre the array pointed to by s is the sole user of a \ref block "block".
diff --git a/src/mminou.c b/src/mminou.c
index 15fcb44a..484d5080 100644
--- a/src/mminou.c
+++ b/src/mminou.c
@@ -67,7 +67,7 @@ flag g_quitPrint = 0; /* Flag that user quit the output */
 /*!
  * \var flag localScrollMode
  *
- * temporarily disables prompted scroll (see \a g_scrollMode) until next user
+ * temporarily disables prompted scroll (see \ref g_scrollMode) until next user
  * prompt
  */
 flag localScrollMode = 1; /* 0 = Scroll continuously only till next prompt */
@@ -85,9 +85,9 @@ pntrString_def(backBuffer);
 /*!
  * \var backBufferPos
  *
- * A position within the \a backBuffer.
+ * A position within the \ref backBuffer.
  *
- * \invariant The value 0 requires an empty \a backBuffer.
+ * \invariant The value 0 requires an empty \ref backBuffer.
  */
 long backBufferPos = 0;
 flag backFromCmdInput = 0; /* User typed "B" at main prompt */
diff --git a/src/mminou.h b/src/mminou.h
index 1cf1ed0f..1baf245a 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -26,9 +26,8 @@ extern FILE *g_listFile_fp;
 /* Global variables used by print2() */
 /*!
  * \var g_outputToString
- * 
  * Global variable redirecting the output of the function print2 from the
- * console ( = 0) to a string ( = 1).
+ * console ( = 0) to a string ( = 1).  Initialized to 0 on program start.
  */
 extern flag g_outputToString;
 extern vstring g_printString;
@@ -45,14 +44,23 @@ extern vstring g_printString;
  * current level of nested SUBMIT commands.  0 is top level and refers to stdin
  * (usually the user controlled command line).  Any invocation of SUBMIT
  * increases this value by 1.  A return from a SUBMIT decrases it by 1 again.
+ * Limited by \ref MAX_COMMAND_FILE_NESTING.
  */
 extern long g_commandFileNestingLevel;
+/*!
+ * \var FILE *g_commandFilePtr[MAX_COMMAND_FILE_NESTING + 1]
+ * file descriptors pointing to files invoked by SUBMIT commands.  The 0-th
+ * element is fixed to stdin, and neither used nor assigned to.  Other
+ * elements, up to the current value of \ref g_commandFileNestingLevel, are
+ * valid, and point to opened files.
+ */
 extern FILE *g_commandFilePtr[MAX_COMMAND_FILE_NESTING + 1];
 extern vstring g_commandFileName[MAX_COMMAND_FILE_NESTING + 1];
 extern flag g_commandFileSilent[MAX_COMMAND_FILE_NESTING + 1];
 /*!
  * \var g_commandFileSilentFlag
- * If set to 1, suppresses prompts on input.
+ * If set to 1, suppresses prompts on input.  Activated through
+ * SUBMIT ... /SILENT commands.  Initialized to 0 on program start.
  */
 extern flag g_commandFileSilentFlag; /* For SUBMIT ... /SILENT */
 
@@ -97,22 +105,22 @@ extern flag g_quitPrint; /* Flag that user typed 'q' to last scrolling prompt */
 /* printLongLine automatically puts a newline \n in the output line. */
 void printLongLine(const char *line, const char *startNextLine, const char *breakMatch);
 /*!
- * \brief requests a line of text from the __stream__.
+ * \brief requests a line of text from the \p stream.
  *
  * If not suppressed, displays a prompt text on the screen.  Then reads a
- * line from the __stream__.  Some lines are interpreted as described further
+ * line from the \p stream.  Some lines are interpreted as described further
  * below, in which case the prompt is reprinted and the next line is read.
- * Returns the first not interpreted line as a \a vstring.
+ * Returns the first not interpreted line as a \ref vstring.
  *
- * A line in the __stream__ is terminated by a LF character (0x0D) character
+ * A line in the \p stream is terminated by a LF character (0x0D) character
  * alone.  It is read, but removed from the result.  The maximum line length
- * without the LF is \a CMD_BUFFER_SIZE - 1.  Reaching EOF (end of file,
+ * without the LF is \ref CMD_BUFFER_SIZE - 1.  Reaching EOF (end of file,
  * CTRL-D) is equivalent to reading LF, if at least 1 byte was read before.
  * Note that the NUL character can be part of the line.  Reading a NUL is not
  * sufficiently supported in the current implementation and may or may not
  * cause an error message or even undefined behavior.
  *
- * Reading from an empty __stream__ (or one that is at EOF position, on the
+ * Reading from an empty \p stream (or one that is at EOF position, on the
  * console CTRL-D) returns NULL, not the empty string, and is formally
  * signalled as an error.  Overflowing the buffer is also an error.  No
  * truncated value is returned.
@@ -145,79 +153,84 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
  * \todo clarify recursive call to print2 and the role of backFromCmdInput. 
  * \param[in] stream (not null) source to read the line from.  _stdin_ is
  *   common for user input from the console. 
- * \param[in] ask prompt text displayed on the screen before __stream__ is
+ * \param[in] ask prompt text displayed on the screen before \p stream is
  *   read.  This prompt is suppressed by either a NULL value, or setting 
- *   \a g_commandFileSilentFlag to 1.  This prompt must be not NULL (empty is
+ *   \ref g_commandFileSilentFlag to 1.  This prompt must be not NULL (empty is
  *   fine!) outside of a SUBMIT call, where user is expected to enter input.
  *   \n
- *   It may be compared to \a g_commandPrompt.  If both match, it is inferred
+ *   It may be compared to \ref g_commandPrompt.  If both match, it is inferred
  *   the user is in top level command mode, where empty input is not returned
  *   to the caller.
- * \return a \a vstring containing the first read and not interpreted line.
+ * \return a \ref vstring containing the first read and not interpreted line.
  *   NULL indicates an error condition.  The result needs to be deallocated by
  *   the caller, if not empty or NULL.
  * \pre
  *   The following variables are honored during execution and should be properly
  *   set:
- *   - \a g_commandFileSilentFlag value 1 suppresses all prompts, not only
+ *   - \ref g_commandFileSilentFlag value 1 suppresses all prompts, not only
  *     those used for scrolling through long text.  It does not suppress error
  *     messages;
- *   - \a g_commandFileNestingLevel a value > 0 indicates a SUBMIT call is
+ *   - \ref g_commandFileNestingLevel a value > 0 indicates a SUBMIT call is
  *     executing, a read line is returned as is.  0 is seen as an interactive
  *     mode, where read lines can be interpreted;
- *   - \a g_outputToString value 1 renders scrolling as pointless and disables it;
- *   - \a backBuffer may contain text to display on scroll back operations;
- *   - \a g_scrollMode value 1 enables scrolling back through text held in
- *     \a backBuffer;
- *   - \a localScrollMode a value of 0 temporarily disables scrolling, despite
- *     the setting in \a g_scrollMode;
- *   - \a g_commandPrompt if this string matches ask, top level user input is
+ *   - \ref g_outputToString value 1 renders scrolling as pointless and
+ *     disables it;
+ *   - \ref backBuffer may contain text to display on scroll back operations;
+ *   - \ref g_scrollMode value 1 enables scrolling back through text held in
+ *     \ref backBuffer;
+ *   - \ref localScrollMode a value of 0 temporarily disables scrolling,
+ *     overriding the setting in \ref g_scrollMode;
+ *   - \ref g_commandPrompt if this string matches ask, top level user input is
  *     assumed, where empty lines are discarded.
  * \post
- *   \a db is updated.
+ *   \ref db is updated.
  * \warning the calling program must deallocate the returned string (if not
  *   null or empty).  Note that the result can be NULL.  This is outside of the
- *   usual behavior of a \a vstring type.
+ *   usual behavior of a \ref vstring type.
  * \warning the returned string need not be valid ASCII or UTF-8.
- * \bug If a character read from __stream__ is NUL, this may sometimes cause a
+ * \bug If a character read from \p stream is NUL, this may sometimes cause a
  *   print of an error message, but execution continues and in the wake may
  *   cause all kind of undefined behavior, like memory accesses beyond
  *   allocated buffers.
  */
 vstring cmdInput(FILE *stream, const char *ask);
 /*!
+ * \brief print explanatory text and then read a line.
+ *
  * gets a line from either stdin or the command file stream depending on
- * \a g_commandFileNestingLevel.  It uses \a cmdInput(), i.e some input
- * lines may be interpreted and not returned to the caller.  The conditions for
- * this are listed in \a cmdInput, except that \a localScrollMode is fixed to 1.
+ * \ref g_commandFileNestingLevel.  If this value is 0, interactive input is
+ * assumed, else It uses \ref cmdInput(), i.e some input lines may be
+ * interpreted and not returned to the caller.  The conditions for this are
+ * listed in \ref cmdInput, except that \ref localScrollMode is fixed to 1.
  * \param ask (not null) text displayed before input prompt.  This can be
- *   located in \a tempAllocStack.  If this text contains more than
- *   \a g_screenWidth characters, it is wrapped preferably at space characters
- *   and split across multiple lines.  If the final line contains spaces in the
- *   range from position 1 to \a g_screenWidth - 11, it is wrapped such, that
+ *   located in \ref tempAllocStack.  If this text contains more than
+ *   \ref g_screenWidth characters, it is wrapped preferably at spaces and
+ *   split across multiple lines.  If the final line contains spaces in the
+ *   range from position 1 to \ref g_screenWidth - 11, it is wrapped such, that
  *   it leaves enough space for ten character user input.
  *   \n
- *   If the user is prompted again, only the last line of the wrapped text is
- *   reprinted.
+ *   If the user is prompted again, only the last line of the wrapped text in
+ *   \p ask is reprinted.
  * \return not interpreted line.
  * \pre
  *   The following variables are honored during execution and should be properly
  *   set:
- *   - \a g_commandFileSilentFlag value 1 suppresses output and prompts, but
+ *   - \ref g_commandFileSilentFlag value 1 suppresses output and prompts, but
  *     not all error messages;
- *   - \a g_commandFileNestingLevel a value > 0 indicates a SUBMIT call is
+ *   - \ref g_commandFileNestingLevel a value > 0 indicates a SUBMIT call is
  *     executing, where a read line is returned as is. 0 is seen as interactive
  *     mode, where read lines can be interpreted;
- *   - \a g_outputToString value 1 renders scrolling as pointless and disables it;
- *   - \a backBuffer may contain text to display on scroll back operations;
- *   - \a g_scrollMode value 1 enables scrolling back through text held in
- *     \a backBuffer;
- *   - \a localScrollMode a value of 0 temporarily disables scrolling, despite
- *     the setting in \a g_scrollMode;
- *   - \a g_commandPrompt if this string matches ask, top level user input is
+ *   - \ref g_outputToString value 1 renders scrolling as pointless and
+ *     disables it;
+ *   - \ref backBuffer may contain text to display on scroll back operations;
+ *   - \ref g_scrollMode value 1 enables scrolling back through text held in
+ *     \ref backBuffer;
+ *   - \ref localScrollMode a value of 0 temporarily disables scrolling,
+ *     overriding the setting in \ref g_scrollMode;
+ *   - \ref g_commandPrompt if this string matches ask, top level user input is
  *     assumed, and an empty line is usually discarded.
  * \post
- *   \a localScrollMode is set to 1
+ *   \ref localScrollMode is set to 1
  * \attention A CTRL_D can cause a return of an empty line, even if an
  *   interactive mode is assumed
  * \warning the calling program must deallocate the returned string.
diff --git a/src/mmvstr.c b/src/mmvstr.c
index 9f0f0796..9392d4c8 100644
--- a/src/mmvstr.c
+++ b/src/mmvstr.c
@@ -32,7 +32,7 @@ This is an emulation of the string functions available in VMS BASIC.
 /*E*/long db1=0;
 /*!
  * \def INCDB1
- * updates \a db1 if NDEBUG is not defined, is a no operation else.
+ * updates \ref db1 if NDEBUG is not defined, is a no operation else.
  *
  * NDEBUG switches C assert instructions off or on.  So the handling of db1 is
  * aligned with assert().
@@ -46,9 +46,9 @@ This is an emulation of the string functions available in VMS BASIC.
 /*!
  * \def MAX_ALLOC_STACK
  *
- * The number of \a vstring pointers set aside for temporary string evaluation.
- * This number covers the needs of ordinary nested functions but it puts a
- * limit to recurrent calls.
+ * The number of \ref vstring pointers set aside for temporary string
+ * evaluation.  This number covers the needs of ordinary nested functions but
+ * it puts a limit to recurrent calls.
  *
  * The number given here is one greater than actually available.  One entry is
  * reserved for the terminal null pointer marking the top of stack.
@@ -61,20 +61,20 @@ long g_startTempAllocStack = 0;    /* Where to start freeing temporary allocatio
 /*!
  * \brief stack for temporary text.
  *
- * This \ref stack "stack" contains \a vstring pointers holding temporary text
- * like fragments, boilerplate and so on.  The current top of the stack is
- * \a g_tempAllocStackTop.  Nested functions share this stack, each setting
+ * This \ref stack "stack" contains \ref vstring pointers holding temporary
+ * text like fragments, boilerplate and so on.  The current top of the stack is
+ * \ref g_tempAllocStackTop.  Nested functions share this stack, each setting
  * aside its own scope.  The scope of the most nested function begins at index
- * \a g_startTempAllocStack.
+ * \ref g_startTempAllocStack.
  *
- * When a nested function starts execution, it saves \a g_startTempAllocStack
- * and copies the \a g_tempAllocStackTop into it, marking the begin of its own
+ * When a nested function starts execution, it saves \ref g_startTempAllocStack
+ * and copies the \ref g_tempAllocStackTop into it, marking the begin of its own
  * scope of temporaries.  Before returning, both values are restored again.
  *
  * The scope of top level functions begins at index 0
  *.
  * \invariant
- * - The entry at \a g_tempAllocStackTop is NULL.
+ * - The entry at \ref g_tempAllocStackTop is NULL.
  */
 void *tempAllocStack[MAX_ALLOC_STACK];
 
@@ -93,10 +93,10 @@ void freeTempAlloc(void) {
 
 /*!
  * \fn pushTempAlloc(void *mem)
- * \brief pushes a pointer onto the \a tempAllocStack.
+ * \brief pushes a pointer onto the \ref tempAllocStack.
  *
- * In case of a stack overflow \a bug is called.  This function is low level
- * that does not ensure that invariants of \a tempAllocStack are kept.
+ * In case of a stack overflow \ref bug is called.  This function is low level
+ * that does not ensure that invariants of \ref tempAllocStack are kept.
  *
  * \param mem (not null) points to either a non-mutable empty string, or
  *   to allocated memory.  Its contents need not be valid yet, although it is
@@ -104,10 +104,10 @@ void freeTempAlloc(void) {
  * \pre
  *   The stack must not be full.
  * \post
- *   If not full, \a mem is added on top of \a tempAllocStack, and
- *   \a g_tempAllocStackTop is increased.  This function
+ *   If not full, \p mem is added on top of \ref tempAllocStack, and
+ *   \ref g_tempAllocStackTop is increased.  This function
  *   does not ensure a NULL pointer follows the pushed pointer.  Statistics in
- *   \a db1 is not updated.
+ *   \ref db1 is not updated.
  * \warning
  *   In case of stack overflow, the caller is not notified and a memory leak
  *   is likely.
@@ -127,19 +127,20 @@ static void pushTempAlloc(void *mem)
 /*!
  * \fn tempAlloc(long size)
  *
- * \brief allocates memory for size bytes and pushes it onto the \a tempAllocStack
+ * \brief allocates memory for size bytes and pushes it onto the
+ *   \ref tempAllocStack
  *
  * This low level function does NOT initialize the allocated memory.  If the
- * allocation on the heap fails, \a bug is called.  The statistic value \a db1
- * is updated.
+ * allocation on the heap fails, \ref bug is called.  The statistic value
+ * \ref db1 is updated.
  *
  * \param size (> 0) number of bytes to allocate on the heap.  If the memory is
  *   intended to hold NUL terminated text, then size must account for the final
  *   NUL character, too.
  * \pre
- *   The \a tempAllocStack must not be full.
+ *   The \ref tempAllocStack must not be full.
  * \post
- *   The top of \a tempAllocStack addresses memory at least the size of the
+ *   The top of \ref tempAllocStack addresses memory at least the size of the
  *   submitted parameter.
  * \warning
  *   In case of stack overflow, the caller is not notified and a memory leak
diff --git a/src/mmvstr.h b/src/mmvstr.h
index 6957856c..21f9468a 100644
--- a/src/mmvstr.h
+++ b/src/mmvstr.h
@@ -138,7 +138,7 @@ for memory allocation. New vstrings should always be constructed from the
  *   character, then its contents is not allocated memory and not mutable
  *   instead;
  * - If not empty, i.e. the pointer points to a character different from
- *   0x00, then this is never a true left portion of another \a vstring.
+ *   0x00, then this is never a true left portion of another \ref vstring.
  * - Although not required under all circumstances, it is highly recommended to
  *   uniquely point to some allocated memory only.
  *
@@ -195,23 +195,23 @@ typedef char* vstring;
 /*!
  * \typedef temp_vstring
  *
- * This alias for \a vstring is used to mark an entry in the \a tempAllocStack.
- * Entries in this stack are subject to automatic deallocation by \a let or
- * calling \a freeTempAlloc.
+ * This alias for \ref vstring is used to mark an entry in the
+ * \ref tempAllocStack.  Entries in this stack are subject to automatic
+ * deallocation by \ref let or \ref freeTempAlloc.
  *
- * Unlike \a vstring this type knows no exceptional handling of empty strings.
- * If an empty string is generated as a temporary in the course of a
- * construction of a final \a vstring, it is allocated on the heap as usual.
+ * Unlike \ref vstring this type knows no exceptional handling of empty
+ * strings.  If an empty string is generated as a temporary in the course of a
+ * construction of a final \ref vstring, it is allocated on the heap as usual.
  *
- * If returned by a function, it is already pushed on the \a tempAllocStack.
+ * If returned by a function, it is already pushed on the \ref tempAllocStack.
  */
 typedef vstring temp_vstring;
 
 /*!
  * \def vstring_def
- * \brief creates a new \a vstring variable.
+ * \brief creates a new \ref vstring variable.
  *
- * declares a \a vstring variable and initiates it with empty text ("").
+ * declares a \ref vstring variable and initiates it with empty text ("").
  * If it remains unmodified, freeing of __x__ is possible, but not required.
  *
  * \param[in] x plain C variable name without quote characters.
@@ -219,27 +219,27 @@ typedef vstring temp_vstring;
  *   the variable has not been declared before in the current scope.
  * \post
  *   initialized with empty text.  No administrative data is added, in
- *   conformance with the semantics of a \a vstring.
+ *   conformance with the semantics of a \ref vstring.
  */
 #define vstring_def(x) vstring x = ""
 /*!
  * \def free_vstring
- * \brief deallocates a \a vstring variable and sets it to the empty string.
+ * \brief deallocates a \ref vstring variable and sets it to the empty string.
  *
  * Multiple invocations on the same variable is possible.  Can be reused again
- * without a call to \a vstring_def.
+ * without a call to \ref vstring_def.
  *
  * Side effect: Frees and pops off entries on and beyond index
- * \a g_startTempAllocStack from the \a tempAllocStack.
+ * \ref g_startTempAllocStack from the \ref tempAllocStack.
  *
- * \param[in,out] x (not null) an initialized \a vstring variable.  According to the
- * semantics of a \a vstring, __x__ is not deallocated, if it points to an
+ * \param[in,out] x (not null) an initialized \ref vstring variable.  According to the
+ * semantics of a \ref vstring, \p x is not deallocated, if it points to an
  * empty string. 
  * \pre
- *   __x__ was declared and initialized before.
+ *   \p x was declared and initialized before.
  * \post
- *   __x__ initialized with empty text.  Entries on and beyond index
- * \a g_startTempAllocStack are freed and popped off the \a tempAllocStack.
+ *   \p x initialized with empty text.  Entries on and beyond index
+ * \ref g_startTempAllocStack are freed and popped off the \ref tempAllocStack.
  */
 #define free_vstring(x) let(&x, "")
 
@@ -250,20 +250,21 @@ typedef vstring temp_vstring;
  * \fn freeTempAlloc
  * \brief Free space allocated for temporary vstring instances.
  *
- * Temporary \a vstring in \a tempAllocStack are used for example to construct
- * final text from patterns, boilerplate etc. along with data to be filled in.
+ * Temporary \ref vstring in \ref tempAllocStack are used for example to
+ * construct final text from patterns, boilerplate etc. along with data to be
+ * filled in.
  *
- * This function frees all entries beginning with \a g_startTempAllocStack.
+ * This function frees all entries beginning with \ref g_startTempAllocStack.
  * It is usually called automatically by let(), but can also be invoked
  * directly to avoid buildup of temporary strings.
  *
  * \pre
- *   \a g_startTempAllocStack is the index in \a tempAllocStack from which
+ *   \ref g_startTempAllocStack is the index in \ref tempAllocStack from which
  *   on enties are freed.
  * \post
- * - Entries in \a tempAllocStack from index \a g_startTempAllocStack on
- *   are freed.  The top of stack \a g_tempAllocStackTop is back to
- *   \a g_startTempAllocStack again, so the current scope of temporaries is
+ * - Entries in \ref tempAllocStack from index \ref g_startTempAllocStack on
+ *   are freed.  The top of stack \ref g_tempAllocStackTop is back to
+ *   \ref g_startTempAllocStack again, so the current scope of temporaries is
  *   empty;
  * - db1 is updated, if NDEBUG is not defined.
  */
@@ -275,46 +276,46 @@ void freeTempAlloc(void);
  * \fn let(vstring *target, const char *source)
  * \brief emulation of BASIC string assignment
  *
- * assigns to text to a \a vstring pointer.  This includes a bit of memory
+ * assigns to text to a \ref vstring pointer.  This includes a bit of memory
  * management.  Not only is the space of the destination of the assignment
  * reallocated if its previous size was too small.  But in addition the
- * \ref stack "stack" \a tempAllocStack is freed of intermediate values again.
- * Every entry on and beyond \a g_startTempAllocStack is considered to be
- * consumed and subject to deallocation.
+ * \ref stack "stack" \ref tempAllocStack is freed of intermediate values
+ * again.  Every entry on and beyond \ref g_startTempAllocStack is considered
+ * to be consumed and subject to deallocation.
  *
  * This deallocation procedure is embedded in this operation, since frequently
  * the final string was composed of some fragments, that now can be disposed
  * of.  In fact, this function must ALWAYS be called to assign to a vstring in
  * order for the memory cleanup routines, etc. to work properly.  A new vstring
- * should be initialized to "" (the empty string), and the 'vstring_def' macro
- * handles creation of such variables.
+ * should be initialized to "" (the empty string), and the \ref vstring_def
+ * macro handles creation of such variables.
  *
  * Possible failures: Out of memory condition.
  *
- * \param[out] target (not null) address of a \a vstring receiving a copy of
+ * \param[out] target (not null) address of a \ref vstring receiving a copy of
  *   the source string.  Its current value, if not empty, must never point to a
- *   true portion of another \a vstring.  It must not coincide with any of the
- *   temporary strings in \a tempAllocStack, from index
- *   \a g_startTempAllocStack on.  You can assign to an entry with index below
- *   this value, though.
+ *   true portion of another \ref vstring.  It must not coincide with any of
+ *   the temporary strings in \ref tempAllocStack, from index
+ *   \ref g_startTempAllocStack on.  You can assign to an entry with index
+ *   below this value, though.
  * \param[in] source (not null) NUL terminated string to be copied from.
  *
  * \pre
- * - \a g_startTempAllocStack contains the starting index of entries in
- *   \a tempAllocStack, that is going to be deallocated.
+ * - \ref g_startTempAllocStack contains the starting index of entries in
+ *   \ref tempAllocStack, that is going to be deallocated.
  * - both parameters are not null and point to NUL terminated strings.
  * - The destination of this function must either be empty, or uniquely point
- *   to a \a vstring, but not any of the temp_vstring;
+ *   to a \ref vstring, but not any of the \ref temp_vstring;
  * - The destination need not provide enough space for the source.  If
  *   necessary, it is reallocated to point to a larger chunk of memory;
  * \post
- * - Entries in \a tempAllocStack from \a g_startTempAllocStack (on entry to the
- *   function) are deallocated;
- * - The stack pointer in \a g_tempAllocStackTop is set to
- *   \a g_startTempAllocStack (on entry to the function);
+ * - Entries in \ref tempAllocStack from \ref g_startTempAllocStack (on entry
+ *   to the function) are deallocated;
+ * - The stack pointer in \ref g_tempAllocStackTop is set to
+ *   \ref g_startTempAllocStack (on entry to the function);
  * - If the assigned value is the empty string, but the destination not, it is
  *   freed and assigned to a constant "";
- * - \a db is updated.
+ * - \ref db is updated.
  */
 void let(vstring *target, const char *source);
 
@@ -329,15 +330,15 @@ void let(vstring *target, const char *source);
  * Up to MAX_CAT_ARGS - 1 (49) NUL terminated strings submitted as parameters
  * are concatenated to form a single NUL terminated string.  The parameters
  * terminate with a NULL pointer, a single NULL pointer is not allowed, though.
- * The resulting string is pushed on \a tempAllocStack.
+ * The resulting string is pushed on \ref tempAllocStack.
  * \param[in] string1 (not null) a pointer to a NUL terminated string.
  *   The following parameters are pointers to NUL terminated strings as well,
  *   except for the last parameter that must be NULL.  It is allowed to
  *   duplicate parameters.
- * \return the concatenated string terminated by a NUL character.
- * \post the resulting string is pushed onto the \a tempAllocStack.
- *   \a db is updated.
- * \bug a stack overflow of \a tempAllocStack is not handled correctly.
+ * \return the concatenated \ref temp_string terminated by a NUL character.
+ * \post the resulting string is pushed onto the \ref tempAllocStack.
+ *   \ref db is updated.
+ * \bug a stack overflow of \ref tempAllocStack is not handled correctly.
  */
 temp_vstring cat(const char * string1, ...);
 
@@ -358,54 +359,56 @@ int linput(FILE *stream, const char *ask, vstring *target);
 /* Indices are 1-based */
 /*!
  * \fn temp_vstring seg(const char *sin, long p1, long p2)
- * Extracts a substring from a source and pushes it on \a tempAllocStack.
+ * Extracts a substring from a source and pushes it on \ref tempAllocStack.
  * Note: The bounding indices are 1-based and inclusive.
  *
  * \param[in] sin (not null) pointer to the NUL-terminated source text.
  * \param[in] p1 offset of the first byte of the substring, counted in bytes from
- *   the first one of __sin__, a 1-based index.  A value less than 1 is
+ *   the first one of \p sin, a 1-based index.  A value less than 1 is
  *   internally corrected to 1, but it must not point beyond the terminating
- *   NUL of __sin__, if __p1__ <= __p2__.
+ *   NUL of \p sin, if \p p1 <= \p p2.
  * \param[in] p2 offset of the last byte of the substring, counted in bytes from
- *   the first one of __sin__, a 1-based index.  The natural bounds of this
- *   value are __p1__ - 1 and the length of __sin__.  Values outside of this
- *   range are internally corrected to the closer of these limits.  If __p2__ <
- *   __p1__ the empty string is returned.
+ *   the first one of \p sin, a 1-based index.  The natural bounds of this
+ *   value are \p p1 - 1 and the length of \p sin.  Values outside of this
+ *   range are internally corrected to the closer of these limits.  If \p p2 <
+ *   \p p1 the empty string is returned.
  * \attention the indices are 1-based: seg("hello", 2, 3) == "el"!
- * \return a pointer to new allocated \a temp_vstring referencing the
- *   requested substring, that is also pushed onto the top of \a tempAllocStack
+ * \return a pointer to new allocated \ref temp_vstring referencing the
+ *   requested substring, that is also pushed onto the top of
+ *   \ref tempAllocStack
  * \pre
- *   __p1__ <= length(__sin__).
+ *   \p p1 <= length(\p sin).
  * \post
- *   A pointer to the substring is pushed on \a tempAllocStack, even if it
+ *   A pointer to the substring is pushed on \ref tempAllocStack, even if it
  *   empty;
  * \warning not UTF-8 safe.
- * \bug a stack overflow of \a tempAllocStack is not handled correctly;
+ * \bug a stack overflow of \ref tempAllocStack is not handled correctly;
  */
 temp_vstring seg(const char *sin, long p1, long p2);
 /*!
  * \fn temp_vstring mid(const char *sin, long p, long l)
- * Extracts a substring from a source and pushes it on \a tempAllocStack
+ * Extracts a substring from a source and pushes it on \ref tempAllocStack
  *
  * \param[in] sin (not null) pointer to the NUL-terminated source text.
- * \param[in] p offset of the substring in bytes from the first byte of __sin__,
+ * \param[in] p offset of the substring in bytes from the first byte of \p sin,
  *   1-based.  A value less than 1 is internally corrected to 1, but it must
- *   never point beyond the terminating NUL of __sin__.
+ *   never point beyond the terminating NUL of \p sin.
  * \param[in] l length of substring in bytes.  Negative values are corrected to 0.
- *   If __p__ + __l__ exceeds the length of __sin__, then only the portion up
+ *   If \p p + \p l exceeds the length of \p sin, then only the portion up
  *   to the terminating NUL is taken.
- * \attention the index __p__ is 1-based: mid("hello", 2, 1) == "e"!
- * \return a pointer to new allocated \a temp_vstring referencing the
- *   requested substring, that is also pushed onto the top of \a tempAllocStack
+ * \attention the index \p p is 1-based: mid("hello", 2, 1) == "e"!
+ * \return a pointer to new allocated \ref temp_vstring referencing the
+ *   requested substring, that is also pushed onto the top of
+ *   \ref tempAllocStack
  * \pre
- *   __p__ <= length(__sin__).  This must hold even if the requested length is
+ *   \p p <= length(\p sin).  This must hold even if the requested length is
  *   0, because its implementation in C requires the validity of the pointer,
  *   even if it is not dereferenced.
  * \post
- *   A pointer to the substring is pushed on \a tempAllocStack, even if it
- *   empty;
+ *   A pointer to the substring is pushed on \ref tempAllocStack, even if it
+ *   is empty;
  * \warning not UTF-8 safe.
- * \bug a stack overflow of \a tempAllocStack is not handled correctly;
+ * \bug a stack overflow of \ref tempAllocStack is not handled correctly;
  */
 temp_vstring mid(const char *sin, long p, long l);
 /*!
@@ -418,15 +421,15 @@ temp_vstring mid(const char *sin, long p, long l);
  *
  * \param[in] sin (not null) pointer to a NUL terminated string to be copied from.
  * \param[in] n count of bytes to be copied from the source.  The natural bounds of
- *   this value is 0 and the length of __sin__ in bytes.  Any value outside of
+ *   this value is 0 and the length of \p sin in bytes.  Any value outside of
  *   this range is corrected to the closer one of these limits.
- * \return a pointer to new allocated \a temp_vstring referencing the
- *   requested portion, that is also pushed onto the top of \a tempAllocStack
+ * \return a pointer to new allocated \ref temp_vstring referencing the
+ *   requested portion, that is also pushed onto the top of \ref tempAllocStack
  * \post
- *   A pointer to the substring is pushed on \a tempAllocStack, even if it
- *   empty.
+ *   A pointer to the substring is pushed on \ref tempAllocStack, even if it
+ *   is empty.
  * \warning not UTF-8 safe.
- * \bug a stack overflow of \a tempAllocStack is not handled correctly.
+ * \bug a stack overflow of \ref tempAllocStack is not handled correctly.
  */
 temp_vstring left(const char *sin, long n);
 /*!
@@ -441,14 +444,14 @@ temp_vstring left(const char *sin, long n);
  *   from.
  * \param[in] n 1-based index of the first not skipped character at the
  *   beginning of the source.  A value less than 1 is internally corrected to 1.
- * \return a pointer to new allocated \a temp_vstring referencing the
- *   requested portion, that is also pushed onto the top of \a tempAllocStack
- * \attention the index __n__ is 1-based: right("hello", 2) == "ello"!
+ * \return a pointer to new allocated \ref temp_vstring referencing the
+ *   requested portion, that is also pushed onto the top of \ref tempAllocStack
+ * \attention the index \p n is 1-based: right("hello", 2) == "ello"!
  * \pre
- *   __n__ <= length(__sin__)
+ *   \p n <= length(\p sin)
  * \post
- *   A pointer to the substring is pushed on \a tempAllocStack, even if it
- *   empty.
+ *   A pointer to the substring is pushed on \ref tempAllocStack, even if it
+ *   is empty.
  * \warning not UTF-8 safe.
  * \bug a stack overflow of \a tempAllocStack is not handled correctly.
  */
@@ -456,29 +459,29 @@ temp_vstring right(const char *sin, long n);
 temp_vstring edit(const char *sin, long control);
 /*!
  * \fn temp_vstring space(long n)
- * pushes a NUL terminated string of __n__ characters onto
- * \a tempAllocStack.
+ * pushes a NUL terminated string of \p n characters onto
+ * \ref tempAllocStack.
  * \param[in] n the count of spaces, one less than the memory to allocate in
  *   bytes.
- * \return a pointer to new allocated \a temp_vstring referencing the
- *   requested contents, also pushed onto the top of \a tempAllocStack
+ * \return a pointer to new allocated \ref temp_vstring referencing the
+ *   requested contents, also pushed onto the top of \ref tempAllocStack
  * \post The returned string is NUL terminated
- * \bug a stack overflow of \a tempAllocStack is not handled correctly.
+ * \bug a stack overflow of \ref tempAllocStack is not handled correctly.
  */
 temp_vstring space(long n);
 /*!
  * \fn temp_vstring string(long n, char c)
- * pushes a NUL terminated string of __n__ characters __c__ onto
- * \a tempAllocStack.
+ * pushes a NUL terminated string of \p n characters \p c onto
+ * \ref tempAllocStack.
  * \param[in] n one less than the memory to allocate in bytes.
  * \param[in] c character to fill the allocated memory with.  It is padded to
  *   the right with a NUL character.
- * \attention The choice of NUL for __c__ returns the empty string in a block
- *   of __n__ + 1 allocated bytes.
+ * \attention The choice of NUL for \p c returns the empty string in a block
+ *   of \p n + 1 allocated bytes.
  * \post The returned string is NUL terminated
- * \return a pointer to new allocated \a temp_vstring referencing the
- *   requested contents, also pushed onto the top of \a tempAllocStack
- * \bug a stack overflow of \a tempAllocStack is not handled correctly.
+ * \return a pointer to new allocated \ref temp_vstring referencing the
+ *   requested contents, also pushed onto the top of \ref tempAllocStack
+ * \bug a stack overflow of \ref tempAllocStack is not handled correctly.
  */
 temp_vstring string(long n, char c);
 /*!
@@ -486,20 +489,20 @@ temp_vstring string(long n, char c);
  * \brief create a temporary string containing a single byte.
  *
  * create a NUL terminated string containing only the least significant byte of
- * __n__.  If this byte is 0x00, an empty string is the result.  If the most
+ * \p n.  If this byte is 0x00, an empty string is the result.  If the most
  * significant bit of this byte is set, the returned string is not an ASCII
  * or UTF-8 string.
  * \param[in] n The eight least significant bits are converted into a
  *   character used to build a string from.
  * \post A string containing a single character different from NUL, or
- *   the empty string else, is pushed onto the \a tempAllocStack.
- * \return a pointer to new allocated \a temp_vstring referencing the
- *   requested contents, also pushed onto the top of \a tempAllocStack
+ *   the empty string else, is pushed onto the \ref tempAllocStack.
+ * \return a pointer to new allocated \ref temp_vstring referencing the
+ *   requested contents, also pushed onto the top of \ref tempAllocStack
  * \warning
  *   the resulting string need not contain exactly 1 character, and if it does,
  *   this character need not be ASCII or UTF-8.  If CHAR_BITS is not 8
  *   (extremely rare nowadays) there might be a portability issue.
- * \bug a stack overflow of \a tempAllocStack is not handled correctly.
+ * \bug a stack overflow of \ref tempAllocStack is not handled correctly.
  */
 temp_vstring chr(long n);
 temp_vstring xlate(const char *sin, const char *table);
@@ -533,7 +536,7 @@ vstring quo$(vstring sout);
  * \var g_tempAllocStackTop
  * \brief Top of stack for temporary text.
  *
- * Refers to the \ref stack "stack" in \a tempAllocStack for temporary text.
+ * Refers to the \ref stack "stack" in \ref tempAllocStack for temporary text.
  * The current top index referencing the next free entry is kept in this variable.
  *
  * This value is made public for setting up scopes of temporary memory for
@@ -548,7 +551,7 @@ extern long g_tempAllocStackTop;   /* Top of stack for tempAlloc function */
  * \var g_startTempAllocStack
  * \brief references the first entry of the current scope of temporaries.
  *
- * Refers to the \ref stack "stack" in \a tempAllocStack for temporary text.
+ * Refers to the \ref stack "stack" in \ref tempAllocStack for temporary text.
  * Nested functions maintain their own scope of temporary data.  The index
  * referencing the first index of the current scope is kept in this variable.
  *
@@ -560,7 +563,7 @@ extern long g_tempAllocStackTop;   /* Top of stack for tempAlloc function */
  * it restores those values.
  *
  * \invariant
- *   \a g_startTempAllocStack <= \a g_tempAllocStackTop.
+ *   \ref g_startTempAllocStack <= \ref g_tempAllocStackTop.
  */
 extern long g_startTempAllocStack; /* Where to start freeing temporary allocation
     when let() is called (normally 0, except for nested vstring functions) */

From 34533da7d076df52eaff3d622b627e2e35f321fb Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 13:07:32 +0100
Subject: [PATCH 07/42] explain cmdIput1, next version

---
 src/mminou.h | 37 ++++++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 15 deletions(-)

diff --git a/src/mminou.h b/src/mminou.h
index 1baf245a..c6f5a54c 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -197,21 +197,28 @@ vstring cmdInput(FILE *stream, const char *ask);
 /*!
  * \brief print explanatory text and then read a line.
  *
- * gets a line from either stdin or the command file stream depending on
- * \ref g_commandFileNestingLevel.  If this value is 0, interactive input is
- * assumed, else It uses \ref cmdInput(), i.e some input lines may be
- * interpreted and not returned to the caller.  The conditions for this are
- * listed in \ref cmdInput, except that \ref localScrollMode is fixed to 1.
- * \param ask (not null) text displayed before input prompt.  This can be
- *   located in \ref tempAllocStack.  If this text contains more than
- *   \ref g_screenWidth characters, it is wrapped preferably at spaces and
- *   split across multiple lines.  If the final line contains spaces in the
- *   range from position 1 to \ref g_screenWidth - 11, it is wrapped such, that
- *   it leaves enough space for ten character user input.
- *   \n
- *   If the user is prompted again, only the last line of the wrapped text in
- *   \p ask is reprinted.
- * \return not interpreted line.
+ * After some explanatory text is printed, gets a line from either stdin or the
+ * command file stream in \ref g_commandFilePt, depending on the value of
+ * \ref g_commandFileNestingLevel.  If this value is 0, interactive input via
+ * stdin is assumed, else non interpreted lines are read from a file.  The line returned
+ * to the caller is more or less what \ref cmdInput() yields, but some fine
+ * tuning is applied.
+ *
+ * 1. The text used to prompt the user is most useful in interactive mode.  It
+ * is wrapped around preferably at spaces to fit into a display of
+ * \ref g_screenWidth.  If possible, wrapping shortens the last line such that
+ * space for 10 characters is available to the right of the prompt for user
+ * input.  Lengthy output may be interrupted for convenient page wise display.
+ * The user's scroll commands are interpreted internally and not seen by the
+ * caller.  If a line is either discarded or interpreted, the user is prompted
+ * again. The full prompt text is never repeated, only its last line after
+ * wrapping.
+ *
+ * 2. In interactive mode, empty lines are usually discarded.  An empty line
+ * resulting from an error (buffer overflow) or a premature EOF (CTRL_D) is
+ * returned, though.
+ *
+ * \return first not interpreted line as \ref vstring.  An empty string on error.
  * \pre
  *   The following variables are honored during execution and should be properly
  *   set:

From 35e8952b8db05340bcf7d62bf45559904ba7966c Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 13:41:21 +0100
Subject: [PATCH 08/42] explain cmdIput1, next version

---
 src/mminou.h | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/mminou.h b/src/mminou.h
index c6f5a54c..fd5660c7 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -214,11 +214,16 @@ vstring cmdInput(FILE *stream, const char *ask);
  * again. The full prompt text is never repeated, only its last line after
  * wrapping.
  *
- * 2. In interactive mode, empty lines are usually discarded.  An empty line
- * resulting from an error (buffer overflow) or a premature EOF (CTRL_D) is
- * returned, though.
+ * 2. In interactive mode, empty lines are discarded, and a reprompt triggered.
+ * 
+ * 3. A NULL resulting from an error (buffer overflow) or a premature EOF
+ * (CTRL_D from keyboard) from \ref cmdInput is either returned as "EXIT".  Or
+ * if the last line of the prompt starts with "Do", then it is assumed to
+ * expand to "Do you want to EXIT anyway (Y, N)?" and a "Y" is returned. In any
+ * case, the returned string is printed before it may finally triggers an
+ * immediate stop on the caller's side.
  *
- * \return first not interpreted line as \ref vstring.  An empty string on error.
+ * \return first not interpreted line as \ref vstring, or "EXIT" on error. 
  * \pre
  *   The following variables are honored during execution and should be properly
  *   set:

From e5e5cd2b628a3adf2d9d3f1049f15e4b94c211a5 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 14:09:15 +0100
Subject: [PATCH 09/42] explain cmdIput1, next version

---
 src/mminou.h | 42 ++++++++++++++++++++++++++++--------------
 1 file changed, 28 insertions(+), 14 deletions(-)

diff --git a/src/mminou.h b/src/mminou.h
index fd5660c7..fc820c10 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -20,6 +20,10 @@
 extern int g_errorCount;     /* Total error count */
 
 /* Global variables used by print2() */
+/*!
+ * \var flag g_logFileOpenFlag
+ * If set to 1, logging of input is enabled.
+ */
 extern flag g_logFileOpenFlag;
 extern FILE *g_logFilePtr;
 extern FILE *g_listFile_fp;
@@ -204,24 +208,32 @@ vstring cmdInput(FILE *stream, const char *ask);
  * to the caller is more or less what \ref cmdInput() yields, but some fine
  * tuning is applied.
  *
- * 1. The text used to prompt the user is most useful in interactive mode.  It
- * is wrapped around preferably at spaces to fit into a display of
- * \ref g_screenWidth.  If possible, wrapping shortens the last line such that
- * space for 10 characters is available to the right of the prompt for user
- * input.  Lengthy output may be interrupted for convenient page wise display.
+ * \par Displaying the prompt text
+ *
+ * The text used to prompt the user is wrapped around preferably spaces to fit
+ * into a display of \ref g_screenWidth.  If possible, wrapping shortens the
+ * last line such that space for 10 characters is available to the right of the
+ * prompt for user input.
+ *
+ * \par Interactive Mode
+ *
+ * 1. A long prompt text may be interrupted for convenient page wise display.
  * The user's scroll commands are interpreted internally and not seen by the
  * caller.  If a line is either discarded or interpreted, the user is prompted
  * again. The full prompt text is never repeated, only its last line after
- * wrapping.
+ * wrapping was applied.
  *
- * 2. In interactive mode, empty lines are discarded, and a reprompt triggered.
+ * 2. Empty lines are discarded, and a reprompt is triggered.
  * 
- * 3. A NULL resulting from an error (buffer overflow) or a premature EOF
- * (CTRL_D from keyboard) from \ref cmdInput is either returned as "EXIT".  Or
- * if the last line of the prompt starts with "Do", then it is assumed to
- * expand to "Do you want to EXIT anyway (Y, N)?" and a "Y" is returned. In any
- * case, the returned string is printed before it may finally triggers an
- * immediate stop on the caller's side.
+ * 3. In interactive mode, a NULL resulting from an error (buffer overflow) or
+ * a premature EOF (CTRL_D from keyboard) from \ref cmdInput is either returned
+ * as "EXIT".  Or if the last line of the prompt starts with "Do", then it is
+ * assumed to expand to "Do you want to EXIT anyway (Y, N)?" and a "Y" is
+ * returned. In any case, the returned string is printed before it may finally
+ * trigger an immediate stop on the caller's side.
+ *
+ * 4. Before the line is returned to the caller, it is logged should that be
+ * enabled.
  *
  * \return first not interpreted line as \ref vstring, or "EXIT" on error. 
  * \pre
@@ -240,7 +252,9 @@ vstring cmdInput(FILE *stream, const char *ask);
  *   - \ref localScrollMode a value of 0 temporarily disables scrolling,
  *     overriding the setting in \ref g_scrollMode;
  *   - \ref g_commandPrompt if this string matches ask, top level user input is
- *     assumed, and an empty line is usually discarded.
+ *     assumed, and an empty line is usually discarded;
+ *   - \ref g_logFileOpenFlag if set to 1, a read line is logged before it is
+ *     passed to the caller.
  * \post
  *   \ref localScrollMode is set to 1
  * \attention A CTRL_D can cause a return of an empty line, even if an

From 83c4919036c86efdda8d4e00fc93903f5a4d9e44 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 14:22:36 +0100
Subject: [PATCH 10/42] doc log file

---
 src/mminou.h | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/src/mminou.h b/src/mminou.h
index fc820c10..70e97310 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -22,9 +22,15 @@ extern int g_errorCount;     /* Total error count */
 /* Global variables used by print2() */
 /*!
  * \var flag g_logFileOpenFlag
- * If set to 1, logging of input is enabled.
+ * If set to 1, logging of input is enabled.  Initially set to 0.
  */
 extern flag g_logFileOpenFlag;
+/*!
+ * \var FILE *g_logFilePtr
+ * The OPEN LOG command opens a log file.  Its file descriptor is stored here,
+ * and not removed, when the log file is closed.  You should access this
+ * descriptor only when \ref g_logFileOpenFlag is 1.
+ */
 extern FILE *g_logFilePtr;
 extern FILE *g_listFile_fp;
 /* Global variables used by print2() */
@@ -225,12 +231,12 @@ vstring cmdInput(FILE *stream, const char *ask);
  *
  * 2. Empty lines are discarded, and a reprompt is triggered.
  * 
- * 3. In interactive mode, a NULL resulting from an error (buffer overflow) or
- * a premature EOF (CTRL_D from keyboard) from \ref cmdInput is either returned
- * as "EXIT".  Or if the last line of the prompt starts with "Do", then it is
- * assumed to expand to "Do you want to EXIT anyway (Y, N)?" and a "Y" is
- * returned. In any case, the returned string is printed before it may finally
- * trigger an immediate stop on the caller's side.
+ * 3. A NULL resulting from an error (buffer overflow) or a premature EOF
+ * (CTRL_D from keyboard) from \ref cmdInput is either returned as "EXIT".  Or
+ * if the last line of the prompt starts with "Do", then it is assumed to
+ * expand to "Do you want to EXIT anyway (Y, N)?" and a "Y" is returned. In any
+ * case, the returned string is printed before it may finally trigger an
+ * immediate stop on the caller's side.
  *
  * 4. Before the line is returned to the caller, it is logged should that be
  * enabled.
@@ -257,8 +263,6 @@ vstring cmdInput(FILE *stream, const char *ask);
  *     passed to the caller.
  * \post
  *   \ref localScrollMode is set to 1
- * \attention A CTRL_D can cause a return of an empty line, even if an
- *   interactive mode is assumed
  * \warning the calling program must deallocate the returned string.
  */
 vstring cmdInput1(const char *ask);

From 39b356c4aa0228dd8721591ed7d8d94f08f245c4 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 18:53:31 +0100
Subject: [PATCH 11/42] point out copy problems of pointers

---
 src/mmdata.h | 22 ++++++++++++++++++++--
 src/mminou.c |  7 +++++--
 src/mminou.h |  7 +++----
 3 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index edf0b98f..c9c8a89e 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -122,7 +122,22 @@ typedef long nmbrString; /* String of numbers */
  * To summarize the usages of this type:
  * - If you want to resize the array/stack you need a pointer to element 0.
  * - You can iterate from an arbitrary pointer to the end.
- * - Sometimes it denotes an isolated element, not embedded in a greater array.
+ * - Sometimes pntrString denotes an isolated element, not embedded in a
+ *   greater array.
+ *
+ * \warning Simply copying elements around is dangerous, if the elements point
+ *   to allocated memory.  There must be a guard that owns the instances,
+ *   survives each of the copies and finally deallocates the instances.
+ *   Otherwise you risk memory leaks, or even worse, undefined behavior, if a
+ *   copied pointer uses an instance previously freed by the original.  One way
+ *   to provide such a guard is a nested program structure.  All copied
+ *   pointers are created in subroutines, and they vanish before the caller
+ *   gains control again, and can safely deallocate the instances.  A similar
+ *   strategy is followed by \ref pntrLet, where deallocations of original and
+ *   derived instances are deferred until an operation finally finishes.  More
+ *   modern concepts employ reference counting schemes, and by avoiding
+ *   dedicated ownership solve this problem more thoroughly, but Metamath is
+ *   not up to that level (yet).
  */
 typedef void* pntrString; /* String of pointers */
 
@@ -614,6 +629,9 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
 
 
 /* String assignment - MUST be used to assign vstrings */
+/*!
+ * \fn void pntrLet(pntrString **target, const pntrString *source)
+ */
 void pntrLet(pntrString **target, const pntrString *source);
 
 /* String concatenation - last argument MUST be NULL */
@@ -658,7 +676,7 @@ long pntrLen(const pntrString *s);
  * derived from administrative data in the surrounding block.  The result
  * excludes the terminal element reserved for a null pointer.
  *
- * \param[in] s points to a element 0 of a \ref pntrString embedded in a block
+ * \param[in] s points to element 0 of a \ref pntrString embedded in a block
  * \return the maximal number of pointers that can be used in the array pointed
  * to by \p s.
  * \pre the array pointed to by s is the sole user of a \ref block "block".
diff --git a/src/mminou.c b/src/mminou.c
index 484d5080..fa75a3e3 100644
--- a/src/mminou.c
+++ b/src/mminou.c
@@ -74,7 +74,9 @@ flag localScrollMode = 1; /* 0 = Scroll continuously only till next prompt */
 
 /* Buffer for B (back) command at end-of-page prompt - for future use */
 /*! \var pntrString* backBuffer
- * Buffer for B (back) command at end-of-page prompt.
+ * Buffer for B (back) command at end-of-page prompt.  Although formally a
+ * \ref pntrString is an array of void*, this buffer contains always pointer to
+ * \ref vstring.
  *
  * Some longer text (like help texts for example) provide a page wise display
  * with a scroll option, so the user can move freely back and forth in the
@@ -85,7 +87,8 @@ pntrString_def(backBuffer);
 /*!
  * \var backBufferPos
  *
- * A position within the \ref backBuffer.
+ * Number of entries in the \ref backBuffer that are available for repeatedly
+ * scrolling back.  Initialized to 0.
  *
  * \invariant The value 0 requires an empty \ref backBuffer.
  */
diff --git a/src/mminou.h b/src/mminou.h
index 70e97310..d24bbed5 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -238,8 +238,7 @@ vstring cmdInput(FILE *stream, const char *ask);
  * case, the returned string is printed before it may finally trigger an
  * immediate stop on the caller's side.
  *
- * 4. Before the line is returned to the caller, it is logged should that be
- * enabled.
+ * 4. If logging is enabled, prompt and returned input is logged.
  *
  * \return first not interpreted line as \ref vstring, or "EXIT" on error. 
  * \pre
@@ -259,8 +258,8 @@ vstring cmdInput(FILE *stream, const char *ask);
  *     overriding the setting in \ref g_scrollMode;
  *   - \ref g_commandPrompt if this string matches ask, top level user input is
  *     assumed, and an empty line is usually discarded;
- *   - \ref g_logFileOpenFlag if set to 1, a read line is logged before it is
- *     passed to the caller.
+ *   - \ref g_logFileOpenFlag if set to 1, a not interpreted returned line is
+ *     logged before it is passed on to the caller.
  * \post
  *   \ref localScrollMode is set to 1
  * \warning the calling program must deallocate the returned string.

From 1017b3d33a96f114b0f56becb214379ea865fc99 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 19:51:19 +0100
Subject: [PATCH 12/42] doc addToUsedPool

---
 src/mmdata.c |  6 ++++++
 src/mmdata.h | 33 +++++++++++++++++++++++++++++----
 2 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/src/mmdata.c b/src/mmdata.c
index 4e138421..31b9444c 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -197,6 +197,10 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
    The pointer to an array always points to element 0 (recast to right size).
 */
 
+/*!
+ * \def MEM_POOL_GROW
+ * Amount that \ref memUsedPool and \ref memFreePool grows when it overflows.
+ */
 #define MEM_POOL_GROW 1000 /* Amount that a pool grows when it overflows. */
 /*??? Let user set this from menu. */
 long poolAbsoluteMax = 1000000; /* Pools will be purged when this is reached */
@@ -2693,6 +2697,8 @@ void pntrZapLen(pntrString *s, long length) {
  * \invariant
  *   If \p s is contained in a \ref block "block", its administrative header is
  *   NOT updated.
+ * \warning The thoughtless use of this function has the potential to create
+ *   risks mentioned in the warning of \ref pntrString.
  */
 void pntrCpy(pntrString *s, const pntrString *t) {
   long i;
diff --git a/src/mmdata.h b/src/mmdata.h
index c9c8a89e..13791245 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -134,10 +134,10 @@ typedef long nmbrString; /* String of numbers */
  *   pointers are created in subroutines, and they vanish before the caller
  *   gains control again, and can safely deallocate the instances.  A similar
  *   strategy is followed by \ref pntrLet, where deallocations of original and
- *   derived instances are deferred until an operation finally finishes.  More
- *   modern concepts employ reference counting schemes, and by avoiding
- *   dedicated ownership solve this problem more thoroughly, but Metamath is
- *   not up to that level (yet).
+ *   dependent instances are deferred until an operation finally finishes.
+ *   More modern concepts employ reference counting schemes, thus avoiding
+ *   dedicated ownership and solving this problem more thoroughly, but Metamath
+ *   is not up to that level (yet).
  */
 typedef void* pntrString; /* String of pointers */
 
@@ -309,6 +309,31 @@ extern flag g_globalDiscouragement; /* SET DISCOURAGEMENT */
 void *poolFixedMalloc(long size /* bytes */);
 void *poolMalloc(long size /* bytes */);
 void poolFree(void *ptr);
+/*!
+ * \fn addToUsedPool(void *ptr)
+ * \brief announces a block with free capacity for further allocation
+ *
+ * The program maintains pools of memory blocks with free capacity.  In case of
+ * demand such a \ref block can temporarily allocate this capacity for new
+ * usage.  Of course two (or more) clients share different parts of the same
+ * \ref block then, so a newer client must complete its usage before the old
+ * one resumes operation and may want to extend its usage of the \ref block.
+ * \n
+ * This function temporarily freezes the usage of a block for an old client, and
+ * allows temporary reallocation of the free capacity to a new client.
+ * \n
+ * Before \p ptr is added to \ref memUsedPool, the pool size is checked and
+ * increased by \ref MEM_POOL_GROW if full.  This may lead to out-of-memory
+ * \ref bug "bugs".  But if \p prt is added to the end of the \ref memUsedPool,
+ * \ref poolTotalFree is updated.
+ * \param[in] ptr pointer to a \ref block.
+ * \pre
+ *   the block is \ref fragmentation "fragmented" (contains unused pointers)
+ *   If this condition is violated \ref bug is called and the function returns
+ *   without further action.
+ * \post
+ *   \ref poolTotalFree is the current free space in bytes in both pools.
+ */
 void addToUsedPool(void *ptr);
 /* Purges reset memory pool usage */
 void memFreePoolPurge(flag untilOK);

From da73b5c2eccb77854f9990c157a060689d7f82cf Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 20:22:39 +0100
Subject: [PATCH 13/42] fix incorrect usage of memUsedPool in case of full
 blocks

---
 src/mmdata.c | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/mmdata.c b/src/mmdata.c
index 31b9444c..9cfb43d4 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -139,10 +139,11 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
  *
  * offset -3:\n
  *   If this block has free space at the end (is \ref fragmentation
- *   "fragmented"), then it contains its index in the used blocks array, see
- *   \ref memUsedPool.  A value of -1 indicates it is either fully occupied or
- *   totally free.  In any of these cases it is not kept in the used blocks
- *   array.
+ *   "fragmented"), then this value contains its index in the used blocks
+ *   array, see \ref memUsedPool.  A value of -1 indicates it is either fully
+ *   occupied or totally free.  It is not kept in the used blocks array then.
+ *   If this block becomes full in the course of events, it is not
+ *   automatically removed from \ref memUsedPool, though.
  */
 
 /*! \page Pool

From 67fa533c7da1f81bc5c83be17e7014f51ef48ea6 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 20:25:33 +0100
Subject: [PATCH 14/42] clarify post cond. of addToUsedPool

---
 src/mmdata.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 13791245..a8eb0d59 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -332,7 +332,8 @@ void poolFree(void *ptr);
  *   If this condition is violated \ref bug is called and the function returns
  *   without further action.
  * \post
- *   \ref poolTotalFree is the current free space in bytes in both pools.
+ *   - \ref poolTotalFree is the current free space in bytes in both pools.
+ *   - A full \ref block is not added to \ref memUsedPool by this function.
  */
 void addToUsedPool(void *ptr);
 /* Purges reset memory pool usage */

From ac1dc027d378fceef3383cb02bb1377a26451f2d Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 4 Mar 2022 20:27:50 +0100
Subject: [PATCH 15/42] fix description of memUsedPool

---
 src/mmdata.c | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/mmdata.c b/src/mmdata.c
index 9cfb43d4..9292371c 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -232,6 +232,8 @@ long poolTotalFree = 0; /* Total amount of free space allocated in pool */
  * at the end of the array are unused.  Its current usage is given by
  * \ref memUsedPoolSize.  Its capacity is given by \ref memUsedPoolMax.
  *
+ * \attention The pool may contain full \ref block "blocks".
+ *
  * \invariant Each block in the used blocks array has its index noted in its
  * hidden header, for backward reference.
  *

From 49af905866162d7932e6fe6084d41666f7fb4c38 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sat, 5 Mar 2022 07:36:40 +0100
Subject: [PATCH 16/42] doc poolFree

---
 src/mmdata.h | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/mmdata.h b/src/mmdata.h
index a8eb0d59..4730c5ea 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -308,6 +308,16 @@ extern flag g_globalDiscouragement; /* SET DISCOURAGEMENT */
 /* Allocation and deallocation in memory pool */
 void *poolFixedMalloc(long size /* bytes */);
 void *poolMalloc(long size /* bytes */);
+/*!
+ * \fn poolFree(void *ptr)
+ *
+ * Removes \p ptr from the \ref memUsedPool, if it is listed there.  Then tries
+ * adding it to the \ref memFreePool.  If this pool is full, it is increased by
+ * \ref MEM_POOL_GROW.  If this fails, an error is created, else \p ptr is
+ * added.
+ * \param[in] ptr pointer to a \ref block.
+ * \bug calls outOfMemory, that can stack up endlessly
+ */
 void poolFree(void *ptr);
 /*!
  * \fn addToUsedPool(void *ptr)
@@ -334,6 +344,7 @@ void poolFree(void *ptr);
  * \post
  *   - \ref poolTotalFree is the current free space in bytes in both pools.
  *   - A full \ref block is not added to \ref memUsedPool by this function.
+ * \bug calls outOfMemory, that can stack up endlessly
  */
 void addToUsedPool(void *ptr);
 /* Purges reset memory pool usage */

From 0fcfc296c53ee96305cf192eba3a62ad8d16e4cf Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sat, 5 Mar 2022 08:18:15 +0100
Subject: [PATCH 17/42] add pre post conditions

---
 src/mmdata.h | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 4730c5ea..36f486d4 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -316,6 +316,10 @@ void *poolMalloc(long size /* bytes */);
  * \ref MEM_POOL_GROW.  If this fails, an error is created, else \p ptr is
  * added.
  * \param[in] ptr pointer to a \ref block.
+ * \pre
+ *   all memory pointed to by \p ptr is considered free.
+ * \post
+ *   \ref poolTotalFree is updated
  * \bug calls outOfMemory, that can stack up endlessly
  */
 void poolFree(void *ptr);
@@ -323,24 +327,24 @@ void poolFree(void *ptr);
  * \fn addToUsedPool(void *ptr)
  * \brief announces a block with free capacity for further allocation
  *
+ * This function temporarily freezes the usage of a block for an old client, and
+ * allows temporary reallocation of the free capacity to a new client.
+ * \n
  * The program maintains pools of memory blocks with free capacity.  In case of
  * demand such a \ref block can temporarily allocate this capacity for new
  * usage.  Of course two (or more) clients share different parts of the same
  * \ref block then, so a newer client must complete its usage before the old
  * one resumes operation and may want to extend its usage of the \ref block.
  * \n
- * This function temporarily freezes the usage of a block for an old client, and
- * allows temporary reallocation of the free capacity to a new client.
- * \n
  * Before \p ptr is added to \ref memUsedPool, the pool size is checked and
  * increased by \ref MEM_POOL_GROW if full.  This may lead to out-of-memory
  * \ref bug "bugs".  But if \p prt is added to the end of the \ref memUsedPool,
  * \ref poolTotalFree is updated.
  * \param[in] ptr pointer to a \ref block.
  * \pre
- *   the block is \ref fragmentation "fragmented" (contains unused pointers)
- *   If this condition is violated \ref bug is called and the function returns
- *   without further action.
+ *   the block is \ref fragmentation "fragmented" (contains unused memory)
+ *   If it is full \ref bug is called and the function returns without further
+ *   action.
  * \post
  *   - \ref poolTotalFree is the current free space in bytes in both pools.
  *   - A full \ref block is not added to \ref memUsedPool by this function.

From 7beeb0e1f3d3fa6b31dc7e5a4520ef753875f52b Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sat, 5 Mar 2022 13:57:38 +0100
Subject: [PATCH 18/42] doc poolMalloc and others

---
 src/mmdata.c | 40 ++++++++++++++++++++++++++++++++++------
 src/mmdata.h | 45 ++++++++++++++++++++++++++++++++++++++-------
 src/mmvstr.h | 40 ++++++++++++++++++++--------------------
 3 files changed, 92 insertions(+), 33 deletions(-)

diff --git a/src/mmdata.c b/src/mmdata.c
index 9292371c..f9e03b96 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -204,12 +204,25 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
  */
 #define MEM_POOL_GROW 1000 /* Amount that a pool grows when it overflows. */
 /*??? Let user set this from menu. */
+/*!
+ * \var long poolAbsoluteMax
+ * The value is a memory amount in bytes.
+ * \n
+ * The \ref suballocator scheme must not hold more memory than is short term
+ * useful.  To the operating system all memory in \ref memFreePool appears as
+ * allocated, although it is not really in use.  To prevent the system from
+ * taking unnecessary action such as saving RAM to disk, a limit to the amount
+ * of free memory managed by the suballocator can be set up.  This limit is
+ * checked in frequent operations, and an automatic purge process is initiated
+ * in \ref memFreePoolPurge should \ref poolTotalFree exceed this value.
+ */
 long poolAbsoluteMax = 1000000; /* Pools will be purged when this is reached */
 /*!
  * \var long poolTotalFree
  * contains the number of free space available in bytes, in both pools
  * \ref memFreePool and \ref memUsedPool, never counting the hidden headers at
- * the beginning of each block, see \ref block.
+ * the beginning of each block, see \ref block.  Exceeding \ref poolAbsoluteMax
+ * may trigger an automatic purge process by \ref memFreePoolPurge.
  */
 long poolTotalFree = 0; /* Total amount of free space allocated in pool */
 /*E*/long i1,j1_,k1; /* 'j1' is a built-in function */
@@ -556,6 +569,21 @@ void addToUsedPool(void *ptr)
 }
 
 /* Free all arrays in the free pool. */
+/*!
+ * \fn void memFreePoolPurge(flag untilOK)
+ * \brief returns memory held in \ref memFreePool
+ * Starting with the last entry in \ref memFreePool, memory held in that pool
+ * is returned to the system until all, or at least a sufficient amount is
+ * freed again (see \p untilOK).
+ * \param[in] untilOK if 1 freeing \ref block "blocks" stops the moment
+ *   \ref poolTotalFree gets within the range of \ref poolAbsoluteMax again.
+ *   Note that it is not guaranteed that the limit \ref poolAbsoluteMax is
+ *   undercut because still too much free memory might be held in the
+ *   \ref memUsedPool.
+ *   \n
+ *   If 0, all \ref memFreePool entries are freed, and the pool itself is
+ *   shrunk back to \ref MEM_POOL_GROW size.
+ */
 void memFreePoolPurge(flag untilOK)
 {
 /*E*/if(db9)getPoolStats(&i1,&j1_,&k1); if(db9)printf("e0: pool %ld stat %ld\n",poolTotalFree,i1+j1_);
@@ -2677,9 +2705,9 @@ void pntrZapLen(pntrString *s, long length) {
  * \ref pntrString.
  *
  * This function determines the length of the source \p t by scanning for a
- * terminating null pointer element.  The destination \p s must have enough
- * space for receiving this amount of pointers, including the terminal null
- * pointer.  Then the source pointers are copied beginning with that at the
+ * terminal null pointer element.  The destination \p s must have enough space
+ * for receiving this amount of pointers, including the terminal null pointer.
+ * Then the source pointers are copied beginning with that at the
  * lowest address to the destination area \p t, including the terminal null
  * pointer.
  *
@@ -2695,8 +2723,8 @@ void pntrZapLen(pntrString *s, long length) {
  *   - \p t is terminated by the first null pointer element.
  *   - the target array \p s must have enough free space to hold the source array
  *     \p t including the terminal null pointer.
- *   - \p s and \p t can overlap if \p t points to a later element than \p s
- *     (move left semantics)
+ *   - \p s and \p t can overlap if \p t points to a later or same element than
+ *     \p s (move left semantics).
  * \invariant
  *   If \p s is contained in a \ref block "block", its administrative header is
  *   NOT updated.
diff --git a/src/mmdata.h b/src/mmdata.h
index 36f486d4..18bc3999 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -307,6 +307,20 @@ extern flag g_globalDiscouragement; /* SET DISCOURAGEMENT */
 
 /* Allocation and deallocation in memory pool */
 void *poolFixedMalloc(long size /* bytes */);
+/*!
+ * \fn void *poolMalloc(long size)
+ * \brief allocates and initializes a new \ref block
+ *
+ * allocates a \ref block, first removing and using the last element of the
+ * \ref memFreePool.  If this block exists, but has not sufficient size, it is
+ * reallocated from the system.  If the pool is empty, a new \ref block of
+ * the given size is allocated from the system.  In any case, the header of the
+ * \ref block is properly initialized.
+ * \param[in] size (in bytes) of the block, not including the block header.
+ * \return a free and initialized block of memory with at least the requested
+ *   user space.
+ * \bug uses outOfMemory that can stack up endlessly
+ */
 void *poolMalloc(long size /* bytes */);
 /*!
  * \fn poolFree(void *ptr)
@@ -317,7 +331,8 @@ void *poolMalloc(long size /* bytes */);
  * added.
  * \param[in] ptr pointer to a \ref block.
  * \pre
- *   all memory pointed to by \p ptr is considered free.
+ *   all memory pointed to by \p ptr is considered free.  This holds even if it
+ *   it is kept in \ref memUsedPool. 
  * \post
  *   \ref poolTotalFree is updated
  * \bug calls outOfMemory, that can stack up endlessly
@@ -327,8 +342,8 @@ void poolFree(void *ptr);
  * \fn addToUsedPool(void *ptr)
  * \brief announces a block with free capacity for further allocation
  *
- * This function temporarily freezes the usage of a block for an old client, and
- * allows temporary reallocation of the free capacity to a new client.
+ * This function temporarily freezes the usage of a block for the current user,
+ * and allows temporary reallocation of the free capacity to a new client.
  * \n
  * The program maintains pools of memory blocks with free capacity.  In case of
  * demand such a \ref block can temporarily allocate this capacity for new
@@ -390,7 +405,7 @@ long getFreeSpace(long max);
 
 /* Fatal memory allocation error */
 /*!
- * \fn outOfMemory
+ * \fn outOfMemory(const char *msg)
  * \brief fatal memory allocation error.
  *
  * called when memory cannot be allocated, either because memory/address space
@@ -408,7 +423,7 @@ void outOfMemory(const char *msg);
 
 /* Bug check error */
 /*!
- * \fn bug
+ * \fn bug(int bugNum)
  */
 void bug(int bugNum);
 
@@ -672,6 +687,20 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
 /* String assignment - MUST be used to assign vstrings */
 /*!
  * \fn void pntrLet(pntrString **target, const pntrString *source)
+ * \param[in,out] target (not null) the address of a pointer pointing to the
+ *   first byte of a \ref block receiving the copied \p source.
+ * \param[in] source (not null) a pointer to the first \ref pntrString element
+ *   in a \ref block, to be copied from.
+ * \pre
+ *   - source does not contain NULL pointer, but is terminated by one.  This
+ *     NULL pointer is not part of the array, but must be present.
+ *   - the target \ref block does not contain used data.
+ * \post
+ *   - the \ref block \p target points to is filled with a copy of
+ *     \ref pntrString elements \p source points to, padded with a terminal
+ *     NULL, or an outOfMemory error is raised.
+ *   - due to a possible reallocation the pointer \p target points to may
+ *     change.
  */
 void pntrLet(pntrString **target, const pntrString *source);
 
@@ -700,8 +729,10 @@ temp_pntrString *pntrPSpace(long n);
  * \brief Determine the length of a pntrString held in a \ref block "block"
  * dedicated to it.
  *
- * returns the number of **used** pointers in the array pointed to by \p s,
- * derived from administrative data in the surrounding block.
+ * returns the number of **reserved** pointers in the array pointed to by \p s,
+ * derived solely from administrative data in the surrounding \ref block.  NULL
+ * pointer in the array are included, a trailing one is not required to
+ * determine the length.´
  *
  * \attention This is not the capacity of the array.
  * \param[in] s points to a element 0 of a \ref pntrString  embedded in a block
diff --git a/src/mmvstr.h b/src/mmvstr.h
index 21f9468a..6a1e31d2 100644
--- a/src/mmvstr.h
+++ b/src/mmvstr.h
@@ -335,7 +335,7 @@ void let(vstring *target, const char *source);
  *   The following parameters are pointers to NUL terminated strings as well,
  *   except for the last parameter that must be NULL.  It is allowed to
  *   duplicate parameters.
- * \return the concatenated \ref temp_string terminated by a NUL character.
+ * \return the concatenated \ref temp_vstring terminated by a NUL character.
  * \post the resulting string is pushed onto the \ref tempAllocStack.
  *   \ref db is updated.
  * \bug a stack overflow of \ref tempAllocStack is not handled correctly.
@@ -358,50 +358,50 @@ int linput(FILE *stream, const char *ask, vstring *target);
 /* Emulation of BASIC string functions */
 /* Indices are 1-based */
 /*!
- * \fn temp_vstring seg(const char *sin, long p1, long p2)
+ * \fn temp_vstring seg(const char *sin, long start, long stop)
  * Extracts a substring from a source and pushes it on \ref tempAllocStack.
  * Note: The bounding indices are 1-based and inclusive.
  *
  * \param[in] sin (not null) pointer to the NUL-terminated source text.
- * \param[in] p1 offset of the first byte of the substring, counted in bytes from
+ * \param[in] start offset of the first byte of the substring, counted in bytes from
  *   the first one of \p sin, a 1-based index.  A value less than 1 is
  *   internally corrected to 1, but it must not point beyond the terminating
- *   NUL of \p sin, if \p p1 <= \p p2.
- * \param[in] p2 offset of the last byte of the substring, counted in bytes from
+ *   NUL of \p sin, if \p start <= \p stop.
+ * \param[in] stop offset of the last byte of the substring, counted in bytes from
  *   the first one of \p sin, a 1-based index.  The natural bounds of this
- *   value are \p p1 - 1 and the length of \p sin.  Values outside of this
- *   range are internally corrected to the closer of these limits.  If \p p2 <
- *   \p p1 the empty string is returned.
+ *   value are \p start - 1 and the length of \p sin.  Values outside of this
+ *   range are internally corrected to the closer of these limits.  If \p stop
+ *   < \p start the empty string is returned.
  * \attention the indices are 1-based: seg("hello", 2, 3) == "el"!
  * \return a pointer to new allocated \ref temp_vstring referencing the
  *   requested substring, that is also pushed onto the top of
  *   \ref tempAllocStack
  * \pre
- *   \p p1 <= length(\p sin).
+ *   \p start <= length(\p sin).
  * \post
  *   A pointer to the substring is pushed on \ref tempAllocStack, even if it
  *   empty;
  * \warning not UTF-8 safe.
  * \bug a stack overflow of \ref tempAllocStack is not handled correctly;
  */
-temp_vstring seg(const char *sin, long p1, long p2);
+temp_vstring seg(const char *sin, long start, long stop);
 /*!
- * \fn temp_vstring mid(const char *sin, long p, long l)
+ * \fn temp_vstring mid(const char *sin, long start, long length)
  * Extracts a substring from a source and pushes it on \ref tempAllocStack
  *
  * \param[in] sin (not null) pointer to the NUL-terminated source text.
- * \param[in] p offset of the substring in bytes from the first byte of \p sin,
- *   1-based.  A value less than 1 is internally corrected to 1, but it must
- *   never point beyond the terminating NUL of \p sin.
- * \param[in] l length of substring in bytes.  Negative values are corrected to 0.
- *   If \p p + \p l exceeds the length of \p sin, then only the portion up
- *   to the terminating NUL is taken.
- * \attention the index \p p is 1-based: mid("hello", 2, 1) == "e"!
+ * \param[in] start offset of the substring in bytes from the first byte of
+ *   \p sin, 1-based.  A value less than 1 is internally corrected to 1, but it
+ *   must never point beyond the terminating NUL of \p sin.
+ * \param[in] length length of substring in bytes.  Negative values are
+ *   corrected to 0.  If \p start + \p length exceeds the length of \p sin,
+ *   then only the portion up to the terminating NUL is taken.
+ * \attention the index \p start is 1-based: mid("hello", 2, 1) == "e"!
  * \return a pointer to new allocated \ref temp_vstring referencing the
  *   requested substring, that is also pushed onto the top of
  *   \ref tempAllocStack
  * \pre
- *   \p p <= length(\p sin).  This must hold even if the requested length is
+ *   \p start <= length(\p sin).  This must hold even if the requested length is
  *   0, because its implementation in C requires the validity of the pointer,
  *   even if it is not dereferenced.
  * \post
@@ -410,7 +410,7 @@ temp_vstring seg(const char *sin, long p1, long p2);
  * \warning not UTF-8 safe.
  * \bug a stack overflow of \ref tempAllocStack is not handled correctly;
  */
-temp_vstring mid(const char *sin, long p, long l);
+temp_vstring mid(const char *sin, long start, long length);
 /*!
  * \fn temp_vstring left(const char *sin, long n)
  * \brief Extract leftmost n characters.

From 61a4c7837ead0b83fc5374315e0e19399950e8ef Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sat, 5 Mar 2022 14:02:03 +0100
Subject: [PATCH 19/42] fix doc of getPoolStats

---
 src/mmdata.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 18bc3999..c93e6942 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -370,7 +370,7 @@ void addToUsedPool(void *ptr);
 void memFreePoolPurge(flag untilOK);
 /* Statistics */
 /*!
- * \fn getPoolStats
+ * \fn getPoolStats(long *freeAlloc, long *usedAlloc, long *usedActual)
  * \brief Provide information about memory in pools at the instant of call.
  *
  * Return the overall statistics about the pools \ref memFreePool

From 702ca83f12e4df193841db6a57b4ae0489ccd387 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sat, 5 Mar 2022 15:53:01 +0100
Subject: [PATCH 20/42] doc pntrTempAlloc

---
 src/metamath.c |  4 ++--
 src/mmdata.c   | 21 +++++++++++++++++++--
 src/mmdata.h   | 47 ++++++++++++++++++++++++++++++++++-------------
 3 files changed, 55 insertions(+), 17 deletions(-)

diff --git a/src/metamath.c b/src/metamath.c
index 970ce4c0..cfcf7549 100644
--- a/src/metamath.c
+++ b/src/metamath.c
@@ -731,8 +731,8 @@ void command(int argc, char *argv[]);
  * will start main with \p argc set to 2, argv[0] to "read set.mm", argv[1]
  * to "verify proof *" (both without quotes) and argv[2] to NULL.
  * Returning 0 indicates successful completion, anything else some kind of
- failure.
- * For details see \ref https://en.cppreference.com/w/cpp/language/main_function.
+ * failure.
+ * For details see https://en.cppreference.com/w/cpp/language/main_function.
  */
 int main(int argc, char *argv[]) {
 
diff --git a/src/mmdata.c b/src/mmdata.c
index f9e03b96..5ff68f05 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -2449,7 +2449,7 @@ long g_pntrStartTempAllocStack = 0;   /* Where to start freeing temporary alloca
                                     when pntrLet() is called (normally 0, except in
                                     special nested vstring functions) */
 /*!
- * \var pntrTempAllocStack
+ * \var pntrString *pntrTempAllocStack[]
  * \brief a \ref stack "stack" of \ref temp_pntrString.
  *
  * Holds pointers to temporarily allocated data of type \ref pntrString.  Such
@@ -2458,7 +2458,24 @@ long g_pntrStartTempAllocStack = 0;   /* Where to start freeing temporary alloca
  */
 pntrString *pntrTempAllocStack[M_MAX_ALLOC_STACK];
 
-
+/*!
+ * \fn temp_pntrString *pntrTempAlloc(long size)
+ * \par size > 0
+ * allocates a \ref block capable of holding \p size \ref pntrString entries
+ * and pushes it onto the \ref pntrTempAllocStack.
+ * \par size == 0
+ * pops off all entries from the \ref pntrTempAllocStack and adds them to the
+ * \ref memFreePool.
+ * \param[in] size count of \ref pntrString entries.  This value must include
+ *   a terminal NULL pointer if needed.
+ * \return a pointer to the allocated \ref block, or NULL if deallocation only
+ * \pre
+ *   \p size ==0: all entries in from \ref pntrTempAllocStack from
+ *   \ref g_pntrTempAllocStackStart do not contain relevant data any more.
+ * \post
+ *   - Exits on out-of-memory
+ *   - updates \ref db2
+ */
 temp_pntrString *pntrTempAlloc(long size) {
                                 /* pntrString memory allocation/deallocation */
   /* When "size" is >0, "size" instances of pntrString are allocated. */
diff --git a/src/mmdata.h b/src/mmdata.h
index c93e6942..a7078e87 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -15,7 +15,7 @@
 
 /* debugging flags & variables */
 /*!
- * \var db
+ * \var long db
  * \brief bytes held by vstring instances outside of the stack of temporaries
  *
  * monitors the number of bytes (including the terminal NUL) currently used in
@@ -31,7 +31,7 @@
 /*E*/extern long db;
 /*E*/extern long db0;
 /*!
- * \var db1
+ * \var long db1
  * \brief bytes held by vstring instances inside of the stack of temporaries
  *
  * monitors the number of bytes currently pointed to by \ref vstring pointers
@@ -43,6 +43,11 @@
  * \bug Seems never be displayed.
  */
 /*E*/extern long db1;
+/*!
+ * \var long db2
+ * Bytes held in \ref blocks managed in \ref tempAllocStack
+ * "temporary pointer stacks".
+ */
 /*E*/extern long db2;
 /*!
  * \var db3
@@ -315,11 +320,11 @@ void *poolFixedMalloc(long size /* bytes */);
  * \ref memFreePool.  If this block exists, but has not sufficient size, it is
  * reallocated from the system.  If the pool is empty, a new \ref block of
  * the given size is allocated from the system.  In any case, the header of the
- * \ref block is properly initialized.
+ * \ref block is properly initialized.  Exits program on out of memory
+ * condition.
  * \param[in] size (in bytes) of the block, not including the block header.
  * \return a free and initialized block of memory with at least the requested
- *   user space.
- * \bug uses outOfMemory that can stack up endlessly
+ *   user space.  Exit on out-of-memory
  */
 void *poolMalloc(long size /* bytes */);
 /*!
@@ -327,15 +332,15 @@ void *poolMalloc(long size /* bytes */);
  *
  * Removes \p ptr from the \ref memUsedPool, if it is listed there.  Then tries
  * adding it to the \ref memFreePool.  If this pool is full, it is increased by
- * \ref MEM_POOL_GROW.  If this fails, an error is created, else \p ptr is
+ * \ref MEM_POOL_GROW.  If this fails, the program is exited, else \p ptr is
  * added.
  * \param[in] ptr pointer to a \ref block.
  * \pre
  *   all memory pointed to by \p ptr is considered free.  This holds even if it
  *   it is kept in \ref memUsedPool. 
  * \post
- *   \ref poolTotalFree is updated
- * \bug calls outOfMemory, that can stack up endlessly
+ *   - \ref poolTotalFree is updated
+ *   - Exit on out-of-memory (the \ref memFreePool overflows)
  */
 void poolFree(void *ptr);
 /*!
@@ -363,7 +368,7 @@ void poolFree(void *ptr);
  * \post
  *   - \ref poolTotalFree is the current free space in bytes in both pools.
  *   - A full \ref block is not added to \ref memUsedPool by this function.
- * \bug calls outOfMemory, that can stack up endlessly
+ *   - Exit on out-of-memory (\ref memUsedPool overflows)
  */
 void addToUsedPool(void *ptr);
 /* Purges reset memory pool usage */
@@ -375,7 +380,7 @@ void memFreePoolPurge(flag untilOK);
  *
  * Return the overall statistics about the pools \ref memFreePool
  * "free block array" and the \ref memUsedPool "used block array".  In MEMORY
- * STATUS mode ON, a diagnostic message compares the the contents of
+ * STATUS mode ON, a diagnostic message compares the contents of
  * \ref poolTotalFree to the values found in this statistics.  They should not
  * differ!
  *
@@ -406,7 +411,7 @@ long getFreeSpace(long max);
 /* Fatal memory allocation error */
 /*!
  * \fn outOfMemory(const char *msg)
- * \brief fatal memory allocation error.
+ * \brief exit after fatal memory allocation error.
  *
  * called when memory cannot be allocated, either because memory/address space
  * is physically exhausted, or because administrative structures would overflow.
@@ -664,12 +669,27 @@ long compressedProofSize(const nmbrString *proof, long statemNum);
 /*!
  * \var long g_pntrTempAllocStackTop
  *
- * Index of the current top af the \ref stack "stack" \ref pntrTempAlloc.
+ * Index of the current top of the \ref stack "stack" \ref pntrTempAlloc.
  * New data is pushed from this location on if space available.
  *
  * \invariant always refers the null pointer element behind the valid data.
  */
 extern long g_pntrTempAllocStackTop;   /* Top of stack for pntrTempAlloc function */
+/*!
+ * \var long g_pntrTempAllocStackStart
+ *
+ * Index of the first entry of the \ref stack "stack" \ref pntrTempAllocStack
+ * eligible for deallocation on the next call to \ref pntrTempAlloc.  Entries
+ * below this value are considered not dependent on the value at this index,
+ * but entries above are.  So when this entry gets deallocated, dependent ones
+ * should follow suit.  A function like \ref pntrTempAlloc or \ref pntrLet
+ * manage this automatic deallocation.
+ * \n
+ * Nested functions using the \ref pntrTempAllocStack usually save the current
+ * value and set it to \ref g_pntrTempAllocStackTop, so they can create their
+ * local dependency chain.  On return the saved value is restored.
+ * \invariant always less or equal to \ref g_pntrTempAllocStackTop.
+ */
 extern long g_pntrStartTempAllocStack; /* Where to start freeing temporary
     allocation when pntrLet() is called (normally 0, except for nested
     pntrString functions) */
@@ -698,7 +718,8 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
  * \post
  *   - the \ref block \p target points to is filled with a copy of
  *     \ref pntrString elements \p source points to, padded with a terminal
- *     NULL, or an outOfMemory error is raised.
+ *     NULL.
+ *   - Exit on out-of-memory
  *   - due to a possible reallocation the pointer \p target points to may
  *     change.
  */

From 1dda3d7aa94ca872eb6c53848225edc52c0b8049 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sat, 5 Mar 2022 17:54:03 +0100
Subject: [PATCH 21/42] fine tuning

---
 src/mmdata.h | 37 ++++++++++++++++++++++++++-----------
 1 file changed, 26 insertions(+), 11 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index a7078e87..4d521370 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -322,7 +322,8 @@ void *poolFixedMalloc(long size /* bytes */);
  * the given size is allocated from the system.  In any case, the header of the
  * \ref block is properly initialized.  Exits program on out of memory
  * condition.
- * \param[in] size (in bytes) of the block, not including the block header.
+ * \param[in] size (in bytes) of the block, not including the block header, but
+ *   including space for a terminal NULL.
  * \return a free and initialized block of memory with at least the requested
  *   user space.  Exit on out-of-memory
  */
@@ -336,11 +337,14 @@ void *poolMalloc(long size /* bytes */);
  * added.
  * \param[in] ptr pointer to a \ref block.
  * \pre
- *   all memory pointed to by \p ptr is considered free.  This holds even if it
- *   it is kept in \ref memUsedPool. 
+ *   - \p ptr was previously allocated.
+ *   - all memory pointed to by \p ptr is considered free.  This holds even if it
+ *     it is kept in \ref memUsedPool. 
  * \post
  *   - \ref poolTotalFree is updated
  *   - Exit on out-of-memory (the \ref memFreePool overflows)
+ * \attention never submit a \p ptr referring to memory not on the heap, like
+ *   NULL_PTRSTRING.
  */
 void poolFree(void *ptr);
 /*!
@@ -410,7 +414,7 @@ long getFreeSpace(long max);
 
 /* Fatal memory allocation error */
 /*!
- * \fn outOfMemory(const char *msg)
+ * \fn void outOfMemory(const char *msg)
  * \brief exit after fatal memory allocation error.
  *
  * called when memory cannot be allocated, either because memory/address space
@@ -428,7 +432,7 @@ void outOfMemory(const char *msg);
 
 /* Bug check error */
 /*!
- * \fn bug(int bugNum)
+ * \fn void bug(int bugNum)
  */
 void bug(int bugNum);
 
@@ -707,21 +711,31 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
 /* String assignment - MUST be used to assign vstrings */
 /*!
  * \fn void pntrLet(pntrString **target, const pntrString *source)
+ * Copies the \ref pntrString elements of \p source to the beginning of a
+ * \ref block referenced by \p target.  If necessary, the \p target block is
+ * reallocated, and if it is, it gets twice the needed size to account for
+ * future growing.  If the \p target block is only partially used after copy it
+ * is added to the \ref memUsedPool.  If \p source is empty, the \p target is
+ * 
  * \param[in,out] target (not null) the address of a pointer pointing to the
- *   first byte of a \ref block receiving the copied \p source.
+ *   first byte of a \ref block receiving the copied elements of \p source.
  * \param[in] source (not null) a pointer to the first \ref pntrString element
  *   in a \ref block, to be copied from.
  * \pre
  *   - source does not contain NULL pointer, but is terminated by one.  This
  *     NULL pointer is not part of the array, but must be present.
- *   - the target \ref block does not contain used data.
+ *   - the target \ref block does not contain any valuable data.
  * \post
  *   - the \ref block \p target points to is filled with a copy of
  *     \ref pntrString elements \p source points to, padded with a terminal
  *     NULL.
- *   - Exit on out-of-memory
  *   - due to a possible reallocation the pointer \p target points to may
  *     change.
+ *   - updates \ref db3 and \ref poolTotalFree.
+ *   - Exit on out-of-memory
+ * \bug If the \p target block is full after the copy operation, it is not
+ *   necessarily removed from the \ref memUsedPool, although other
+ *   functions like \ref addToUsedPool do not support this.
  */
 void pntrLet(pntrString **target, const pntrString *source);
 
@@ -751,9 +765,10 @@ temp_pntrString *pntrPSpace(long n);
  * dedicated to it.
  *
  * returns the number of **reserved** pointers in the array pointed to by \p s,
- * derived solely from administrative data in the surrounding \ref block.  NULL
- * pointer in the array are included, a trailing one is not required to
- * determine the length.´
+ * derived solely from administrative data in the surrounding \ref block. Thus,
+ * the value is valid, even if data has not yet been transferred to the
+ * reserved space, and the terminal NULL is not safely recognized. The returned
+ * value excludes the space set aside for a terminal NULL.
  *
  * \attention This is not the capacity of the array.
  * \param[in] s points to a element 0 of a \ref pntrString  embedded in a block

From 023eda45c5c8b3dd9e85b59a853d6bd7d5b2bb5c Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sat, 5 Mar 2022 18:05:46 +0100
Subject: [PATCH 22/42] be more precise with temp_pntrString

---
 src/mmdata.h | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 4d521370..2bd32570 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -160,8 +160,10 @@ typedef nmbrString temp_nmbrString;
  * \brief a single \ref pntrString element for use in a \ref stack "stack".
  *
  * These elements are pushed onto and popped off a \ref stack 
- * "stack of temporary data".  Special commands can free all pointers on and
- * after a particular one in such a stack.
+ * "stack of temporary data".  All pointer of this type should ONLY refer to
+ * adynamically llocated memory on the heap.  Special commands support
+ * dependency tracking and free all pointers on and after a particular one in
+ * such a stack. 
  */
 typedef pntrString temp_pntrString;
 

From ff8f9d19c1b07a1be95fee615df6314a6229af14 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sat, 5 Mar 2022 20:05:05 +0100
Subject: [PATCH 23/42] improve doc of poolMalloc

---
 src/mmdata.h | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 2bd32570..fa04596d 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -115,18 +115,18 @@ typedef long nmbrString; /* String of numbers */
  * \brief an array (maybe of size 1) of untyped pointers (void*)
  *
  * In general this array is organized like a stack: the number of elements in
- * the pntrString grows and shrinks during program flow, values are pushed and
- * popped at the end.  Such a stack is embedded in a \ref block that contains
- * administrative information about the stack.  The stack begins with
+ * the pntrString array grows and shrinks during program flow, values are
+ * pushed and popped at the end.  Such a stack is embedded in a \ref block that
+ * contains administrative information about the stack.  The stack begins with
  * element 0, and the administrative information is accessed through negative
  * indices, but need reinterpretation then.  To allow iterating through the
- * tail of the array from a certain element on, the array terminates with a
+ * tail of an array from a certain element on, an array terminates with a
  * null pointer.  This type of usage forbids null pointer as ordinary elements,
  * and the terminal null pointer is not part of the data in the array.
  *
  * To summarize the usages of this type:
  * - If you want to resize the array/stack you need a pointer to element 0.
- * - You can iterate from an arbitrary pointer to the end.
+ * - You can iterate from an arbitrary element to the end.
  * - Sometimes pntrString denotes an isolated element, not embedded in a
  *   greater array.
  *
@@ -161,7 +161,7 @@ typedef nmbrString temp_nmbrString;
  *
  * These elements are pushed onto and popped off a \ref stack 
  * "stack of temporary data".  All pointer of this type should ONLY refer to
- * adynamically llocated memory on the heap.  Special commands support
+ * dynamically allocated memory on the heap.  Special commands support
  * dependency tracking and free all pointers on and after a particular one in
  * such a stack. 
  */
@@ -324,10 +324,10 @@ void *poolFixedMalloc(long size /* bytes */);
  * the given size is allocated from the system.  In any case, the header of the
  * \ref block is properly initialized.  Exits program on out of memory
  * condition.
- * \param[in] size (in bytes) of the block, not including the block header, but
- *   including space for a terminal NULL.
- * \return a free and initialized block of memory with at least the requested
- *   user space.  Exit on out-of-memory
+ * \param[in] size (in bytes) of the block, not including the block header.
+ * \return a \ref block with enough capacity for \p size bytes of data.  The
+ *   data space is filled with random contents, but in the block header its
+ *   \p size is noted.   Exit on out-of-memory
  */
 void *poolMalloc(long size /* bytes */);
 /*!
@@ -339,7 +339,7 @@ void *poolMalloc(long size /* bytes */);
  * added.
  * \param[in] ptr pointer to a \ref block.
  * \pre
- *   - \p ptr was previously allocated.
+ *   - \p ptr was previously dynamically allocated.
  *   - all memory pointed to by \p ptr is considered free.  This holds even if it
  *     it is kept in \ref memUsedPool. 
  * \post

From c58210d9bc895d284c4ff6ecb35796ee8d6b0d1e Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 02:17:07 +0100
Subject: [PATCH 24/42] do the best to ref to bug()

---
 src/mmdata.h | 12 +++++++-----
 src/mmvstr.c |  6 +++---
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index fa04596d..4d75a250 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -327,7 +327,7 @@ void *poolFixedMalloc(long size /* bytes */);
  * \param[in] size (in bytes) of the block, not including the block header.
  * \return a \ref block with enough capacity for \p size bytes of data.  The
  *   data space is filled with random contents, but in the block header its
- *   \p size is noted.   Exit on out-of-memory
+ *   \p size is noted.´   Exit on out-of-memory
  */
 void *poolMalloc(long size /* bytes */);
 /*!
@@ -364,13 +364,13 @@ void poolFree(void *ptr);
  * \n
  * Before \p ptr is added to \ref memUsedPool, the pool size is checked and
  * increased by \ref MEM_POOL_GROW if full.  This may lead to out-of-memory
- * \ref bug "bugs".  But if \p prt is added to the end of the \ref memUsedPool,
+ * \ref outOfMemory "exit".  But if \p ptr is added to the end of the \ref memUsedPool,
  * \ref poolTotalFree is updated.
  * \param[in] ptr pointer to a \ref block.
  * \pre
  *   the block is \ref fragmentation "fragmented" (contains unused memory)
- *   If it is full \ref bug is called and the function returns without further
- *   action.
+ *   If it is full, \ref bugfn "bug" is called and the function returns without
+ *   further action.
  * \post
  *   - \ref poolTotalFree is the current free space in bytes in both pools.
  *   - A full \ref block is not added to \ref memUsedPool by this function.
@@ -401,7 +401,7 @@ void memFreePoolPurge(flag untilOK);
  * \param[out] usedActual (not-null) address of a long variable receiving the
  * accumulated bytes consumed by usage so far.  This value includes the hidden
  * header of the block.
- * \pre Do not call within bug().\n
+ * \pre Do not call within \ref bugfn "bug".\n
  *   Submit only non-null pointers, even if not all information is requested.\n
  *   Pointers to irrelevant information may be the same.
  * \post Statistic data is copied to the locations the parameters point to.
@@ -434,7 +434,9 @@ void outOfMemory(const char *msg);
 
 /* Bug check error */
 /*!
+ * \anchor bugfn
  * \fn void bug(int bugNum)
+ * \param[in] bugNum
  */
 void bug(int bugNum);
 
diff --git a/src/mmvstr.c b/src/mmvstr.c
index 9392d4c8..84206592 100644
--- a/src/mmvstr.c
+++ b/src/mmvstr.c
@@ -95,7 +95,7 @@ void freeTempAlloc(void) {
  * \fn pushTempAlloc(void *mem)
  * \brief pushes a pointer onto the \ref tempAllocStack.
  *
- * In case of a stack overflow \ref bug is called.  This function is low level
+ * In case of a stack overflow \ref bugfn "bug" is called.  This function is low level
  * that does not ensure that invariants of \ref tempAllocStack are kept.
  *
  * \param mem (not null) points to either a non-mutable empty string, or
@@ -131,8 +131,8 @@ static void pushTempAlloc(void *mem)
  *   \ref tempAllocStack
  *
  * This low level function does NOT initialize the allocated memory.  If the
- * allocation on the heap fails, \ref bug is called.  The statistic value
- * \ref db1 is updated.
+ * allocation on the heap fails, \ref bugfn "bug" is called.  The statistic
+ * value \ref db1 is updated.
  *
  * \param size (> 0) number of bytes to allocate on the heap.  If the memory is
  *   intended to hold NUL terminated text, then size must account for the final

From d7ebf7752bc3ceb1df48b7cb049ba40a4a91ef20 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 03:07:18 +0100
Subject: [PATCH 25/42] better doc early phase of pntrString allocation

---
 src/mmdata.c |  5 ++++-
 src/mmdata.h | 20 ++++++++++++++------
 2 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/src/mmdata.c b/src/mmdata.c
index 5ff68f05..d6dcb0ea 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -2468,11 +2468,14 @@ pntrString *pntrTempAllocStack[M_MAX_ALLOC_STACK];
  * \ref memFreePool.
  * \param[in] size count of \ref pntrString entries.  This value must include
  *   a terminal NULL pointer if needed.
- * \return a pointer to the allocated \ref block, or NULL if deallocation only
+ * \return a pointer to the allocated \ref block, or NULL if deallocation
+ *   requested
  * \pre
  *   \p size ==0: all entries in from \ref pntrTempAllocStack from
  *   \ref g_pntrTempAllocStackStart do not contain relevant data any more.
  * \post
+ *   - \p size > 0: memory for \p size entries is reserved in the \ref block
+ *     "block's" header, but the data is still random.
  *   - Exits on out-of-memory
  *   - updates \ref db2
  */
diff --git a/src/mmdata.h b/src/mmdata.h
index 4d75a250..89b2d365 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -51,8 +51,8 @@
 /*E*/extern long db2;
 /*!
  * \var db3
- * \brief monitors the de/allocations of nmbrString and pntrString outside of
- * temporary arrays.
+ * \brief monitors the de/allocations of nmbrString and \ref pntrString outside
+ * of temporary arrays.
  *
  * The number of bytes held in blocks dedicated to global data.  There exist
  * also temporary stacks, but they are not considered here.  Useful to see
@@ -123,6 +123,12 @@ typedef long nmbrString; /* String of numbers */
  * tail of an array from a certain element on, an array terminates with a
  * null pointer.  This type of usage forbids null pointer as ordinary elements,
  * and the terminal null pointer is not part of the data in the array.
+ * \n
+ * The length of a pntrString array is implicitely given by a terminal NULL
+ * pointer.  If this array is held in a \ref block, its size can also be
+ * determined from its header's administrative data.  Both values must be kept
+ * synchronized.  In early phases of memory allocation, when data wasn't
+ * assigned yet, this need not hold.
  *
  * To summarize the usages of this type:
  * - If you want to resize the array/stack you need a pointer to element 0.
@@ -325,9 +331,11 @@ void *poolFixedMalloc(long size /* bytes */);
  * \ref block is properly initialized.  Exits program on out of memory
  * condition.
  * \param[in] size (in bytes) of the block, not including the block header.
- * \return a \ref block with enough capacity for \p size bytes of data.  The
- *   data space is filled with random contents, but in the block header its
- *   \p size is noted.´   Exit on out-of-memory
+ * \return a \ref block with enough capacity for \p size bytes of data.
+ *  \post
+ *    - The \ref block "block's" header denotes \p size bytes are occupied, but
+ *      they yet contain random data.
+ *    - Exit on out-of-memory.
  */
 void *poolMalloc(long size /* bytes */);
 /*!
@@ -339,7 +347,7 @@ void *poolMalloc(long size /* bytes */);
  * added.
  * \param[in] ptr pointer to a \ref block.
  * \pre
- *   - \p ptr was previously dynamically allocated.
+ *   - \p ptr refers to dynamically allocated memory on the heap.
  *   - all memory pointed to by \p ptr is considered free.  This holds even if it
  *     it is kept in \ref memUsedPool. 
  * \post

From bc48424e96c0291b5a8c2005098611089865ed3b Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 11:48:28 +0100
Subject: [PATCH 26/42] describe temporary stacks in more detail

---
 src/mmdata.c | 35 ++++++++++++++++++++++++++---------
 src/mmdata.h |  2 +-
 2 files changed, 27 insertions(+), 10 deletions(-)

diff --git a/src/mmdata.c b/src/mmdata.c
index d6dcb0ea..92c0aa66 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -167,17 +167,32 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
  * ubiquitous and frequent, that the processor, and all relevant program
  * languages provide simple mechanisms for de/allocation of such __local__
  * data.  Metamath is no exception to this.
+ *
  * While the C compiler silently cares about __local__ variables, it must not
  * interfere with data managed by a \ref suballocation "Suballocator".  Instead
  * of tracking all __locally__ created memory individually for later
- * deallocation, a stack like \ref Pool "pool" allows a command like
- * `free all memory` that has been created after a certain point.  This greatly
- * automatizes handling of these data.
+ * deallocation, a stack like \ref Pool "pool" is used to automate this
+ * handling.
+ *
+ * Stacks of temporary data only contain pointers to dynamically allocated
+ * memory from the heap or the \ref suballocator.  This stack functions like an
+ * operand stack.  A final result depends on fragments, temporary results and
+ * similar, all pushed onto this stack.  When the final operation is executed,
+ * and its result is persisted in some variable, the dependency on its
+ * temporary operands ceases.  Consequently, they should be freed again.  To
+ * automate this operation,  such a stack maintains a __start__ index.  A
+ * client saves this value and sets it to the current stack top, then starts
+ * pushing dynamically allocated operands on the stack.  After the result is
+ * persisted, all entries beginning with the element at index  __start__ are
+ * deallocated again, and the stack top is reset to the __start__ value, while
+ * the __start__ value is reset to the saved value, to accomodate nesting of
+ * this procedure.
  *
- * A stack is not the same as a \ref block "block", though similar.  Like a
- * block it is defined as an array of elements, but it comes with no hidden
- * header.  Instead openly accessible stack pointer (actually indices) directly
- * support stack semantics.
+ * This scheme needs a few conditions to be met:
+ * - No operand is used in more than one evaluation context;
+ * - Operations are executed strictly sequential, or in a nested manner. No two
+ *   operations interleave pushing operands.
+ *   push operands interleaved
  */
 
 /* Memory pools are used to reduce the number of malloc and alloc calls that
@@ -2452,9 +2467,11 @@ long g_pntrStartTempAllocStack = 0;   /* Where to start freeing temporary alloca
  * \var pntrString *pntrTempAllocStack[]
  * \brief a \ref stack "stack" of \ref temp_pntrString.
  *
- * Holds pointers to temporarily allocated data of type \ref pntrString.  Such
+ * Holds pointers to temporarily allocated data of type \ref temp_pntrString.  Such
  * a \ref stack "stack" contains strictly __local__ data of a function, not
  * accessed from outer levels.
+ * \bug The element type should be temp_pntrString, because a NULL_PNTRSTRING
+ *   must not be pushed on the stack.
  */
 pntrString *pntrTempAllocStack[M_MAX_ALLOC_STACK];
 
@@ -2476,8 +2493,8 @@ pntrString *pntrTempAllocStack[M_MAX_ALLOC_STACK];
  * \post
  *   - \p size > 0: memory for \p size entries is reserved in the \ref block
  *     "block's" header, but the data is still random.
- *   - Exits on out-of-memory
  *   - updates \ref db2
+ *   - Exits on out-of-memory
  */
 temp_pntrString *pntrTempAlloc(long size) {
                                 /* pntrString memory allocation/deallocation */
diff --git a/src/mmdata.h b/src/mmdata.h
index 89b2d365..e15769d4 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -410,7 +410,7 @@ void memFreePoolPurge(flag untilOK);
  * accumulated bytes consumed by usage so far.  This value includes the hidden
  * header of the block.
  * \pre Do not call within \ref bugfn "bug".\n
- *   Submit only non-null pointers, even if not all information is requested.\n
+ *   Submit only non-null pointers, even if not all information is needed.\n
  *   Pointers to irrelevant information may be the same.
  * \post Statistic data is copied to the locations the parameters point to.
  */

From 0f3adf21967b8866a28625ffb795e9f59a268d16 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 12:02:26 +0100
Subject: [PATCH 27/42] extend description of pntrTempAllocStack

---
 src/mmdata.c | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/mmdata.c b/src/mmdata.c
index 92c0aa66..9051aa09 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -2468,8 +2468,11 @@ long g_pntrStartTempAllocStack = 0;   /* Where to start freeing temporary alloca
  * \brief a \ref stack "stack" of \ref temp_pntrString.
  *
  * Holds pointers to temporarily allocated data of type \ref temp_pntrString.  Such
- * a \ref stack "stack" contains strictly __local__ data of a function, not
- * accessed from outer levels.
+ * a \ref stack "stack" is primarily designed to function like a stack for
+ * temporary allocated ad hoc operands, as described in \ref stack.  The stack top
+ * index is \ref g_pntrTempAllocStackTop, always refering to the next push
+ * position.  The \ref g_pntrStartTempAllocStack supports nested operations by
+ * indicating where the operands for the upcoming operation start from.
  * \bug The element type should be temp_pntrString, because a NULL_PNTRSTRING
  *   must not be pushed on the stack.
  */

From 9149544a12a6546f8c5711c60f07226af070096b Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 13:14:40 +0100
Subject: [PATCH 28/42] improve doc of pntrLet

---
 src/mmdata.c | 17 ++++++++++++-----
 src/mmdata.h | 18 ++++++++++++++----
 2 files changed, 26 insertions(+), 9 deletions(-)

diff --git a/src/mmdata.c b/src/mmdata.c
index 9051aa09..37e791c5 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -2468,11 +2468,16 @@ long g_pntrStartTempAllocStack = 0;   /* Where to start freeing temporary alloca
  * \brief a \ref stack "stack" of \ref temp_pntrString.
  *
  * Holds pointers to temporarily allocated data of type \ref temp_pntrString.  Such
- * a \ref stack "stack" is primarily designed to function like a stack for
- * temporary allocated ad hoc operands, as described in \ref stack.  The stack top
- * index is \ref g_pntrTempAllocStackTop, always refering to the next push
- * position.  The \ref g_pntrStartTempAllocStack supports nested operations by
- * indicating where the operands for the upcoming operation start from.
+ * a \ref stack "stack" is primarily designed to operate like one for temporary
+ * allocated ad hoc operands, as described in \ref stack.  The stack top index
+ * is \ref g_pntrTempAllocStackTop, always refering to the next push position.
+ * The \ref g_pntrStartTempAllocStack supports nested operations by indicating
+ * where the operands for the upcoming operation start from.
+ * \attention A \ref pntrString consists of an array of pointers.  These
+ *   pointers may themself refer data that needs a clean up, when the last
+ *   reference  to it disappears (such as deallocating memory for example).
+ *   There is no automatic procedure handling such cases when pointers are
+ *   popped off the stack to be freed.
  * \bug The element type should be temp_pntrString, because a NULL_PNTRSTRING
  *   must not be pushed on the stack.
  */
@@ -2498,6 +2503,8 @@ pntrString *pntrTempAllocStack[M_MAX_ALLOC_STACK];
  *     "block's" header, but the data is still random.
  *   - updates \ref db2
  *   - Exits on out-of-memory
+ * \bug it is unfortunate that the same function is used for opposite
+ *   operations like de-/allocation.
  */
 temp_pntrString *pntrTempAlloc(long size) {
                                 /* pntrString memory allocation/deallocation */
diff --git a/src/mmdata.h b/src/mmdata.h
index e15769d4..4393e0d2 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -128,7 +128,7 @@ typedef long nmbrString; /* String of numbers */
  * pointer.  If this array is held in a \ref block, its size can also be
  * determined from its header's administrative data.  Both values must be kept
  * synchronized.  In early phases of memory allocation, when data wasn't
- * assigned yet, this need not hold.
+ * assigned yet, this need not hold, though.
  *
  * To summarize the usages of this type:
  * - If you want to resize the array/stack you need a pointer to element 0.
@@ -728,14 +728,22 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
  * reallocated, and if it is, it gets twice the needed size to account for
  * future growing.  If the \p target block is only partially used after copy it
  * is added to the \ref memUsedPool.  If \p source is empty, the \p target is
- * 
+ * to \ref NULL_PNTRSTRING.
+ * \n
+ * It is assumed that the value persisted in \p target is in fact computed from
+ * temporary operands in \ref pntrTempAllocStack.  All blocks starting with
+ * the element at \ref g_pntrTempAllocStackStart are returned to the
+ * \ref memFreePool.
+ * \attention freed \ref block "blocks" contain \ref pntrString instances.
+ *   See \ref pntrTempAllocStack to learn how this free process can be
+ *   dangerous if no precautions are taken.
  * \param[in,out] target (not null) the address of a pointer pointing to the
  *   first byte of a \ref block receiving the copied elements of \p source.
  * \param[in] source (not null) a pointer to the first \ref pntrString element
  *   in a \ref block, to be copied from.
  * \pre
- *   - source does not contain NULL pointer, but is terminated by one.  This
- *     NULL pointer is not part of the array, but must be present.
+ *   - source does not contain NULL pointerelements , but is terminated by one.
+ *     This final NULL pointer is not part of the array, but must be present.
  *   - the target \ref block does not contain any valuable data.
  * \post
  *   - the \ref block \p target points to is filled with a copy of
@@ -743,6 +751,8 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
  *     NULL.
  *   - due to a possible reallocation the pointer \p target points to may
  *     change.
+ *   - The stack pointer of \ref pntrTempAllocStack is reset to
+ *     \ref g_pntrTempAllocStackStart
  *   - updates \ref db3 and \ref poolTotalFree.
  *   - Exit on out-of-memory
  * \bug If the \p target block is full after the copy operation, it is not

From 42fa455433d392262071e8bae8413f4d455a2992 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 13:30:13 +0100
Subject: [PATCH 29/42] improve doc of pntrLet

---
 src/mmdata.h | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 4393e0d2..63998c35 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -736,15 +736,17 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
  * \ref memFreePool.
  * \attention freed \ref block "blocks" contain \ref pntrString instances.
  *   See \ref pntrTempAllocStack to learn how this free process can be
- *   dangerous if no precautions are taken.
+ *   dangerous if insufficient precautions are taken.
  * \param[in,out] target (not null) the address of a pointer pointing to the
  *   first byte of a \ref block receiving the copied elements of \p source.
  * \param[in] source (not null) a pointer to the first \ref pntrString element
  *   in a \ref block, to be copied from.
  * \pre
- *   - source does not contain NULL pointerelements , but is terminated by one.
- *     This final NULL pointer is not part of the array, but must be present.
+ *   - source does not contain NULL pointer elements , but is terminated by
+ *     one.  This final NULL pointer is not part of the array, but must be present.
  *   - the target \ref block does not contain any valuable data.
+ *   - all \ref pntrString elements held in \ref pntrTempAllocStack can be
+ *     discarded without losing relevant references.
  * \post
  *   - the \ref block \p target points to is filled with a copy of
  *     \ref pntrString elements \p source points to, padded with a terminal
@@ -752,7 +754,9 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
  *   - due to a possible reallocation the pointer \p target points to may
  *     change.
  *   - The stack pointer of \ref pntrTempAllocStack is reset to
- *     \ref g_pntrTempAllocStackStart
+ *     \ref g_pntrTempAllocStackStart and all referenced
+ *     \ref block "blocks" on and beyond that are returned to the
+ *     \ref memFreePool.
  *   - updates \ref db3 and \ref poolTotalFree.
  *   - Exit on out-of-memory
  * \bug If the \p target block is full after the copy operation, it is not

From 515fec49405d8ed57b1045023eef0e7bf7d3b4fb Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 13:58:02 +0100
Subject: [PATCH 30/42] fix doc of let

---
 src/mmdata.h |  4 ++--
 src/mmvstr.h | 24 +++++++++++-------------
 2 files changed, 13 insertions(+), 15 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 63998c35..7ec2b500 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -728,7 +728,7 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
  * reallocated, and if it is, it gets twice the needed size to account for
  * future growing.  If the \p target block is only partially used after copy it
  * is added to the \ref memUsedPool.  If \p source is empty, the \p target is
- * to \ref NULL_PNTRSTRING.
+ * set to \ref NULL_PNTRSTRING.
  * \n
  * It is assumed that the value persisted in \p target is in fact computed from
  * temporary operands in \ref pntrTempAllocStack.  All blocks starting with
@@ -745,7 +745,7 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
  *   - source does not contain NULL pointer elements , but is terminated by
  *     one.  This final NULL pointer is not part of the array, but must be present.
  *   - the target \ref block does not contain any valuable data.
- *   - all \ref pntrString elements held in \ref pntrTempAllocStack can be
+ *   - all \ref pntrString elements freed in \ref pntrTempAllocStack can be
  *     discarded without losing relevant references.
  * \post
  *   - the \ref block \p target points to is filled with a copy of
diff --git a/src/mmvstr.h b/src/mmvstr.h
index 6a1e31d2..681fe05b 100644
--- a/src/mmvstr.h
+++ b/src/mmvstr.h
@@ -259,8 +259,8 @@ typedef vstring temp_vstring;
  * directly to avoid buildup of temporary strings.
  *
  * \pre
- *   \ref g_startTempAllocStack is the index in \ref tempAllocStack from which
- *   on enties are freed.
+ *   All references freed in \ref tempAllocStack can be safely discarded
+ *   without risking a memory leak.
  * \post
  * - Entries in \ref tempAllocStack from index \ref g_startTempAllocStack on
  *   are freed.  The top of stack \ref g_tempAllocStackTop is back to
@@ -283,31 +283,28 @@ void freeTempAlloc(void);
  * again.  Every entry on and beyond \ref g_startTempAllocStack is considered
  * to be consumed and subject to deallocation.
  *
- * This deallocation procedure is embedded in this operation, since frequently
- * the final string was composed of some fragments, that now can be disposed
- * of.  In fact, this function must ALWAYS be called to assign to a vstring in
- * order for the memory cleanup routines, etc. to work properly.  A new vstring
+ * This deallocation procedure is embedded in this operation, since often the
+ * final string is composed of some fragments, that now can be disposed of.  In
+ * fact, this function must ALWAYS be called to assign to a vstring in order
+ * for the memory cleanup routines, etc. to work properly.  A new vstring
  * should be initialized to "" (the empty string), and the \ref vstring_def
  * macro handles creation of such variables.
  *
  * Possible failures: Out of memory condition.
  *
- * \param[out] target (not null) address of a \ref vstring receiving a copy of
+ * \param[in,out] target (not null) address of a \ref vstring receiving a copy of
  *   the source string.  Its current value, if not empty, must never point to a
- *   true portion of another \ref vstring.  It must not coincide with any of
- *   the temporary strings in \ref tempAllocStack, from index
- *   \ref g_startTempAllocStack on.  You can assign to an entry with index
- *   below this value, though.
+ *   true tail of another \ref vstring.  You must not assign to any of the
+ *   temporary strings in \ref tempAllocStack.
  * \param[in] source (not null) NUL terminated string to be copied from.
  *
  * \pre
  * - \ref g_startTempAllocStack contains the starting index of entries in
  *   \ref tempAllocStack, that is going to be deallocated.
- * - both parameters are not null and point to NUL terminated strings.
  * - The destination of this function must either be empty, or uniquely point
  *   to a \ref vstring, but not any of the \ref temp_vstring;
  * - The destination need not provide enough space for the source.  If
- *   necessary, it is reallocated to point to a larger chunk of memory;
+ *   necessary, it is reallocated;
  * \post
  * - Entries in \ref tempAllocStack from \ref g_startTempAllocStack (on entry
  *   to the function) are deallocated;
@@ -316,6 +313,7 @@ void freeTempAlloc(void);
  * - If the assigned value is the empty string, but the destination not, it is
  *   freed and assigned to a constant "";
  * - \ref db is updated.
+ * \bug In an out-of-memory situation the program is not exited
  */
 void let(vstring *target, const char *source);
 

From 8ba2356848b34794824007bc30aa021b13818c4f Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 14:27:54 +0100
Subject: [PATCH 31/42] fix spelling errors

---
 src/mmdata.c |  6 +++---
 src/mmdata.h | 27 +++++++++++++++++++++++----
 src/mmvstr.h |  8 ++++----
 3 files changed, 30 insertions(+), 11 deletions(-)

diff --git a/src/mmdata.c b/src/mmdata.c
index 37e791c5..506a67df 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -2489,15 +2489,15 @@ pntrString *pntrTempAllocStack[M_MAX_ALLOC_STACK];
  * allocates a \ref block capable of holding \p size \ref pntrString entries
  * and pushes it onto the \ref pntrTempAllocStack.
  * \par size == 0
- * pops off all entries from the \ref pntrTempAllocStack and adds them to the
- * \ref memFreePool.
+ * pops off all entries from index \ref g_pntrStartTempAllocStack on from
+ * \ref pntrTempAllocStack and adds them to the \ref memFreePool.
  * \param[in] size count of \ref pntrString entries.  This value must include
  *   a terminal NULL pointer if needed.
  * \return a pointer to the allocated \ref block, or NULL if deallocation
  *   requested
  * \pre
  *   \p size ==0: all entries in from \ref pntrTempAllocStack from
- *   \ref g_pntrTempAllocStackStart do not contain relevant data any more.
+ *   \ref g_pntrStartTempAllocStack do not contain relevant data any more.
  * \post
  *   - \p size > 0: memory for \p size entries is reserved in the \ref block
  *     "block's" header, but the data is still random.
diff --git a/src/mmdata.h b/src/mmdata.h
index 7ec2b500..f9c41ec6 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -45,7 +45,7 @@
 /*E*/extern long db1;
 /*!
  * \var long db2
- * Bytes held in \ref blocks managed in \ref tempAllocStack
+ * Bytes held in \ref block "blocks" managed in \ref tempAllocStack
  * "temporary pointer stacks".
  */
 /*E*/extern long db2;
@@ -526,6 +526,25 @@ extern struct nullPntrStruct g_PntrNull;
  * \post The variable is initialized.
  */
 #define pntrString_def(x) pntrString *x = NULL_PNTRSTRING
+/*!
+ * \def free_pntrString
+ * \param[in,out] x variable name
+ * Assigns \ref NULL_PNTRSTRING to a variable \ref pntrString \p x.  Frees all
+ * \ref pntrTempAllocStack, beginning with index 
+ * \ref g_pntrStartTempAllocStack.  See \ref pntrLet.
+ * \pre
+ *   - the \ref block assigned to \p x does not contain any valuable data.
+ *   - all \ref pntrString elements freed in \ref pntrTempAllocStack can be
+ *     discarded without losing relevant references.
+ * \post
+ *   - \p x is assigned NULL_PNTRSTRING.
+ *   - The stack pointer of \ref pntrTempAllocStack is reset to
+ *     \ref g_pntrStartTempAllocStack and all referenced
+ *     \ref block "blocks" on and beyond that are returned to the
+ *     \ref memFreePool.
+ *   - updates \ref db3 and \ref poolTotalFree.
+ *   - Exit on out-of-memory
+ */
 #define free_pntrString(x) pntrLet(&x, NULL_PNTRSTRING)
 
 
@@ -692,7 +711,7 @@ long compressedProofSize(const nmbrString *proof, long statemNum);
  */
 extern long g_pntrTempAllocStackTop;   /* Top of stack for pntrTempAlloc function */
 /*!
- * \var long g_pntrTempAllocStackStart
+ * \var long g_pntrStartTempAllocStack
  *
  * Index of the first entry of the \ref stack "stack" \ref pntrTempAllocStack
  * eligible for deallocation on the next call to \ref pntrTempAlloc.  Entries
@@ -732,7 +751,7 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
  * \n
  * It is assumed that the value persisted in \p target is in fact computed from
  * temporary operands in \ref pntrTempAllocStack.  All blocks starting with
- * the element at \ref g_pntrTempAllocStackStart are returned to the
+ * the element at \ref g_pntrStartTempAllocStack are returned to the
  * \ref memFreePool.
  * \attention freed \ref block "blocks" contain \ref pntrString instances.
  *   See \ref pntrTempAllocStack to learn how this free process can be
@@ -754,7 +773,7 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
  *   - due to a possible reallocation the pointer \p target points to may
  *     change.
  *   - The stack pointer of \ref pntrTempAllocStack is reset to
- *     \ref g_pntrTempAllocStackStart and all referenced
+ *     \ref g_pntrStartTempAllocStack and all referenced
  *     \ref block "blocks" on and beyond that are returned to the
  *     \ref memFreePool.
  *   - updates \ref db3 and \ref poolTotalFree.
diff --git a/src/mmvstr.h b/src/mmvstr.h
index 681fe05b..bfb95780 100644
--- a/src/mmvstr.h
+++ b/src/mmvstr.h
@@ -301,16 +301,16 @@ void freeTempAlloc(void);
  * \pre
  * - \ref g_startTempAllocStack contains the starting index of entries in
  *   \ref tempAllocStack, that is going to be deallocated.
- * - The destination of this function must either be empty, or uniquely point
- *   to a \ref vstring, but not any of the \ref temp_vstring;
- * - The destination need not provide enough space for the source.  If
+ * - The \p target of this function must either be empty, or uniquely point
+ *   to a \ref vstring, but not to any of the \ref temp_vstring;
+ * - The \p target need not provide enough space for the source.  If
  *   necessary, it is reallocated;
  * \post
  * - Entries in \ref tempAllocStack from \ref g_startTempAllocStack (on entry
  *   to the function) are deallocated;
  * - The stack pointer in \ref g_tempAllocStackTop is set to
  *   \ref g_startTempAllocStack (on entry to the function);
- * - If the assigned value is the empty string, but the destination not, it is
+ * - If the assigned value is the empty string, but the \p target not, it is
  *   freed and assigned to a constant "";
  * - \ref db is updated.
  * \bug In an out-of-memory situation the program is not exited

From 733456f35728f1ff6696a912aad3ad1b9075feab Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 15:18:30 +0100
Subject: [PATCH 32/42] doc pntrAddElement

---
 src/mmdata.h | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/src/mmdata.h b/src/mmdata.h
index f9c41ec6..7b096e68 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -849,6 +849,23 @@ long pntrRevInstr(long start_position, const pntrString *string1,
 flag pntrEq(const pntrString *sout, const pntrString *sin);
 
 /* Add a single null string element to a pntrString - faster than pntrCat */
+/*!
+ * \fn temp_pntrString *pntrAddElement(const pntrString *g)
+ * \param[in] g points to the first element of a NULL terminated array in a
+ *   \ref block.
+ * \return a copy of \p g, the terminal NULL replaced with a \ref vstring ""
+ *   followed by NULL.
+ * \attention   
+ *   - the pointers in \p g are copied to the result.  If some of them
+ *     reference allocated memory, check for possible double free, for example.
+ *   - a pointer to constant data is padded to the right.  The refernced memory
+ *     must not be overwritten.
+ * \post 
+ *   - the elements of \p g are duplicated.
+ *   - a pointer to a NUL byte ("") constant is padded to the right.  Make sure
+ *     the referenced memory is never overwritten.
+ * \bug a pointer to constant data is added as a writeable void*.
+ */
 temp_pntrString *pntrAddElement(const pntrString *g);
 
 /* Add a single null pntrString element to a pntrString - faster than pntrCat */

From 7f6602207d02059ba141b2dfa610e7398cacb2f2 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 18:33:58 +0100
Subject: [PATCH 33/42] doc submit mode in cmdInput1

---
 src/mmdata.h |  2 +-
 src/mminou.h | 35 +++++++++++++++++++++++++++++++----
 2 files changed, 32 insertions(+), 5 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 7b096e68..39f9eac5 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -858,7 +858,7 @@ flag pntrEq(const pntrString *sout, const pntrString *sin);
  * \attention   
  *   - the pointers in \p g are copied to the result.  If some of them
  *     reference allocated memory, check for possible double free, for example.
- *   - a pointer to constant data is padded to the right.  The refernced memory
+ *   - a pointer to constant data is padded to the right.  The referenced memory
  *     must not be overwritten.
  * \post 
  *   - the elements of \p g are duplicated.
diff --git a/src/mminou.h b/src/mminou.h
index d24bbed5..a06f2583 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -65,6 +65,12 @@ extern long g_commandFileNestingLevel;
  * valid, and point to opened files.
  */
 extern FILE *g_commandFilePtr[MAX_COMMAND_FILE_NESTING + 1];
+/*!
+ * \var vstring g_commandFileName[]
+ * list of command file names in nested SUBMIT commands.  This name need not be
+ * fully qualified (with all directories down from the root directory).  The
+ * first element is reserved for stdin and never set.
+ */
 extern vstring g_commandFileName[MAX_COMMAND_FILE_NESTING + 1];
 extern flag g_commandFileSilent[MAX_COMMAND_FILE_NESTING + 1];
 /*!
@@ -210,9 +216,9 @@ vstring cmdInput(FILE *stream, const char *ask);
  * After some explanatory text is printed, gets a line from either stdin or the
  * command file stream in \ref g_commandFilePt, depending on the value of
  * \ref g_commandFileNestingLevel.  If this value is 0, interactive input via
- * stdin is assumed, else non interpreted lines are read from a file.  The line returned
- * to the caller is more or less what \ref cmdInput() yields, but some fine
- * tuning is applied.
+ * stdin is assumed, else non interpreted lines are read from a file in submit
+ * mode.  The line returned to the caller is more or less what \ref cmdInput()
+ * yields, but some fine tuning is applied.
  *
  * \par Displaying the prompt text
  *
@@ -239,6 +245,19 @@ vstring cmdInput(FILE *stream, const char *ask);
  * immediate stop on the caller's side.
  *
  * 4. If logging is enabled, prompt and returned input is logged.
+ * 
+ * \par Submit Mode
+ *
+ * 1. a non-interpreted line is read from the appropriate entry in
+ * \ref g_commandFilePtr by \ref cmdInput.
+ *
+ * 2. If NULL is returned, reaching EOF is assumed, the file is closed, its
+ * name in \ref g_commandFileName deallocated and the previous
+ * \ref g_commandFileLevel is activated.  In this particular case the read line
+ * is the empty string.  A message indicating the end of the command file is
+ * printed.  The \ref g_commandFileSilentFlag controlling console output is
+ * copied from the appropriate entry of \ref g_commandFileSilent, unless the
+ * interactive mode is reached; here output is never suppressed (value 0).
  *
  * \return first not interpreted line as \ref vstring, or "EXIT" on error. 
  * \pre
@@ -261,7 +280,15 @@ vstring cmdInput(FILE *stream, const char *ask);
  *   - \ref g_logFileOpenFlag if set to 1, a not interpreted returned line is
  *     logged before it is passed on to the caller.
  * \post
- *   \ref localScrollMode is set to 1
+ *   - \ref localScrollMode is set to 1
+ *   - \ref printedLines is reset to 0
+ *   - \ref g_quitPrint is reset to 0
+ *   - interactive mode: \ref tempAllocStack frees top elements down to
+ *     \ref g_startTempAlloc.
+ *   - interactive mode: \ref pntrTempAllocStack frees top elements down to
+ *     \ref g_pntrStartTempAlloc.
+ *   - interactive mode: The \ref backBuffer is cleared, then filled with
+ *     prompt (last line only) and input of the user.
  * \warning the calling program must deallocate the returned string.
  */
 vstring cmdInput1(const char *ask);

From 251d2b5a27e004fc4068442deb9cf2ea08f53456 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 18:59:09 +0100
Subject: [PATCH 34/42] finished doc of cmdInput1

---
 src/mminou.h |  8 ++++++++
 src/mmvstr.h | 25 +++++++++++++++++++++++++
 2 files changed, 33 insertions(+)

diff --git a/src/mminou.h b/src/mminou.h
index a06f2583..877b5108 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -259,6 +259,11 @@ vstring cmdInput(FILE *stream, const char *ask);
  * copied from the appropriate entry of \ref g_commandFileSilent, unless the
  * interactive mode is reached; here output is never suppressed (value 0).
  *
+ * 3. remove all CR (0x0D) characters, not only those in compination with LF.
+ *
+ * 4. prompt and command is printed, if not suppressed, then the read line is
+ * returned.
+ *
  * \return first not interpreted line as \ref vstring, or "EXIT" on error. 
  * \pre
  *   The following variables are honored during execution and should be properly
@@ -289,6 +294,9 @@ vstring cmdInput(FILE *stream, const char *ask);
  *     \ref g_pntrStartTempAlloc.
  *   - interactive mode: The \ref backBuffer is cleared, then filled with
  *     prompt (last line only) and input of the user.
+ *   - submit mode: In case of EOF the previous \ref g_commandFileNestingLevel
+ *     is activated, necessary cleanups performed, and 
+ *     the \ref g_commandFileSilentFlag is updated appropriately.
  * \warning the calling program must deallocate the returned string.
  */
 vstring cmdInput1(const char *ask);
diff --git a/src/mmvstr.h b/src/mmvstr.h
index bfb95780..f334b78c 100644
--- a/src/mmvstr.h
+++ b/src/mmvstr.h
@@ -454,6 +454,31 @@ temp_vstring left(const char *sin, long n);
  * \bug a stack overflow of \a tempAllocStack is not handled correctly.
  */
 temp_vstring right(const char *sin, long n);
+/*!
+ * \fn temp_vstring edit(const char *sin, long control)
+ * perform a combination of transformations on \p sin based on the set bits in
+ * \p control.
+ *      Bit   Effect
+ *      1        Clear parity bits
+ *      2        Discard all spaces and tabs
+ *      4        Discard characters: CR, LF, FF, ESC, RUBOUT, and NULL
+ *      8        Discard leading spaces and tabs
+ *      16       Reduce spaces and tabs to one space
+ *      32       Convert lowercase to uppercase
+ *      64       Convert [ to ( and ] to )
+ *      128      Discard trailing spaces and tabs
+ *      256      Do not alter characters inside quotes
+ *      512      Convert uppercase to lowercase
+ *      1024     Tab the line (convert spaces to equivalent tabs)
+ *      2048     Untab the line (convert tabs to equivalent spaces)
+ *      4096     Convert VT220 screen print frame graphics to -,|,+ characters
+ *      8192     Discard CR only (to assist DOS-to-Unix conversion)
+ *      16384    Discard trailing spaces, tabs, and LFs
+ * \param[in] sin (not null) NUL terminated string to convert
+ * \param[in] control a combination of set bit requesting the desired
+ *   transformation(s)
+ * \return the transformed \p sin ready for pushing on \ref tempAllocStack.
+ */
 temp_vstring edit(const char *sin, long control);
 /*!
  * \fn temp_vstring space(long n)

From 677d6a7aa77d626c69b9f1aa40984a11cb3e5260 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sun, 6 Mar 2022 19:03:47 +0100
Subject: [PATCH 35/42] the final edits were not saved, so here they are

---
 src/mminou.c | 6 ++++++
 src/mmvstr.h | 2 +-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/mminou.c b/src/mminou.c
index fa75a3e3..97ad1dc6 100644
--- a/src/mminou.c
+++ b/src/mminou.c
@@ -46,6 +46,12 @@ vstring_def(g_printString);
 long g_commandFileNestingLevel = 0;
 FILE *g_commandFilePtr[MAX_COMMAND_FILE_NESTING + 1];
 vstring g_commandFileName[MAX_COMMAND_FILE_NESTING + 1];
+/*!
+ * \var flag g_commandFileSilent[]
+ * a 1 for a particular \ref g_commandFileNestingLevel suppresses output for
+ * that submit nesting level.  The value for the interactive level
+ * (\ref g_commandFileNestingLevel == 0) is ignored.
+ */
 flag g_commandFileSilent[MAX_COMMAND_FILE_NESTING + 1];
 flag g_commandFileSilentFlag = 0; /* For SUBMIT ... /SILENT */
 
diff --git a/src/mmvstr.h b/src/mmvstr.h
index f334b78c..e3c307a0 100644
--- a/src/mmvstr.h
+++ b/src/mmvstr.h
@@ -457,7 +457,7 @@ temp_vstring right(const char *sin, long n);
 /*!
  * \fn temp_vstring edit(const char *sin, long control)
  * perform a combination of transformations on \p sin based on the set bits in
- * \p control.
+ * \p control.  This is an ASCII based transformation.
  *      Bit   Effect
  *      1        Clear parity bits
  *      2        Discard all spaces and tabs

From d4d1faabec84c8e27bd71ae3fa3ad328e5318019 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Mon, 7 Mar 2022 07:11:06 +0100
Subject: [PATCH 36/42] fix review issues

---
 src/mmdata.c | 44 ++++++++++++++++++++++++++------------------
 src/mmdata.h |  3 +--
 src/mminou.h | 14 +++-----------
 src/mmvstr.h | 33 +++++++++++++++++----------------
 4 files changed, 47 insertions(+), 47 deletions(-)

diff --git a/src/mmdata.c b/src/mmdata.c
index 506a67df..9b8b34a4 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -180,19 +180,17 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
  * similar, all pushed onto this stack.  When the final operation is executed,
  * and its result is persisted in some variable, the dependency on its
  * temporary operands ceases.  Consequently, they should be freed again.  To
- * automate this operation,  such a stack maintains a __start__ index.  A
- * client saves this value and sets it to the current stack top, then starts
- * pushing dynamically allocated operands on the stack.  After the result is
- * persisted, all entries beginning with the element at index  __start__ are
- * deallocated again, and the stack top is reset to the __start__ value, while
- * the __start__ value is reset to the saved value, to accomodate nesting of
- * this procedure.
+ * automate this operation,  such a stack maintains a `start` index.  A client
+ * saves this value and sets it to the current stack top, then starts pushing
+ * dynamically allocated operands on the stack.  After the result is persisted,
+ * all entries beginning with the element at index  `start` are deallocated
+ * again, and the stack top is reset to the `start` value, while the `start`
+ * value is reset to the saved value, to accommodate nesting of this procedure.
  *
  * This scheme needs a few conditions to be met:
  * - No operand is used in more than one evaluation context;
  * - Operations are executed strictly sequential, or in a nested manner. No two
  *   operations interleave pushing operands.
- *   push operands interleaved
  */
 
 /* Memory pools are used to reduce the number of malloc and alloc calls that
@@ -213,16 +211,27 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
    The pointer to an array always points to element 0 (recast to right size).
 */
 
+/*!
+ * \page doc-todo Improvements in documentation
+ * 
+ * - Revisit the \ref block "block", \ref stack "stack" references to check the
+ *   inserted wording.
+ * - Check what the advantages of __p__ tag are and whether the are better
+ *   replaced with backtick pairs. (\p aParam vs `aParam`)
+ * - Regularly check the warning in \ref pntrString to see whether it still
+ *   holds, or can be made more precise.
+ */
+
 /*!
  * \def MEM_POOL_GROW
  * Amount that \ref memUsedPool and \ref memFreePool grows when it overflows.
  */
-#define MEM_POOL_GROW 1000 /* Amount that a pool grows when it overflows. */
+#define MEM_POOL_GROW 1000
 /*??? Let user set this from menu. */
 /*!
  * \var long poolAbsoluteMax
  * The value is a memory amount in bytes.
- * \n
+ *
  * The \ref suballocator scheme must not hold more memory than is short term
  * useful.  To the operating system all memory in \ref memFreePool appears as
  * allocated, although it is not really in use.  To prevent the system from
@@ -590,14 +599,13 @@ void addToUsedPool(void *ptr)
  * Starting with the last entry in \ref memFreePool, memory held in that pool
  * is returned to the system until all, or at least a sufficient amount is
  * freed again (see \p untilOK).
- * \param[in] untilOK if 1 freeing \ref block "blocks" stops the moment
- *   \ref poolTotalFree gets within the range of \ref poolAbsoluteMax again.
- *   Note that it is not guaranteed that the limit \ref poolAbsoluteMax is
- *   undercut because still too much free memory might be held in the
- *   \ref memUsedPool.
- *   \n
- *   If 0, all \ref memFreePool entries are freed, and the pool itself is
- *   shrunk back to \ref MEM_POOL_GROW size.
+ * \param[in] untilOK
+ *   - if 1 freeing \ref block "blocks" stops the moment \ref poolTotalFree
+ *     gets within the range of \ref poolAbsoluteMax again.  Note that it is
+ *     not guaranteed that the limit \ref poolAbsoluteMax is undercut because
+ *     still too much free memory might be held in the \ref memUsedPool.
+ *   - If 0, all \ref memFreePool entries are freed, and the pool itself is
+ *     shrunk back to \ref MEM_POOL_GROW size.
  */
 void memFreePoolPurge(flag untilOK)
 {
diff --git a/src/mmdata.h b/src/mmdata.h
index 39f9eac5..819292b2 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -166,7 +166,7 @@ typedef nmbrString temp_nmbrString;
  * \brief a single \ref pntrString element for use in a \ref stack "stack".
  *
  * These elements are pushed onto and popped off a \ref stack 
- * "stack of temporary data".  All pointer of this type should ONLY refer to
+ * "stack of temporary data".  Pointers of this type should ONLY refer to
  * dynamically allocated memory on the heap.  Special commands support
  * dependency tracking and free all pointers on and after a particular one in
  * such a stack. 
@@ -864,7 +864,6 @@ flag pntrEq(const pntrString *sout, const pntrString *sin);
  *   - the elements of \p g are duplicated.
  *   - a pointer to a NUL byte ("") constant is padded to the right.  Make sure
  *     the referenced memory is never overwritten.
- * \bug a pointer to constant data is added as a writeable void*.
  */
 temp_pntrString *pntrAddElement(const pntrString *g);
 
diff --git a/src/mminou.h b/src/mminou.h
index 877b5108..a8d75da1 100644
--- a/src/mminou.h
+++ b/src/mminou.h
@@ -154,17 +154,9 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
  * 
  * No timeout is applied while waiting for user input from the console.
  *
- * Detected format errors result in following bug messages:
- *   - 1507: The first read character is NUL
- *   - 1508: line overflow, the last character is not NUL
- *   - 1519: padding of LF failed, or first read character was NUL
- *   - 1521: a NUL in first and second position was read
- *   - 1523: NULL instead of a prompt text when user input is required
- *   - 1525: missing terminating LF, not caused by an EOF.
- *
- *   A bug message need not result in an execution stop.  It is not directed to
- *   the metamath bug function to avoid stacking up calls (bug calling cmdInput
- *   again for scrolling etc.).
+ * A bug message need not result in an execution stop.  It is not directed to
+ * the metamath bug function to avoid stacking up calls (bug calling cmdInput
+ * again for scrolling etc.).
  *
  * \todo clarify recursive call to print2 and the role of backFromCmdInput. 
  * \param[in] stream (not null) source to read the line from.  _stdin_ is
diff --git a/src/mmvstr.h b/src/mmvstr.h
index e3c307a0..4b248be9 100644
--- a/src/mmvstr.h
+++ b/src/mmvstr.h
@@ -458,22 +458,23 @@ temp_vstring right(const char *sin, long n);
  * \fn temp_vstring edit(const char *sin, long control)
  * perform a combination of transformations on \p sin based on the set bits in
  * \p control.  This is an ASCII based transformation.
- *      Bit   Effect
- *      1        Clear parity bits
- *      2        Discard all spaces and tabs
- *      4        Discard characters: CR, LF, FF, ESC, RUBOUT, and NULL
- *      8        Discard leading spaces and tabs
- *      16       Reduce spaces and tabs to one space
- *      32       Convert lowercase to uppercase
- *      64       Convert [ to ( and ] to )
- *      128      Discard trailing spaces and tabs
- *      256      Do not alter characters inside quotes
- *      512      Convert uppercase to lowercase
- *      1024     Tab the line (convert spaces to equivalent tabs)
- *      2048     Untab the line (convert tabs to equivalent spaces)
- *      4096     Convert VT220 screen print frame graphics to -,|,+ characters
- *      8192     Discard CR only (to assist DOS-to-Unix conversion)
- *      16384    Discard trailing spaces, tabs, and LFs
+ *      Bit    |  Effect
+ *      -----  |  ------
+ *      1      |  Clear parity bits
+ *      2      |  Discard all spaces and tabs
+ *      4      |  Discard characters: CR, LF, FF, ESC, RUBOUT, and NULL
+ *      8      |  Discard leading spaces and tabs
+ *      16     |  Reduce spaces and tabs to one space
+ *      32     |  Convert lowercase to uppercase
+ *      64     |  Convert [ to ( and ] to )
+ *      128    |  Discard trailing spaces and tabs
+ *      256    |  Do not alter characters inside quotes
+ *      512    |  Convert uppercase to lowercase
+ *      1024   |  Tab the line (convert spaces to equivalent tabs)
+ *      2048   |  Untab the line (convert tabs to equivalent spaces)
+ *      4096   |  Convert VT220 screen print frame graphics to -,|,+ characters
+ *      8192   |  Discard CR only (to assist DOS-to-Unix conversion)
+ *      16384  |  Discard trailing spaces, tabs, and LFs
  * \param[in] sin (not null) NUL terminated string to convert
  * \param[in] control a combination of set bit requesting the desired
  *   transformation(s)

From 3021161f45f1154f67bc7d51f1730a0045649e5e Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Mon, 7 Mar 2022 09:30:28 +0100
Subject: [PATCH 37/42] rm a LF

---
 src/mmdata.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 819292b2..ab011ce8 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -123,7 +123,7 @@ typedef long nmbrString; /* String of numbers */
  * tail of an array from a certain element on, an array terminates with a
  * null pointer.  This type of usage forbids null pointer as ordinary elements,
  * and the terminal null pointer is not part of the data in the array.
- * \n
+ *
  * The length of a pntrString array is implicitely given by a terminal NULL
  * pointer.  If this array is held in a \ref block, its size can also be
  * determined from its header's administrative data.  Both values must be kept

From c9b3a49ec295a13cefc04bc1b77060ba393ffe83 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Mon, 7 Mar 2022 12:27:17 +0100
Subject: [PATCH 38/42] add pre to pntrAddElement

---
 src/mmdata.c |  6 ++++--
 src/mmdata.h | 14 ++++++--------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/mmdata.c b/src/mmdata.c
index 9b8b34a4..7f71779b 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -216,8 +216,10 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
  * 
  * - Revisit the \ref block "block", \ref stack "stack" references to check the
  *   inserted wording.
- * - Check what the advantages of __p__ tag are and whether the are better
- *   replaced with backtick pairs. (\p aParam vs `aParam`)
+ * - The formatting of __p__ tags seem insufficient.  Figure out whether and
+ *   how doxygen allows assigning formats to a semantic tag.  Do not replace
+ *   a tag with direct formattings like \p aParam vs `aParam`, as some editors
+ *   recognize and highlight semantic tags.
  * - Regularly check the warning in \ref pntrString to see whether it still
  *   holds, or can be made more precise.
  */
diff --git a/src/mmdata.h b/src/mmdata.h
index ab011ce8..6eca82bc 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -852,18 +852,16 @@ flag pntrEq(const pntrString *sout, const pntrString *sin);
 /*!
  * \fn temp_pntrString *pntrAddElement(const pntrString *g)
  * \param[in] g points to the first element of a NULL terminated array in a
- *   \ref block.
+ *   \ref block.  It is assumed it is an array of pointer to \ref vstring.
  * \return a copy of \p g, the terminal NULL replaced with a \ref vstring ""
  *   followed by NULL.
  * \attention   
- *   - the pointers in \p g are copied to the result.  If some of them
- *     reference allocated memory, check for possible double free, for example.
- *   - a pointer to constant data is padded to the right.  The referenced memory
- *     must not be overwritten.
+ *   the pointers in \p g are copied to the result.  If some of them
+ *   reference allocated memory, check for possible double free, for example.
+ * \pre
+ *   Intended to be used with arrays of \ref vstring * only.
  * \post 
- *   - the elements of \p g are duplicated.
- *   - a pointer to a NUL byte ("") constant is padded to the right.  Make sure
- *     the referenced memory is never overwritten.
+ *   the elements of \p g are duplicated.
  */
 temp_pntrString *pntrAddElement(const pntrString *g);
 

From 91b9cd61b6c1e1391948baebd5b89d274d1fe217 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Mon, 7 Mar 2022 13:58:12 +0100
Subject: [PATCH 39/42] rm more unnecessary LF

---
 src/mmdata.h | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 6eca82bc..339fb275 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -363,13 +363,13 @@ void poolFree(void *ptr);
  *
  * This function temporarily freezes the usage of a block for the current user,
  * and allows temporary reallocation of the free capacity to a new client.
- * \n
+ *
  * The program maintains pools of memory blocks with free capacity.  In case of
  * demand such a \ref block can temporarily allocate this capacity for new
  * usage.  Of course two (or more) clients share different parts of the same
  * \ref block then, so a newer client must complete its usage before the old
  * one resumes operation and may want to extend its usage of the \ref block.
- * \n
+ *
  * Before \p ptr is added to \ref memUsedPool, the pool size is checked and
  * increased by \ref MEM_POOL_GROW if full.  This may lead to out-of-memory
  * \ref outOfMemory "exit".  But if \p ptr is added to the end of the \ref memUsedPool,
@@ -719,7 +719,7 @@ extern long g_pntrTempAllocStackTop;   /* Top of stack for pntrTempAlloc functio
  * but entries above are.  So when this entry gets deallocated, dependent ones
  * should follow suit.  A function like \ref pntrTempAlloc or \ref pntrLet
  * manage this automatic deallocation.
- * \n
+ *
  * Nested functions using the \ref pntrTempAllocStack usually save the current
  * value and set it to \ref g_pntrTempAllocStackTop, so they can create their
  * local dependency chain.  On return the saved value is restored.
@@ -748,7 +748,7 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
  * future growing.  If the \p target block is only partially used after copy it
  * is added to the \ref memUsedPool.  If \p source is empty, the \p target is
  * set to \ref NULL_PNTRSTRING.
- * \n
+ *
  * It is assumed that the value persisted in \p target is in fact computed from
  * temporary operands in \ref pntrTempAllocStack.  All blocks starting with
  * the element at \ref g_pntrStartTempAllocStack are returned to the

From ff2ba42e95c13562d429dab7cda447538ab8d6c8 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Mon, 7 Mar 2022 20:38:35 +0100
Subject: [PATCH 40/42] fix dangling conflict marker

---
 src/mmdata.h | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/mmdata.h b/src/mmdata.h
index 28e12b7e..7479e6a9 100644
--- a/src/mmdata.h
+++ b/src/mmdata.h
@@ -171,11 +171,6 @@ typedef nmbrString temp_nmbrString;
  * dynamically allocated memory on the heap.  Special commands support
  * dependency tracking and free all pointers on and after a particular one in
  * such a stack. 
-=======
- * These elements are pushed onto and popped off a \ref stack
- * "stack of temporary data".  Special commands can free all pointers on and
- * after a particular one in such a stack.
->>>>>>> upstream/master
  */
 typedef pntrString temp_pntrString;
 

From e9d586b403094cd56bbee1330a39b85ee7aa4597 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Mon, 7 Mar 2022 20:41:28 +0100
Subject: [PATCH 41/42] fix indentation

---
 src/mmvstr.h | 31 +++++++++++++++----------------
 1 file changed, 15 insertions(+), 16 deletions(-)

diff --git a/src/mmvstr.h b/src/mmvstr.h
index cef1fbdb..5fd25622 100644
--- a/src/mmvstr.h
+++ b/src/mmvstr.h
@@ -167,24 +167,24 @@ typedef char* vstring;
  * A `temp_vstring` should never be used as the first argument of a `let`.
  * This code is INCORRECT:
  *
- *   temp_vstring foo = left("foobar", 3);
- *   let(&foo, "bar"); // this will cause a double free
+ *     temp_vstring foo = left("foobar", 3);
+ *     let(&foo, "bar"); // this will cause a double free
  *
  * It is okay (and quite common) to use a temp_vstring as the second argument,
  * however. It is best not to hold on to the value, though, because the `let`
  * will free it. This code is INCORRECT:
  *
- *   vstring_def(x);
- *   temp_vstring foobar = cat("foo", "bar");
- *   let(&x, foobar); // frees foobar
- *   let(&x, foobar); // dangling reference
+ *     vstring_def(x);
+ *     temp_vstring foobar = cat("foo", "bar");
+ *     let(&x, foobar); // frees foobar
+ *     let(&x, foobar); // dangling reference
  *
  * There is a converse problem when `temp_vstring`s are used without `let`:
  *
- *   for (int i = 0; i < 100000; i++) {
- *     vstring_def(x);
- *     if (strlen(space(i)) == 99999) break;
- *   }
+ *     for (int i = 0; i < 100000; i++) {
+ *       vstring_def(x);
+ *       if (strlen(space(i)) == 99999) break;
+ *     }
  *
  * We don't need to deallocate the string returned by `space()` directly,
  * because it returns a `temp_vstring`, but because there is no `let` in
@@ -194,12 +194,11 @@ typedef char* vstring;
  * we can either use a dummy `let()` statement in the loop, or call
  * `freeTempAlloc` directly:
  *
- *   for (int i = 0; i < 100000; i++) {
- *     vstring_def(x);
- *     if (strlen(space(i)) == 99999) break;
- *     freeTempAlloc();
- *   }
- *
+ *     for (int i = 0; i < 100000; i++) {
+ *       vstring_def(x);
+ *       if (strlen(space(i)) == 99999) break;
+ *       freeTempAlloc();
+ *     }
  */
 typedef vstring temp_vstring;
 

From da19baf0e93555a40dedb3e3edf760d74ef01437 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Tue, 8 Mar 2022 07:08:55 +0100
Subject: [PATCH 42/42] css for customizing p tags

---
 src/mmdata.c | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/mmdata.c b/src/mmdata.c
index 8effce13..02487ae0 100644
--- a/src/mmdata.c
+++ b/src/mmdata.c
@@ -220,6 +220,9 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
  *   how doxygen allows assigning formats to a semantic tag.  Do not replace
  *   a tag with direct formattings like \p aParam vs `aParam`, as some editors
  *   recognize and highlight semantic tags.
+ *     The parameters are included in <code>aParam</code> tags.  You can change
+ *     the appearance by using your customized CSS file and let doxygen use it
+ *     with HTML-EXTRA-STYLESHEET in your own Doxyfile.
  * - Regularly check the warning in \ref pntrString to see whether it still
  *   holds, or can be made more precise.
  */