1 /* Title: Tools/8bit/c-sources/isa2latex/conv-main.c |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1996 TU Muenchen |
|
5 |
|
6 converter for isabelle files |
|
7 main file (ANSI-C) |
|
8 |
|
9 derived from |
|
10 |
|
11 spec2latex: Version from 30.3.93 |
|
12 Authors Franz Huber, B. Rumpe, David v. Oheimb |
|
13 |
|
14 New or changed features: |
|
15 |
|
16 - flex is used to scan for multi character sequences |
|
17 - automatic generation of flex source from user translation tables |
|
18 - semantics of modes have changed, see the manpage |
|
19 - flag for latex2e |
|
20 */ |
|
21 |
|
22 #include <stdio.h> |
|
23 |
|
24 /* |
|
25 * VERSION: |
|
26 */ |
|
27 |
|
28 void version(void) { |
|
29 fprintf(stderr, "Isabelle Converter, Version 1.4, 30 May 1996\n"); |
|
30 } |
|
31 |
|
32 #include "conv-defs.h" |
|
33 #include "conv-tables.h" |
|
34 |
|
35 extern char *translateHi(int ch, int code); |
|
36 extern char *translateLow(int ch); |
|
37 extern char *translateLong(int ch); |
|
38 extern void reset_tabs(void); |
|
39 |
|
40 extern int yylex(void); |
|
41 |
|
42 FILE* finput; /* input file, default = stdin */ |
|
43 FILE* foutput; /* output file,default = stdout */ |
|
44 |
|
45 int use2e = FALSE; /* generate latex2e output */ |
|
46 int bigTabs = FALSE; /* flag for big tabs */ |
|
47 int tabBlanks = TABBLANKS; /* number of blanks subsituted for a tab */ |
|
48 char isa_env_beg0[200], /* latex command to begin isa environment */ |
|
49 isa_env_beg1[200]; |
|
50 char isa_env_end[200]; /* latex command to end isa environment */ |
|
51 int cc; /* character counter in line */ |
|
52 int tabcount; /* counter for tab positions */ |
|
53 |
|
54 int destCode = DEFAULT_DEST; /* default destination */ |
|
55 int convMode = DEFAULT_MODE; /* default conversion mode */ |
|
56 int accept_ASCII = FALSE; /* accept ASCII input for 8bit characters */ |
|
57 |
|
58 /* |
|
59 * einfache Fehlerbehandlung: |
|
60 */ |
|
61 |
|
62 void error(char* s, char* t) { |
|
63 fprintf(stderr, "Error! %s: %s\n", s, t); |
|
64 } |
|
65 |
|
66 |
|
67 /* |
|
68 * erklaert Programmbenutzung: |
|
69 */ |
|
70 |
|
71 void usage(void) { |
|
72 fprintf(stderr, "Isabelle converter. Valid Options:\n"); |
|
73 fprintf(stderr, "<file>: input file other than stdin\n"); |
|
74 fprintf(stderr, "-o <file>: output file other than stdout\n"); |
|
75 fprintf(stderr, "-a: generate 7 bit ASCII representation\n"); |
|
76 fprintf(stderr, "-A: accept ASCII representation of graphical characters (unsafe)\n"); |
|
77 fprintf(stderr, "-i: generate LaTeX representation (default)\n"); |
|
78 fprintf(stderr, " (for inclusion into other LaTeX documents)\n"); |
|
79 fprintf(stderr, "-s: generate standalone LaTeX document\n"); |
|
80 fprintf(stderr, "-x: allows mixture of specifications and given LaTeX parts\n"); |
|
81 fprintf(stderr, "-e: generate LaTeX2e code (if option -s given)\n"); |
|
82 fprintf(stderr, "-t <num>: set tabulator every <num> characters\n"); |
|
83 fprintf(stderr, " (for conversion to LaTeX; default: 8)\n"); |
|
84 fprintf(stderr, "-b: 'BigTabs'; generates bigger tabbings\n"); |
|
85 fprintf(stderr, " than standard for the LaTeX conversion\n"); |
|
86 fprintf(stderr, "-f <strg>: use another font than the default cmr-font when converting\n"); |
|
87 fprintf(stderr, " to LaTeX. <strg> is the font-string in LaTeX syntax\n"); |
|
88 fprintf(stderr, "-v: show version number and release date\n"); |
|
89 fprintf(stderr, "-h(elp): print this message\n"); |
|
90 } |
|
91 |
|
92 |
|
93 /* |
|
94 * main programm |
|
95 */ |
|
96 |
|
97 int main(int argc, char* argv[]) { |
|
98 char *s; /* pointer to traverse components of argv */ |
|
99 char texFont[200]; /* string for TeX font change if destCode==TO_LaTeX */ |
|
100 int i,j; |
|
101 |
|
102 /* |
|
103 * initialize users font string: |
|
104 */ |
|
105 texFont[0] = '\0'; |
|
106 |
|
107 finput = stdin; |
|
108 foutput = stdout; |
|
109 |
|
110 /* |
|
111 * process command line |
|
112 */ |
|
113 while (--argc > 0) { |
|
114 s = *++argv; |
|
115 if (*s++ == '-') |
|
116 switch (*s) { |
|
117 case 'v': |
|
118 version(); |
|
119 exit(0); |
|
120 case 'h': |
|
121 usage(); |
|
122 exit(0); |
|
123 case 'a': |
|
124 destCode = TO_7bit; |
|
125 break; |
|
126 case 'A': |
|
127 accept_ASCII = TRUE; |
|
128 break; |
|
129 case 'i': |
|
130 destCode = TO_LaTeX; |
|
131 convMode = INCLUDE; |
|
132 break; |
|
133 case 's': |
|
134 destCode = TO_LaTeX; |
|
135 convMode = STANDALONE; |
|
136 break; |
|
137 case 'x': |
|
138 destCode = TO_LaTeX; |
|
139 convMode = MIXED; |
|
140 break; |
|
141 case 'e': |
|
142 use2e = TRUE; |
|
143 break; |
|
144 case 'b': |
|
145 bigTabs = TRUE; |
|
146 break; |
|
147 case 'f': |
|
148 if (--argc) |
|
149 strncpy(texFont, *++argv, 200); |
|
150 else |
|
151 error("No font specified with -f option, using default", s); |
|
152 break; |
|
153 case 'o': |
|
154 if (--argc) { |
|
155 if ((foutput = fopen(*++argv, "w")) == NULL) { |
|
156 error("Creating output file", *argv); |
|
157 exit(-1); |
|
158 } |
|
159 } else { |
|
160 error("No output file specified for option", s); |
|
161 usage(); |
|
162 exit(-1); |
|
163 } |
|
164 break; |
|
165 case 't': |
|
166 { int temp; |
|
167 if (--argc) { |
|
168 if (temp = atoi(*++argv)) |
|
169 tabBlanks = temp; |
|
170 else { |
|
171 error("Not a valid tabulator value", *argv); |
|
172 exit(-1); |
|
173 } |
|
174 } else { |
|
175 error("No value specified for option", s); |
|
176 usage(); |
|
177 exit(-1); |
|
178 } |
|
179 } |
|
180 break; |
|
181 default: |
|
182 error("Unknown option", s); |
|
183 usage(); |
|
184 exit(-1); |
|
185 } /* switch */ |
|
186 else |
|
187 /* |
|
188 * no further parameters with "-"; therefore we see input file: |
|
189 */ |
|
190 if ((finput = fopen(--s, "r")) == NULL) { |
|
191 error("Opening input file", s); |
|
192 exit(-1); |
|
193 } |
|
194 } |
|
195 |
|
196 /* |
|
197 * if destination is TO_LaTeX and mode is STANDALONE then produce LaTeX header |
|
198 */ |
|
199 |
|
200 if (convMode == STANDALONE) { |
|
201 if (use2e){ |
|
202 fprintf(foutput, |
|
203 "\\documentclass[]{article}\n"); |
|
204 fprintf(foutput, |
|
205 "\\usepackage{latexsym,amssymb,isa2latex}\n"); |
|
206 } else { |
|
207 fprintf(foutput, |
|
208 "\\documentstyle[10pt,latexsym,amssymb,isa2latex]{article}\n"); |
|
209 } |
|
210 fprintf(foutput, "\\topmargin-8ex\n" |
|
211 "\\oddsidemargin0ex\n" |
|
212 "\\textheight158ex\n" |
|
213 "\\begin{document}\n"); |
|
214 } |
|
215 |
|
216 if(texFont[0] != '\0') /* adjust font definition */ |
|
217 fprintf(foutput, "%s\n", texFont); |
|
218 |
|
219 /* |
|
220 * prepare a tabbing environment with tabstops every 'tabBlanks' blanks: |
|
221 strcpy(isa_env_beg, "{\\isamode\\begin{tabbing}"); |
|
222 for (i = 0; i < NUM_TABS; i++) { |
|
223 for (j = 0; j < tabBlanks; j++) |
|
224 strcat(isa_env_beg, bigTabs ? BIG_TABBING_UNIT : NORMAL_TABBING_UNIT); |
|
225 strcat(isa_env_beg, "\\="); |
|
226 } |
|
227 strcat(isa_env_beg, "\\kill{}\\hspace{-1.2ex}\n"); |
|
228 strcpy(isa_env_end, "\n\\end{tabbing}}"); |
|
229 */ |
|
230 strcpy(isa_env_beg0, "{\\isabegin{}\\noindent "); |
|
231 strcpy(isa_env_beg1, "{\\isabegin{\\isamodify}\\noindent "); |
|
232 strcpy(isa_env_end , "\\isaend}\\noindent "); |
|
233 |
|
234 if (convMode == STANDALONE || (convMode == INCLUDE) && (destCode != TO_7bit)) |
|
235 fprintf(foutput, isa_env_beg0); |
|
236 |
|
237 /* |
|
238 * start the conversion: use lexer in all modes to do the job. |
|
239 */ |
|
240 |
|
241 reset_tabs(); |
|
242 yylex(); |
|
243 |
|
244 /* |
|
245 * output footers |
|
246 */ |
|
247 |
|
248 if(convMode == STANDALONE || (convMode == INCLUDE) && (destCode != TO_7bit)) |
|
249 fprintf(foutput, isa_env_end); |
|
250 |
|
251 if(convMode == STANDALONE) |
|
252 fprintf(foutput, "\\end{document}\n"); |
|
253 return(0); |
|
254 } |
|
255 |
|
256 |
|