summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/bin/old/idcheck.l
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/bin/old/idcheck.l')
-rw-r--r--Master/texmf-dist/source/latex/stex/bin/old/idcheck.l130
1 files changed, 130 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/stex/bin/old/idcheck.l b/Master/texmf-dist/source/latex/stex/bin/old/idcheck.l
new file mode 100644
index 00000000000..9b1603527d2
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/bin/old/idcheck.l
@@ -0,0 +1,130 @@
+%{
+#include <string.h>
+int ur,ok,a,lin,i,j,c,n,m,d,s,q,fe,f,for_ok,curr_lin;
+typedef char idstr[50];
+idstr l[5000], r[5000];
+%}
+
+ID [a-zA-Z0-9._:\|-]*
+WS [\n\t ]*
+
+%s env inenv fid foc
+
+%%
+
+"\\begin"{WS}"{"("proof"|"example")"}"{WS}"[" {
+fe=1;
+for_ok=0;
+curr_lin=lin;
+BEGIN(env); // stuff that "for" keyval is recommended for
+}
+
+"\\begin"{WS}"{"("proof"|"example")"}" if (f) printf("Missing 'for' at line %d\n",lin);
+
+("\\begin"{WS}"{"("definition"|"assertion"|"proof"|"omtext"|"example"|"step"|"pfcase"|"module")"}"{WS}"[")|("\\justification"{WS}"[") {
+fe=0;
+BEGIN(env);
+}
+
+<env>"]" {
+if (fe && !for_ok && f) printf("Missing 'for' at line %d\n",curr_lin);
+BEGIN(INITIAL);
+}
+
+<env>"id"{WS}"="{WS} BEGIN(fid);
+
+<fid>{ID} {
+for (i=0; i<yyleng; i++) l[n][i]=yytext[i];
+l[n][yyleng]=0;
+if (s) printf("%s\n",l[n]);
+n++;
+BEGIN(env);
+}
+
+<env>("for"){WS}"="{WS} {
+for_ok=1;
+BEGIN(foc);
+}
+<env>("continues"|"for"|"uses"|"premises"){WS}"="{WS} BEGIN(foc);
+
+<foc>{ID} {
+for (j=0; j<yyleng; j++) r[m][j]=yytext[j];
+r[m][yyleng]=0;
+m++;
+BEGIN(env);
+}
+
+<env>("premises"|"uses"){WS}"="{WS}"{" BEGIN(inenv);
+
+<inenv>{ID} {
+strncpy(r[m],yytext,yyleng);
+r[m][yyleng]=0;
+m++;
+}
+
+<inenv>"}" BEGIN(env);
+
+\n {c++;lin++;}
+. c++;
+
+%%
+
+main(argc, argv)
+ int argc;
+ char **argv;
+{
+ if (argc==1) {
+ printf("Usage: idcheck [-q | -s | -f] filename(s)\n");
+ printf("Option -s shows all detected IDs. \n");
+ printf("Option -f shows line numbers for examples and proofs\n that have 'for' keyval missing. \n");
+ printf("Option -q for quiet mode.\n");
+ } else{
+ s=0; q=0;
+ a=1;
+ if (argv[1][0]=='-') {
+ a++;
+ for (j=1; j<strlen(argv[1]); j++)
+ if (argv[1][j]=='s') s=1; else
+ if (argv[1][j]=='q') q=1; else
+ if (argv[1][j]=='f') f=1;
+ }
+ d=0;
+ while (a<argc){
+ if (!q) printf("Parsing %s...\n",argv[a]);
+ yyin = fopen(argv[a] , "r");
+ c = 0;
+ lin = 1;
+ n = 0;
+ m = 0;
+ yylex();
+ fclose(yyin);
+ if (!q) printf("%d characters skipped. Found %d IDs. \n",c,n);
+ if (!q) printf("Checking for duplicates...\n");
+ for (i=0; i<n; i++)
+ for (j=i+1; j<n; j++)
+ if (strcmp(l[i],l[j])==0) {
+ printf("ID=%s is a duplicate in %s\n",l[i],argv[a]);
+ d++;
+ }
+ if (!q) printf("Found %d duplicates.\n",d);
+ if (!q) printf("Checking references... (found %d)\n",m);
+ ur=0;
+ for (i=0;i<m; i++){
+ ok=0;
+ for (j=0; j<n; j++)
+ if (strcmp(r[i],l[j])==0){
+ ok=1;
+ break;
+ }
+ if (!ok) {
+ printf("Unmatched reference for ID=%s\n",r[i]);
+ ur++;
+ }
+ }
+ if (!q) printf("Found %d unmatched references.\n",ur);
+ a++;
+ }
+ return d+ur;
+ }
+ return 1;
+}