--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-main.c Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,249 @@
+/* Title: Tools/8bit/c-sources/isa2latex/conv-main.c
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1996 TU Muenchen
+
+converter for isabelle files
+main file (ANSI-C)
+
+ derived from
+
+ spec2latex: Version from 30.3.93
+ Authors Franz Huber, B. Rumpe, David v. Oheimb
+
+ New or changed features:
+
+ - flex is used to scan for multi character sequences
+ - automatic generation of flex source from user translation tables
+ - semantics of modes have changed, see the manpage
+ - flag for latex2e
+*/
+
+#include <stdio.h>
+
+/*
+ * VERSION:
+ */
+
+void version(void) {
+ fprintf(stderr, "Isabelle Converter, Version 1.4, 30 May 1996\n");
+}
+
+#include "conv-defs.h"
+#include "conv-tables.h"
+
+extern char *translateHi(int ch, int code);
+extern char *translateLow(int ch);
+extern char *translateLong(int ch);
+extern void reset_tabs(void);
+
+extern int yylex(void);
+
+FILE* finput; /* input file, default = stdin */
+FILE* foutput; /* output file,default = stdout */
+
+int use2e = FALSE; /* generate latex2e output */
+int bigTabs = FALSE; /* flag for big tabs */
+int tabBlanks = TABBLANKS; /* number of blanks subsituted for a tab */
+char isa_env_beg[200]; /* latex command to begin isa environment */
+char isa_env_end[200]; /* latex command to end isa environment */
+int cc; /* character counter in line */
+int tabcount; /* counter for tab positions */
+
+int destCode = DEFAULT_DEST; /* default destination */
+int convMode = DEFAULT_MODE; /* default conversion mode */
+int accept_ASCII = FALSE; /* accept ASCII input for 8bit characters */
+
+/*
+ * einfache Fehlerbehandlung:
+ */
+
+void error(char* s, char* t) {
+ fprintf(stderr, "Error! %s: %s\n", s, t);
+}
+
+
+/*
+ * erklaert Programmbenutzung:
+ */
+
+void usage(void) {
+ fprintf(stderr, "Isabelle converter. Valid Options:\n");
+ fprintf(stderr, "<file>: input file other than stdin\n");
+ fprintf(stderr, "-o <file>: output file other than stdout\n");
+ fprintf(stderr, "-a: generate 7 bit ASCII representation\n");
+ fprintf(stderr, "-A: accept ASCII representation of graphical characters (unsafe)\n");
+ fprintf(stderr, "-i: generate LaTeX representation (default)\n");
+ fprintf(stderr, " (for inclusion into other LaTeX documents)\n");
+ fprintf(stderr, "-s: generate standalone LaTeX document\n");
+ fprintf(stderr, "-x: allows mixture of specifications and given LaTeX parts\n");
+ fprintf(stderr, "-e: generate LaTeX2e code (if option -s given)\n");
+ fprintf(stderr, "-t <num>: set tabulator every <num> characters\n");
+ fprintf(stderr, " (for conversion to LaTeX; default: 8)\n");
+ fprintf(stderr, "-b: 'BigTabs'; generates bigger tabbings\n");
+ fprintf(stderr, " than standard for the LaTeX conversion\n");
+ fprintf(stderr, "-f <strg>: use another font than the default cmr-font when converting\n");
+ fprintf(stderr, " to LaTeX. <strg> is the font-string in LaTeX syntax\n");
+ fprintf(stderr, "-v: show version number and release date\n");
+ fprintf(stderr, "-h(elp): print this message\n");
+}
+
+
+/*
+ * main programm
+ */
+
+int main(int argc, char* argv[]) {
+ char *s; /* pointer to traverse components of argv */
+ char texFont[200]; /* string for TeX font change if destCode==TO_LaTeX */
+ int i,j;
+
+ /*
+ * initialize users font string:
+ */
+ texFont[0] = '\0';
+
+ finput = stdin;
+ foutput = stdout;
+
+ /*
+ * process command line
+ */
+ while (--argc > 0) {
+ s = *++argv;
+ if (*s++ == '-')
+ switch (*s) {
+ case 'v':
+ version();
+ exit(0);
+ case 'h':
+ usage();
+ exit(0);
+ case 'a':
+ destCode = TO_7bit;
+ break;
+ case 'A':
+ accept_ASCII = TRUE;
+ break;
+ case 'i':
+ destCode = TO_LaTeX;
+ convMode = INCLUDE;
+ break;
+ case 's':
+ destCode = TO_LaTeX;
+ convMode = STANDALONE;
+ break;
+ case 'x':
+ destCode = TO_LaTeX;
+ convMode = MIXED;
+ break;
+ case 'e':
+ use2e = TRUE;
+ break;
+ case 'b':
+ bigTabs = TRUE;
+ break;
+ case 'f':
+ if (--argc)
+ strncpy(texFont, *++argv, 200);
+ else
+ error("No font specified with -f option, using default", s);
+ break;
+ case 'o':
+ if (--argc) {
+ if ((foutput = fopen(*++argv, "w")) == NULL) {
+ error("Creating output file", *argv);
+ exit(-1);
+ }
+ } else {
+ error("No output file specified for option", s);
+ usage();
+ exit(-1);
+ }
+ break;
+ case 't':
+ { int temp;
+ if (--argc) {
+ if (temp = atoi(*++argv))
+ tabBlanks = temp;
+ else {
+ error("Not a valid tabulator value", *argv);
+ exit(-1);
+ }
+ } else {
+ error("No value specified for option", s);
+ usage();
+ exit(-1);
+ }
+ }
+ break;
+ default:
+ error("Unknown option", s);
+ usage();
+ exit(-1);
+ } /* switch */
+ else
+ /*
+ * no further parameters with "-"; therefore we see input file:
+ */
+ if ((finput = fopen(--s, "r")) == NULL) {
+ error("Opening input file", s);
+ exit(-1);
+ }
+ }
+
+ /*
+ * if destination is TO_LaTeX and mode is STANDALONE then produce LaTeX header
+ */
+
+ if (convMode == STANDALONE) {
+ if (use2e){
+ fprintf(foutput,
+ "\\documentclass[a4paper,11pt]{article}\n");
+ fprintf(foutput,
+ "\\usepackage{latexsym,amssymb,isa2latex}\n");
+ } else {
+ fprintf(foutput,
+ "\\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article}\n");
+ }
+ fprintf(foutput, "\\begin{document}\n");
+ }
+
+ if(texFont[0] != '\0') /* adjust font definition */
+ fprintf(foutput, "%s\n", texFont);
+
+ /*
+ * prepare a tabbing environment with tabstops every 'tabBlanks' blanks:
+ */
+ strcpy(isa_env_beg, "{\\isamode\\begin{tabbing}");
+ for (i = 0; i < NUM_TABS; i++) {
+ for (j = 0; j < tabBlanks; j++)
+ strcat(isa_env_beg, bigTabs ? BIG_TABBING_UNIT : NORMAL_TABBING_UNIT);
+ strcat(isa_env_beg, "\\=");
+ }
+ strcat(isa_env_beg, "\\kill{}\\hspace{-1ex}\n");
+ strcpy(isa_env_end, "\n\\end{tabbing}}");
+
+ if (convMode == STANDALONE || convMode == INCLUDE)
+ fprintf(foutput, isa_env_beg);
+
+ /*
+ * start the conversion: use lexer in all modes to do the job.
+ */
+
+ reset_tabs();
+ yylex();
+
+ /*
+ * output footers
+ */
+
+ if(convMode == STANDALONE || convMode == INCLUDE)
+ fprintf(foutput, isa_env_end);
+
+ if(convMode == STANDALONE)
+ fprintf(foutput, "\\end{document}\n");
+ return(0);
+}
+
+