Skip to content

Commit e49422b

Browse files
authored
Doxy (#74)
* corrections, tweaks, explaining mid * fix a mistake * fix invariants of tempAllocStack * fix invariants of tempAllocStack * function left * fix broken text in let * describe right * document space and others * describe cat * doc free_string * doc free_string, part 2 * doc cmdInput * corrections * doc chr * fix missing entries in doxygen * doc scollMode * add attention tags to point to 1-based semantics * document seg, mar params as in out * explain bounds in seg * be more precise about the limitations of seg * fix preconditions * C standard limits parameter of mid * provide doxygen friendly macro expansions * improve description of backBuffer * parse function like macros * better structure of Doxyfile.diff * rm _DOXYGEN_ code block - not needed anymore * explain scroll flags * improve description of scroll back * doc g_commandPrompt * describe a bug in cmdInput * improve doc of cmdInput * add warnings if not UTF-8 compatible * complete description of cmdInput * forgot to mention g_outputToString * fix format error * fix another format error * fix incorrect description * improve post condition * rewrite post Co-authored-by: Wolf Lammen <[email protected]>
1 parent d02a72a commit e49422b

File tree

7 files changed

+398
-41
lines changed

7 files changed

+398
-41
lines changed

Doxyfile.diff

Lines changed: 28 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,35 @@ PROJECT_BRIEF = "executable used to maintain *.mm files"
3333

3434
PROJECT_LOGO = "Metamath.png"
3535

36-
# disable Graphviz .dot output
36+
#---------------------------------------------------------------------------
37+
# Output extent related overrides
38+
#---------------------------------------------------------------------------
3739

40+
# If you set the HAVE_DOT tag to YES then doxygen will assume the dot tool is
41+
# available from the path. This tool is part of Graphviz (see:
42+
# http://www.graphviz.org/), a graph visualization toolkit from AT&T and Lucent
43+
# Bell Labs. The other options in this section have no effect if this option is
44+
# set to NO
45+
# The default value is: YES.
3846
HAVE_DOT = NO
3947

4048
GENERATE_LATEX = NO
49+
50+
#---------------------------------------------------------------------------
51+
# Parsing C contents related overrides
52+
#---------------------------------------------------------------------------
53+
54+
# If the EXTRACT_STATIC tag is set to YES, all static members of a file will be
55+
# included in the documentation.
56+
# The default value is: NO.
57+
EXTRACT_STATIC = YES
58+
59+
# cope with function like macros (pntrString_def and similar).
60+
# If the MACRO_EXPANSION tag is set to YES, doxygen will expand all macro names
61+
# in the source code. If set to NO, only conditional compilation will be
62+
# performed. Macro expansion can be done in a controlled way by setting
63+
# EXPAND_ONLY_PREDEF to YES.
64+
# The default value is: NO.
65+
# This tag requires that the tag ENABLE_PREPROCESSING is set to YES.
66+
67+
MACRO_EXPANSION = YES

src/mmcmdl.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,11 @@ extern nmbrString *g_rawArgNmbr;
2828
extern long g_rawArgs;
2929
extern pntrString *g_fullArg;
3030
extern vstring g_fullArgString; /* g_fullArg as one string */
31+
/*!
32+
* \var vstring g_commandPrompt
33+
* text displayed at the beginning of the line where a user is supposed to
34+
* enter a new command. For example 'MM>'.
35+
*/
3136
extern vstring g_commandPrompt;
3237
extern vstring g_commandLine;
3338
extern long g_showStatement;

src/mmdata.h

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -342,7 +342,7 @@ long getFreeSpace(long max);
342342
* before exiting the program raising an error condition.
343343
*
344344
* \param msg error message displayed to the user.
345-
* \returns never, but exits the program instead.
345+
* \return never, but exits the program instead.
346346
* \bug calls functions like print2, that in turn may call outOfMemory again
347347
* under restricted memory conditions, so finally memory error messages are
348348
* stacked up endlessly.
@@ -590,7 +590,7 @@ long compressedProofSize(const nmbrString *proof, long statemNum);
590590
memory allocation (use with caution) *******/
591591

592592
/*!
593-
* \var g_pntrTempAllocStackTop
593+
* \var long g_pntrTempAllocStackTop
594594
*
595595
* Index of the current top af the \ref stack "stack" \a pntrTempAlloc.
596596
* New data is pushed from this location on if space available.
@@ -636,7 +636,7 @@ temp_pntrString *pntrNSpace(long n);
636636
temp_pntrString *pntrPSpace(long n);
637637

638638
/*!
639-
* \fn pntrLen
639+
* \fn long pntrLen(const pntrString *s)
640640
* \brief Determine the length of a pntrString held in a \ref block "block"
641641
* dedicated to it.
642642
*
@@ -650,7 +650,7 @@ temp_pntrString *pntrPSpace(long n);
650650
*/
651651
long pntrLen(const pntrString *s);
652652
/*!
653-
* \fn pntrAllocLen
653+
* \fn long pntrAllocLen(const pntrString *s)
654654
* \brief Determine the capacity of a pntrString embedded in a dedicated block
655655
*
656656
* returns the capacity of pointers in the array pointed to by \p s,

src/mminou.c

Lines changed: 23 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,14 +57,29 @@ long g_screenWidth = MAX_LEN; /* Width default = 79 */
5757
/* g_screenHeight is one less than the physical screen to account for the
5858
prompt line after pausing. */
5959
long g_screenHeight = SCREEN_HEIGHT; /* Default = 23 */
60+
/*!
61+
* \var int printedLines
62+
* Lines printed since last user input (mod screen height)
63+
*/
6064
int printedLines = 0; /* Lines printed since last user input (mod screen height) */
6165
flag g_scrollMode = 1; /* Flag for continuous (0) or prompted (1) scroll */
6266
flag g_quitPrint = 0; /* Flag that user quit the output */
67+
/*!
68+
* \var flag localScrollMode
69+
*
70+
* temporarily disables prompted scroll (see \a g_scrollMode) until next user
71+
* prompt
72+
*/
6373
flag localScrollMode = 1; /* 0 = Scroll continuously only till next prompt */
6474

6575
/* Buffer for B (back) command at end-of-page prompt - for future use */
66-
/*! \var backBuffer
76+
/*! \var pntrString* backBuffer
6777
* Buffer for B (back) command at end-of-page prompt.
78+
*
79+
* Some longer text (like help texts for example) provide a page wise display
80+
* with a scroll option, so the user can move freely back and forth in the
81+
* text. This is the storage of already displayed text kept for possible
82+
* redisplay.
6883
*/
6984
pntrString_def(backBuffer);
7085
/*!
@@ -620,6 +635,12 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea
620635
return;
621636
} /* printLongLine */
622637

638+
/*!
639+
* \def CMD_BUFFER_SIZE
640+
* Number of bytes allocated for prompted text, including the terminating NUL,
641+
* but excluding the return key stroke the user finishes her/his input with.
642+
*/
643+
#define CMD_BUFFER_SIZE 2000
623644

624645
vstring cmdInput(FILE *stream, const char *ask) {
625646
/* This function prints a prompt (if 'ask' is not NULL) and gets a line from
@@ -628,9 +649,9 @@ vstring cmdInput(FILE *stream, const char *ask) {
628649
be freed by the caller. */
629650
vstring_def(g); /* Always init vstrings to "" for let(&...) to work */
630651
long i;
631-
#define CMD_BUFFER_SIZE 2000
632652

633653
while (1) { /* For "B" backup loop */
654+
// drucke prompt
634655
if (ask != NULL && !g_commandFileSilentFlag) {
635656
printf("%s", ask);
636657
#if __STDC__

src/mminou.h

Lines changed: 117 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -33,11 +33,27 @@ extern FILE *g_listFile_fp;
3333
extern flag g_outputToString;
3434
extern vstring g_printString;
3535
/* Global variables used by cmdInput() */
36+
/*!
37+
* \def MAX_COMMAND_FILE_NESTING
38+
* limits number of nested SUBMIT calls to 10. A SUBMIT redirects the input
39+
* to file, which in turn may temporarily redirect input to another file, and
40+
* so on.
41+
*/
3642
#define MAX_COMMAND_FILE_NESTING 10
43+
/*!
44+
* \var long g_commandFileNestingLevel
45+
* current level of nested SUBMIT commands. 0 is top level and refers to stdin
46+
* (usually the user controlled command line). Any invocation of SUBMIT
47+
* increases this value by 1. A return from a SUBMIT decrases it by 1 again.
48+
*/
3749
extern long g_commandFileNestingLevel;
3850
extern FILE *g_commandFilePtr[MAX_COMMAND_FILE_NESTING + 1];
3951
extern vstring g_commandFileName[MAX_COMMAND_FILE_NESTING + 1];
4052
extern flag g_commandFileSilent[MAX_COMMAND_FILE_NESTING + 1];
53+
/*!
54+
* \var g_commandFileSilentFlag
55+
* If set to 1, suppresses prompts on input.
56+
*/
4157
extern flag g_commandFileSilentFlag; /* For SUBMIT ... /SILENT */
4258

4359
extern FILE *g_input_fp; /* File pointers */
@@ -48,7 +64,7 @@ extern vstring g_input_fn, g_output_fn; /* File names */
4864
flag print2(const char* fmt,...);
4965
extern long g_screenHeight; /* Height of screen */
5066
/*!
51-
* \var g_screenWidth
67+
* \var long g_screenWidth
5268
* The minimum width of the display, measured in fixed width characters.
5369
*/
5470
extern long g_screenWidth; /* Width of screen */
@@ -63,18 +79,116 @@ extern long g_screenWidth; /* Width of screen */
6379
*/
6480
#define MAX_LEN 79 /* Default width of screen */
6581
#define SCREEN_HEIGHT 23 /* Lines on screen, minus 1 to account for prompt */
82+
/*!
83+
* \var flag g_scrollMode
84+
* \brief controls whether output stops after a full page is printed.
85+
*
86+
* A value of 1 indicates the user wants prompted page wise output.
87+
* The command SET SCROLL controls this value. If followed by CONTINUOUS, this
88+
* flag is reset to 0.
89+
*/
6690
extern flag g_scrollMode; /* Flag for continuous or prompted scroll */
91+
/*!
92+
* \var flag g_quitPrint
93+
* The value 1 indicates the user entered a 'q' at the last scrolling prompt.
94+
*/
6795
extern flag g_quitPrint; /* Flag that user typed 'q' to last scrolling prompt */
6896

6997
/* printLongLine automatically puts a newline \n in the output line. */
7098
void printLongLine(const char *line, const char *startNextLine, const char *breakMatch);
99+
/*!
100+
* \brief requests a line of text from the __stream__.
101+
*
102+
* If not suppressed, displays a prompt text on the screen. Then reads a
103+
* single line from the __stream__. Returns this line as a \a vstring.
104+
*
105+
* A line in the __stream__ is terminated by a LF character (0x0D) character
106+
* alone. It is read, but removed from the result. The maximum line length
107+
* without the LF is \a CMD_BUFFER_SIZE - 1. Reaching EOF (end of file) is
108+
* equivalent to reading LF, if at least 1 byte was read before. Note that the
109+
* NUL character can be part of the line. Reading a NUL is not sufficiently
110+
* handled in the current implementation and may or may not cause an error
111+
* message or even undefined behavior.
112+
*
113+
* Reading from an empty __stream__ (or one that is at EOF position) returns
114+
* NULL, not the empty string, and is formally signalled as an error.
115+
* Overflowing the buffer is also an error. No truncated value is returned.
116+
*
117+
* This routine automatically handles input in a loop under following two
118+
* conditions:
119+
*
120+
* 1. If scrolling is enabled, the input is interpreted. A line consisting of
121+
* a single character b or B indicates the user wants to scroll back through
122+
* saved pages of output. This is handled within this routine, as often as
123+
* requested and possible.
124+
*
125+
* 2. The user repetitively hits ENTER (only) while prompted in top level
126+
* context. The prompt is simply replayed as often. Entering an isolated 'b'
127+
* or 'B' is first directed to case 1, and only if it cannot be served there,
128+
* the routine exits, returning the b or B to the caller.
129+
*
130+
* No timeout is applied when waiting for user input from the console.
131+
*
132+
* Detected format errors result in following bug messages:
133+
* - 1507: The first read character is NUL
134+
* - 1508: line overflow, the last character is not NUL
135+
* - 1519: padding of LF failed, or first read character was NUL
136+
* - 1521: a NUL in first and second position was read
137+
* - 1523: no prompt text when user is required to input something
138+
* - 1525: missing terminating LF, not caused by an EOF.
139+
*
140+
* A bug message need not result in an execution stop.
141+
* \param[in] stream (not null) source to read the line from. _stdin_ is
142+
* common for user input from the console.
143+
* \param[in] ask prompt text displayed on the screen before __stream__ is
144+
* read. This prompt is suppressed by either a NULL value, or setting
145+
* \a g_commandFileSilentFlag to 1. This prompt must be not NULL (empty is
146+
* fine!) outside of a SUBMIT call, where user is expected to enter input.
147+
* \n
148+
* It may be compared to \a g_commandPrompt. If both match, it is inferred
149+
* the user is in top level command mode, where empty input is not returned
150+
* to the caller.
151+
* \return a \a vstring containing the read (or interpreted) line. The result
152+
* needs to be deallocated by the caller, if not empty or NULL.
153+
* \pre
154+
* The following variables are honored during execution and should be properly
155+
* set:
156+
* - \a commandFileSilentFlag value 1 suppresses prompts altogether, not only
157+
* those used for scrolling through long text;
158+
* - \a g_commandFileNestingLevel a value > 0 indicates a SUBMIT call is
159+
* executing, where scrolling prompts are suppressed;
160+
* - \a g_outputToString value 1 renders scrolling as pointless and disables it;
161+
* - \a backBuffer may contain text to display on scroll back operations;
162+
* - \a g_scrollMode value 1 enables scrolling back through text held in
163+
* \a backBuffer;
164+
* - \a localScrollMode a value of 0 temporarily disables scrolling, despite
165+
* the setting in \a g_scrollMode;
166+
* - \a g_commandPrompt if its string matches ask, empty input is ignored.
167+
* \post
168+
* \a db is updated and includes the length of the interpreted input.
169+
* Some input is ignored by simply reprinting the prompt:
170+
* - Empty strings in top command level;
171+
* - Isolated 'b' or 'B' input, if scroll mode is active, supported and the
172+
* \a backBuffer provides a saved page.
173+
* \warning the calling program must deallocate the returned string (if not
174+
* null or empty). Note that the result can be NULL. This is outside of the
175+
* usual behavior of a \a vstring type.
176+
* \warning the returned string need not be valid ASCII or UTF-8.
177+
* \bug If the first character read from __stream__ is NUL (e.g. a file is
178+
* read), this will cause a print of an error message, but execution
179+
* continues and in the wake may cause all kind of undefined behavior, like
180+
* memory accesses beyond allocated buffers.
181+
*/
71182
vstring cmdInput(FILE *stream, const char *ask);
72183
/*!
73184
* gets a line from either the terminal or the command file stream depending on
74185
* g_commandFileNestingLevel > 0. It calls cmdInput().
75186
* \param ask text displayed before input prompt. This can be located in
76-
* \a tempAllocStack.
77-
* \returns the entered input.
187+
* \a tempAllocStack. If this text contains more than \a g_screenWidth
188+
* characters, it is wrapped preferably at space characters and split across
189+
* multiple lines. The final line leaves space for enough for a ten
190+
* character user input
191+
* \return the entered input.
78192
* \warning the calling program must deallocate the returned string.
79193
*/
80194
vstring cmdInput1(const char *ask);

src/mmvstr.c

Lines changed: 39 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,10 @@ long g_startTempAllocStack = 0; /* Where to start freeing temporary allocatio
7171
* and copies the \a g_tempAllocStackTop into it, marking the begin of its own
7272
* scope of temporaries. Before returning, both values are restored again.
7373
*
74-
* The scope of top level functions begins at index 0.
74+
* The scope of top level functions begins at index 0
75+
*.
76+
* \invariant
77+
* - The entry at \a g_tempAllocStackTop is NULL.
7578
*/
7679
void *tempAllocStack[MAX_ALLOC_STACK];
7780

@@ -89,17 +92,25 @@ void freeTempAlloc(void) {
8992
} /* freeTempAlloc */
9093

9194
/*!
92-
* \fn pushTempAlloc
93-
* \brief pushes a \a temp_vstring onto the \a tempAllocStack.
95+
* \fn pushTempAlloc(void *mem)
96+
* \brief pushes a pointer onto the \a tempAllocStack.
9497
*
95-
* In case of a stack overflow \a bug is called.
98+
* In case of a stack overflow \a bug is called. This function is low level
99+
* that does not ensure that invariants of \a tempAllocStack are kept.
96100
*
97101
* \param mem (not null) points to either a non-mutable empty string, or
98-
* uniquely to allocated memory. Its contents need not be valid yet,
99-
* although it is highly recommended to point to a non-NUL character in the
100-
* latter case. If valid, it should point to a NUL terminated string.
101-
* \bug In case of stack overflow, the caller is not notified of this
102-
* condition, and a memory leak is likely.
102+
* to allocated memory. Its contents need not be valid yet, although it is
103+
* recommended to point to a non-NUL character.
104+
* \pre
105+
* The stack must not be full.
106+
* \post
107+
* If not full, \a mem is added on top of \a tempAllocStack, and
108+
* \a g_tempAllocStackTop is increased. This function
109+
* does not ensure a NULL pointer follows the pushed pointer. Statistics in
110+
* \a db1 is not updated.
111+
* \warning
112+
* In case of stack overflow, the caller is not notified and a memory leak
113+
* is likely.
103114
*/
104115
static void pushTempAlloc(void *mem)
105116
{
@@ -114,7 +125,25 @@ static void pushTempAlloc(void *mem)
114125
} /* pushTempAlloc */
115126

116127
/*!
117-
* \fn tempAlloc
128+
* \fn tempAlloc(long size)
129+
*
130+
* \brief allocates memory for size bytes and pushes it onto the \a tempAllocStack
131+
*
132+
* This low level function does NOT initialize the allocated memory. If the
133+
* allocation on the heap fails, \a bug is called. The statistic value \a db1
134+
* is updated.
135+
*
136+
* \param size (> 0) number of bytes to allocate on the heap. If the memory is
137+
* intended to hold NUL terminated text, then size must account for the final
138+
* NUL character, too.
139+
* \pre
140+
* The \a tempAllocStack must not be full.
141+
* \post
142+
* The top of \a tempAllocStack addresses memory at least the size of the
143+
* submitted parameter.
144+
* \warning
145+
* In case of stack overflow, the caller is not notified and a memory leak
146+
* is likely.
118147
*/
119148
static void* tempAlloc(long size) /* String memory allocation/deallocation */
120149
{

0 commit comments

Comments
 (0)