Structured Typesetting (STS) generation #9
There are no files selected for viewing
This file contains hidden or 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 hidden or 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 hidden or 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 |
|---|---|---|
|
|
@@ -704,6 +704,7 @@ | |
| #include "mmunif.h" | ||
| #include "mmword.h" | ||
| #include "mmwtex.h" | ||
| #include "mmwsts.h" | ||
| #ifdef THINK_C | ||
| #include "mmmaci.h" | ||
| #endif | ||
|
|
@@ -2375,14 +2376,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 . */ | ||
| parsetSTSRules(stsOutput); | ||
| } | ||
|
|
||
| if (2/*error*/ == readTexDefs(0 /* 1 = check errors only */, | ||
|
|
@@ -2947,6 +2959,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 +2973,8 @@ void command(int argc, char *argv[]) | |
| i = 5; /* # arguments with only / HTML or / ALT_HTML */ | ||
| if (noVersioning) i = i + 2; | ||
| if (switchPos("/ TIME")) i = i + 2; | ||
| /* 7-Jul-2017 added MathML/STS */ | ||
| if (switchPos("/ STS")) i = i + 1; | ||
|
There was a problem hiding this comment. @wlammen wrote:
Interesting. So, a typical I'll add a comment to make that clearer. There was a problem hiding this comment. I am subject to a learning curve as well while reviewing, wrt both to your source code and the review style. |
||
| if (g_rawArgs != i) { | ||
| printLongLine(cat("?The HTML qualifiers may not be combined with", | ||
| " others except / NO_VERSIONING and / TIME.\n", NULL), " ", " "); | ||
|
|
@@ -3011,6 +3027,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. */ | ||
| parsetSTSRules(stsOutput); | ||
| } | ||
|
|
||
| q = 0; | ||
|
|
||
| /* Special feature: if the match statement starts with "*", we | ||
|
|
@@ -3082,20 +3107,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 +3267,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 +3420,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 +8134,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 hidden or 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 hidden or 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?
Uh oh!
There was an error while loading. Please reload this page.
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.