Structured Typesetting (STS) generation #9
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| *.o | ||
| metamath | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -20,6 +20,7 @@ | |
| memory management; converts between proof formats | ||
| mmhlpa.c - The help file, part 1. | ||
| mmhlpb.c - The help file, part 2. | ||
| mmhtbl.c - Hashtable implementation | ||
| mminou.c - Basic input and output interface | ||
| mmmaci.c - THINK C Macintosh interface (obsolete) | ||
| mmpars.c - Parses the source file | ||
|
|
@@ -29,6 +30,7 @@ | |
| mmveri.c - Proof verifier for source file | ||
| mmvstr.c - BASIC-like string functions | ||
| mmwtex.c - LaTeX/HTML source generation | ||
| mmwsts.c - STS source generation | ||
| mmword.c - File revision utility (for TOOLS> UPDATE) (not generally useful) | ||
| */ | ||
|
|
||
|
|
@@ -57,7 +59,16 @@ | |
|
|
||
|
|
||
|
|
||
| #define MVERSION "0.199 24-Dec-2021" | ||
| /* 0.199 tar 24-Dec-2021 mmwsts.c and others - Merge STS source generation code | ||
| originally developped in July 2017. STS stands for Structured TypeSetting and | ||
| can be used to generate MathML, which can in turn be postprocessed by MathJAX | ||
| to output mathematical typesetting (this includes indices, exponents, summands | ||
| and integrals with sets specifed below the sign, square roots with overhangs, | ||
| fraction bars, sized parentheses, etc.) The code introduces a new / STS flag | ||
| as a third alternative to / HTML and / ALT_HTML for HTML page generation, and | ||
| a / VERIFY STS option to only check the integrity of the external STS command | ||
| file. */ | ||
| /* 0.198 nm 7-Aug-2021 mmpars.c - Fix cosmetic bug in WRITE SOURCE ... /REWRAP | ||
| that prevented end of sentence (e.g. period) from appearing in column 79, | ||
| thus causing some lines to be shorter than necessary. */ | ||
|
|
@@ -704,6 +715,7 @@ | |
| #include "mmunif.h" | ||
| #include "mmword.h" | ||
| #include "mmwtex.h" | ||
| #include "mmwsts.h" | ||
| #ifdef THINK_C | ||
| #include "mmmaci.h" | ||
| #endif | ||
|
|
@@ -2375,14 +2387,25 @@ void command(int argc, char *argv[]) | |
| g_htmlFlag = 1; | ||
| /* If not specified, for backwards compatibility in scripts | ||
| leave g_altHtmlFlag at current value */ | ||
| /* 7-Jul-17 - MathML/STS handling */ | ||
| if (switchPos("/ HTML") != 0) { | ||
| if (switchPos("/ ALT_HTML") != 0 || switchPos("/ STS") != 0 ) { | ||
| print2("?Please specify only one of / HTML , / ALT_HTML and / STS.\n"); | ||
|
Comment on lines
+2141
to
+2142
There was a problem hiding this comment. @wlammen wrote:
I don't think this is called 3 times. There are 3 else..if branches, and it is called one time in each, to ensure only one HTML output formatting option is chosen. There was a problem hiding this comment. You're right. It still looks awkward since the call and the parameter is coded several times. |
||
| continue; | ||
| } | ||
| g_altHtmlFlag = 0; | ||
| } else if (switchPos("/ ALT_HTML") != 0) { | ||
| if (switchPos ("/ STS") != 0) { | ||
| print2 ("?Please specify only one of / HTML , / ALT_HTML and / STS.\n"); | ||
| continue; | ||
| } | ||
| g_altHtmlFlag = 1; | ||
| } else if (switchPos ("/ STS") != 0) { | ||
| stsFlag = 1; | ||
| let(&stsOutput, g_fullArg[5]); | ||
|
|
||
| /* Parse the STS rules corresponding to the expected output . */ | ||
| parseSTSRules(stsOutput); | ||
| } | ||
|
|
||
| if (2/*error*/ == readTexDefs(0 /* 1 = check errors only */, | ||
|
|
@@ -2947,6 +2970,8 @@ void command(int argc, char *argv[]) | |
| switchPos("/ HTML") | ||
| || switchPos("/ BRIEF_HTML") | ||
| || switchPos("/ ALT_HTML") | ||
| /* 7-Jul-2017 added MathML/STS */ | ||
| || switchPos("/ STS") | ||
| || switchPos("/ BRIEF_ALT_HTML"))) { | ||
| /* Special processing for the / HTML qualifiers - for each matching | ||
| statement, a .html file is opened, the statement is output, | ||
|
|
@@ -2959,6 +2984,8 @@ void command(int argc, char *argv[]) | |
| i = 5; /* # arguments with only / HTML or / ALT_HTML */ | ||
| if (noVersioning) i = i + 2; | ||
| if (switchPos("/ TIME")) i = i + 2; | ||
| /* 7-Jul-2017 added MathML/STS : one more argument for STS */ | ||
| if (switchPos("/ STS")) i = i + 1; | ||
| if (g_rawArgs != i) { | ||
| printLongLine(cat("?The HTML qualifiers may not be combined with", | ||
| " others except / NO_VERSIONING and / TIME.\n", NULL), " ", " "); | ||
|
|
@@ -3011,6 +3038,15 @@ void command(int argc, char *argv[]) | |
| g_altHtmlFlag = 0; | ||
| } | ||
|
|
||
| /* 7-Jul-2017 added MathML/STS */ | ||
| if (switchPos("/ STS")) { | ||
| stsFlag = 1; | ||
| let(&stsOutput, g_fullArg[5]); | ||
|
|
||
| /* Parse the STS rules corresponding to the expected output. */ | ||
| parseSTSRules(stsOutput); | ||
| } | ||
|
|
||
| q = 0; | ||
|
|
||
| /* Special feature: if the match statement starts with "*", we | ||
|
|
@@ -3082,20 +3118,32 @@ void command(int argc, char *argv[]) | |
| let(&g_texFileName, cat(g_Statement[g_showStatement].labelName, ".html", | ||
| NULL)); | ||
| } | ||
| /* 29-Sep-17 Thierry Arnoux - Post processing (for pre-rendering) */ | ||
| if(stsFlag && strlen(postProcess) != 0) { | ||
| vstring pipeCommand = ""; | ||
| print2("Creating and processing HTML file \"%s\"...\n", g_texFileName); | ||
| let(&pipeCommand, cat(postProcess, " > ", g_texFileName, NULL)); | ||
| g_texFilePtr = popen(pipeCommand, "w"); | ||
| if (!g_texFilePtr) print2("?Could not execute the command \"%s\".\n", | ||
| pipeCommand); | ||
| let(&pipeCommand, ""); | ||
| } | ||
| else { | ||
| print2("Creating HTML file \"%s\"...\n", g_texFileName); | ||
| g_texFilePtr = fSafeOpen(g_texFileName, "w", /* 17-Jul-2019 nm */ | ||
| noVersioning /*noVersioningFlag*/); | ||
| /****** old code before 17-Jul-2019 ******* | ||
| if (switchPos("/ NO_VERSIONING") == 0) { | ||
| g_texFilePtr = fSafeOpen(g_texFileName, "w", 0/@noVersioningFlag@/); | ||
| } else { | ||
| /@ 6-Jul-2008 nm Added / NO_VERSIONING @/ | ||
| /@ Don't create the backup versions ~1, ~2,... @/ | ||
| g_texFilePtr = fopen(g_texFileName, "w"); | ||
| if (!g_texFilePtr) print2("?Could not open the file \"%s\".\n", | ||
| g_texFileName); | ||
| } | ||
| ********* end of old code before 17-Jul-2019 *******/ | ||
| } | ||
| if (!g_texFilePtr) goto htmlDone; /* Couldn't open it (err msg was | ||
| provided) */ | ||
| g_texFileOpenFlag = 1; | ||
|
|
@@ -3230,7 +3278,10 @@ void command(int argc, char *argv[]) | |
| if (!instr(1, str3, cat(" ", str1, " ", NULL))) { | ||
| let(&str3, cat(str3, " ", str1, " ", NULL)); | ||
| let(&str2, ""); | ||
| /* 27 Jul 2017 tar For MathML/STS */ | ||
| if(stsFlag) str2 = stsToken((g_Statement[i].mathString)[j], i); | ||
| else | ||
| str2 = tokenToTex(g_MathToken[(g_Statement[i].mathString)[j] | ||
| ].tokenName, i/*stmt# for error msgs*/); | ||
| /* 2/9/02 Skip any tokens (such as |- in QL Explorer) that | ||
| may be suppressed */ | ||
|
|
@@ -3380,7 +3431,8 @@ void command(int argc, char *argv[]) | |
| ABORT_S: | ||
| /*** Close the html file ***/ | ||
| printTexTrailer(1 /*texHeaderFlag*/); | ||
| if(stsFlag && strlen(postProcess) != 0) pclose(g_texFilePtr); | ||
| else fclose(g_texFilePtr); | ||
| g_texFileOpenFlag = 0; | ||
| let(&g_texFileName,""); | ||
|
|
||
|
|
@@ -8093,6 +8145,13 @@ void command(int argc, char *argv[]) | |
| continue; | ||
| } | ||
|
|
||
| if (cmdMatches("VERIFY STS")) { | ||
| /* 12-Dec-17 - Go through all non-definition axioms, | ||
| * and check whether there is a corresponding STS scheme */ | ||
| verifySts(g_fullArg[2]); | ||
| continue; | ||
| } | ||
|
|
||
| print2("?This command has not been implemented.\n"); | ||
| continue; | ||
|
|
||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@wlammen writes:
I'm not sure which info you would like to add to the README.
There is a standard .gitignore file for C projects here, we could give it a try.
Maybe better in a separate PR?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The reason why I added this comment is, because the metamath sources are distributed via a tar archive as well. Obviously you wont need the gitignore in this case. I think, some kind of distribution how-to is finally called for. That are my thoughts. I was curious why you added the file. Separate PR is fine with me.