summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/bin/old
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/bin/old')
-rw-r--r--Master/texmf-dist/source/latex/stex/bin/old/Makefile28
-rw-r--r--Master/texmf-dist/source/latex/stex/bin/old/defcon.l91
-rw-r--r--Master/texmf-dist/source/latex/stex/bin/old/idcheck.l130
-rw-r--r--Master/texmf-dist/source/latex/stex/bin/old/modstr.l137
-rwxr-xr-xMaster/texmf-dist/source/latex/stex/bin/old/symdef46
5 files changed, 432 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/stex/bin/old/Makefile b/Master/texmf-dist/source/latex/stex/bin/old/Makefile
new file mode 100644
index 00000000000..d2ae41c6401
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/bin/old/Makefile
@@ -0,0 +1,28 @@
+all: src exec
+
+src: idcheck.l defcon.l modstr.l
+ flex -ft idcheck.l > idcheck.yy.c
+ flex -ft defcon.l > defcon.yy.c
+ flex -f+t modstr.l > modstr.yy.cc
+
+idcheck: idcheck.l
+ flex -f $<
+ gcc lex.yy.c -lfl -o idcheck
+
+defcon: defcon.l
+ flex -f $<
+ gcc lex.yy.c -lfl -o defcon
+
+modstr: modstr.l
+ flex -f+ $<
+ g++ lex.yy.cc -lfl -o modstr
+
+exec: idcheck.yy.c defcon.yy.c modstr.yy.cc
+ gcc idcheck.yy.c -lfl -o idcheck
+ gcc defcon.yy.c -lfl -o defcon
+ g++ modstr.yy.cc -lfl -o modstr
+
+clean:
+ rm -f *.yy.c *.yy.cc *~
+
+distclean: clean
diff --git a/Master/texmf-dist/source/latex/stex/bin/old/defcon.l b/Master/texmf-dist/source/latex/stex/bin/old/defcon.l
new file mode 100644
index 00000000000..ad758086145
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/bin/old/defcon.l
@@ -0,0 +1,91 @@
+%{
+
+#include <string.h>
+
+char ltxml[100];
+char fext[6] = ".ltxml";
+
+char symstr[200];
+char ltxmlstr[200];
+
+int i,t,c,tmp,q;
+FILE *lt;
+
+%}
+
+ID [a-zA-Z0-9._:\|-]*
+NR [0-9]*
+
+%s idenv env sym
+
+%%
+
+"\\begin{module}"(" ")*"[" BEGIN(idenv);
+<idenv>"]" BEGIN(INITIAL);
+
+<idenv>"id="{ID} {
+ for (i=3; i<yyleng; i++) ltxml[i-3]=yytext[i];
+ t=yyleng-3;
+ tmp=strlen(fext);
+ for (i=0; i<tmp; i++) ltxml[t+i]=fext[i];
+ t=t+tmp;
+ ltxml[t]=0;
+ if (!q) printf("File %s\n",ltxml);
+ lt = fopen(ltxml,"w");
+ BEGIN(env);
+}
+
+<env>"symdef{\\"{ID}"}"(.)* {
+i=7;
+while (yytext[i]!='}'){
+ symstr[i-7]=yytext[i];
+ i++;
+}
+symstr[i-7]=0;
+BEGIN(sym);
+}
+
+<sym>"latexmldef{"(.)* {
+i=11;
+while (i<yyleng){
+ ltxmlstr[i-11]=yytext[i];
+ i++;
+}
+ltxmlstr[i-12]=0;
+fprintf(lt,"DefConstructor('\%s{}...{}','%s')\n",symstr,ltxmlstr);
+BEGIN(env);
+}
+
+<env,sym>"\\end{module}" {
+fclose(lt);
+BEGIN(INITIAL);
+}
+
+\n c++;
+. c++;
+
+%%
+
+main(argc, argv)
+ int argc;
+ char **argv;
+{
+ if (argc==1) {
+ printf("arguments expected: [-q] filename(s)\n");
+ } else {
+ q=0;
+ i=1;
+ if (argv[1][0]=='-'){
+ i++;
+ if (argv[1][1]=='q') q=1;
+ }
+ while (i<argc){
+ if (!q) printf("Processing %s...\n",argv[i]);
+ yyin = fopen(argv[i], "r");
+ c=0;
+ yylex();
+ fclose(yyin);
+ i++;
+ }
+ }
+}
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;
+}
diff --git a/Master/texmf-dist/source/latex/stex/bin/old/modstr.l b/Master/texmf-dist/source/latex/stex/bin/old/modstr.l
new file mode 100644
index 00000000000..ae0101147c5
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/bin/old/modstr.l
@@ -0,0 +1,137 @@
+%{
+#include <iostream>
+#include <string>
+#include <map>
+#include <vector>
+using namespace std;
+
+
+const int indent = 4;
+const char start_char = '*';
+
+typedef struct {
+ vector<string> defs,list;
+ int father;
+} nodetype;
+
+map<string,nodetype> g;
+
+string vertex, data;
+int d, miss, skip;
+
+int max(int, int);
+
+%}
+
+ID [a-zA-Z0-9._:\|-]*
+SEP [,;]*
+WS [\n\t ]*
+M [^}]*
+
+%x in_module found_vertex in_module_cont mdef
+%x found_one_child found_more_children
+
+%%
+
+<INITIAL>"\\begin"{WS}"{module}"{WS}"[" BEGIN(in_module);
+
+<in_module>"id"{WS}"=" BEGIN(found_vertex);
+<found_vertex>{ID} {
+vertex = YYText();
+g[vertex].father=0;
+if (miss) cout << endl << "<-------- Module '" << vertex
+ << "' -------->" << endl << endl;
+BEGIN(in_module);
+}
+<in_module>"uses"{WS}"=" BEGIN(found_one_child);
+<found_one_child>"{" BEGIN(found_more_children);
+<found_more_children>"}" BEGIN(in_module);
+<found_one_child>{ID} {
+data=YYText();
+if (g[data].list.empty())
+ g[vertex].father=g[data].father+1;
+else
+ g[vertex].father=max(g[data].father+1,g[vertex].father);
+g[data].list.push_back(vertex);
+BEGIN(in_module);
+}
+<found_more_children>{ID} {
+data=YYText();
+if (g[data].list.empty())
+ g[vertex].father=g[data].father+1;
+else
+ g[vertex].father=max(g[data].father+1,g[vertex].father);
+g[data].list.push_back(vertex);
+}
+
+<found_one_child,found_more_children,found_vertex>{SEP}|{WS}
+
+<in_module>"]" BEGIN(in_module_cont);
+
+<in_module,in_module_cont>(.|\n)
+
+<in_module_cont>"\\"("symdef"|"abbrdef"|"elldef"|"aliasdef"){WS}"{"{WS} BEGIN(mdef);
+<mdef>{M} {
+data = YYText();
+g[vertex].defs.push_back(data);
+}
+<mdef>"}" BEGIN(in_module_cont);
+<in_module_cont>"\\end"{WS}"{module}" BEGIN(INITIAL);
+
+<INITIAL>(.|\n) if (miss) cout << YYText();
+
+<*>{WS}(%)(.)*(\n)*
+
+%%
+
+void spc(int n){
+ for(int i=0; i<n; i++) cout << " ";
+}
+
+int max(int a, int b){
+ return a>b?a:b;
+}
+
+void go(map<string, nodetype > ::iterator node, int depth){
+if (skip && node->second.father!=depth) return;
+spc(d);
+cout << start_char << " " << node->first << "{";
+int tmp = node->second.defs.size()-1;
+for (int j=0; j<=tmp; j++){
+ cout << node->second.defs[j];
+ if (j!=tmp) cout << ",";
+}
+cout << "}" << endl;
+d+=indent;
+for (int i=0; i<node->second.list.size(); i++)
+ go(g.find(node->second.list[i]),depth+1);
+d-=indent;
+}
+
+int main(int argc, char** argv){
+miss=0;
+skip=0;
+if (argc==2)
+ if (argv[1][0]=='-')
+ for (int z=1; argv[1][z]!=0; z++)
+ if (argv[1][z]=='m') miss=1; else
+ if (argv[1][z]=='s') skip=1; else
+ if (argv[1][z]=='h') {
+ cout << " Usage: modstr [-s|m|h]\n Input: stdin\n Output: stdout\n";
+ cout << " Options: -s Show module usage only at the deepest level\n";
+ cout << " -m Show text not within a module\n";
+ cout << " -h This help screen\n";
+ return 0;
+ }
+if (miss) cout << "Text NOT within a module:\n" << endl;
+FlexLexer* lex = new yyFlexLexer;
+lex->yylex();
+d=0;
+map<string, nodetype > ::iterator start = g.begin();
+map<string, nodetype > ::iterator stop = g.end();
+cout << endl;
+for(;stop!=start;start++)
+ if (!start->second.father) go(start,0);
+cout << endl;
+return 0;
+}
diff --git a/Master/texmf-dist/source/latex/stex/bin/old/symdef b/Master/texmf-dist/source/latex/stex/bin/old/symdef
new file mode 100755
index 00000000000..b5c789a1c72
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/bin/old/symdef
@@ -0,0 +1,46 @@
+#!/usr/bin/perl -w
+
+use strict;
+use Getopt::Long;
+use Pod::Usage;
+
+my $output = "-";
+my $input = "-";
+
+GetOptions("output=s",\$output);
+
+$input = $ARGV[0] if @ARGV;
+
+open(FIN,$input) or die "Can't open input file.";
+open(FOUT,">$output");
+
+my $line;
+
+while ($line=<FIN>){
+ if ($line !~ m/symdef/ && $line !~ m/elldef/ && $line !~ m/abbrdef/){
+ print FOUT $line;
+ next;
+ }
+ if ($line =~ m/\}\[\d,/){
+ print FOUT $line;
+ next;
+ }
+
+ if ($line =~ m/\\(sym|abbr|ell)def\{\\([^\}]+)\}\[(\d)\]([^\n\%]+)(.*)/){
+ print FOUT "\\$1def{\\$2}[$3,name=$2]$4$5\n";
+ } else {
+ if ($line =~ m/\\(sym|ell|abbr)def\{\\([^\}]+)\}([^\n\%]+)(.*)/){
+ print FOUT "\\$1def{\\$2}[0,name=$2]$3$4\n";
+ }
+ }
+}
+
+close(FIN);
+close(FOUT);
+
+
+__END__
+
+=head1 SYNOPSIS
+
+symdef [--output=outputfile] [texfile]