# HG changeset patch
# User oheimb
# Date 878741151 -3600
# Node ID 6b8bbcc9f05f058b812c4a2c8f8508f42df51280
# Parent  c63f261fb025805a4612740dfbb7c294125a7385
several minor improvements

diff -r c63f261fb025 -r 6b8bbcc9f05f src/Tools/8bit/c-sources/isa2latex/conv-defs.h
--- a/src/Tools/8bit/c-sources/isa2latex/conv-defs.h	Wed Nov 05 15:42:30 1997 +0100
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-defs.h	Wed Nov 05 15:45:51 1997 +0100
@@ -54,8 +54,8 @@
 /* BEGIN gen-isa2latex */
 #define START_LOW_TABLE 32
 #define END_LOW_TABLE   126
-#define START_HI_TABLE  161
+#define START_HI_TABLE  160
 #define END_HI_TABLE    255
-#define SEQ_TABLE       11
+#define SEQ_TABLE       27
 /* END gen-isa2latex */
 
diff -r c63f261fb025 -r 6b8bbcc9f05f src/Tools/8bit/c-sources/isa2latex/conv-lex.x
--- a/src/Tools/8bit/c-sources/isa2latex/conv-lex.x	Wed Nov 05 15:42:30 1997 +0100
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-lex.x	Wed Nov 05 15:45:51 1997 +0100
@@ -18,7 +18,7 @@
 extern FILE *finput, *foutput;
 extern int tabBlanks;
 extern int tabcount;
-extern char isa_env_beg[], isa_env_end[];
+extern char isa_env_beg0[], isa_env_beg1[], isa_env_end[];
 extern int convMode;
 extern int accept_ASCII;
 extern int destCode;
@@ -44,11 +44,14 @@
   else 
 	BEGIN_ISA;
 
-<LATEX>\\I@		{ BEGIN_ISA; inline_mode=TRUE ; fprintf(foutput, 
-				"{\\isainline{"); }
-<LATEX>\\I@isa[ \t]*\n?	{ BEGIN_ISA; inline_mode=FALSE; fprintf(foutput, 
-				isa_env_beg); reset_tabs(); 
-			  if (yytext[strlen(yytext)-1] == '\n') lineno++;
+<LATEX>\\I@@?		{ BEGIN_ISA; inline_mode=TRUE ; fprintf(foutput, 
+			  (yytext[3]=='@' ? "\\mbox{\\isainline[\\isamodify]{"
+					  : "\\mbox{\\isainline{")); }
+<LATEX>\\I@isa@?[ \t]*\n? { BEGIN_ISA; inline_mode=FALSE; fprintf(foutput, 
+				(yytext[6]=='@' ? isa_env_beg1
+						: isa_env_beg0)); reset_tabs(); 
+			  if (yytext[strlen(yytext)-1] == '\n')
+			  { fprintf(foutput, "\n"); lineno++; }
 			}
 <LATEX>\\E@		{ ECHO; not_suitable("\\E@","LATEX"); }
 <LATEX>\n		{ put(*yytext,FALSE,0); lineno++; }
@@ -59,7 +62,9 @@
 			  else
 			  { ECHO; not_suitable("\\I@","ISA"); }
 			}
-<ISA,ISAA>\n?[ \t]*\\I@isa	{ if (inline_mode)
+<ISA,ISAA>\n?[ \t]*\\I@isa {if (yytext[0] == '\n')
+			    { fprintf(foutput, "\n"); lineno++; };
+			  if (inline_mode)
 			  { ECHO; not_suitable("\\I@isa","INLINE"); }
 			  else
 			  { if (convMode == MIXED) {
@@ -68,7 +73,6 @@
 			      ECHO; warning(
 				"\\I@isa only allowed with -x option"); }
 			  }
-			  if (yytext[0] == '\n') lineno++;
 			}
 <ISA,ISAA>\\E@		{ BEGIN ESC; fprintf(foutput, "{\\isaescape{"); }
 <ISA,ISAA><<EOF>>	{ if (convMode == MIXED) 
@@ -96,129 +100,162 @@
   /* The following is generated by the perl script gen-isa2latex. */
   /* Make modifications in configuration file for gen-isa2latex!  */             
   /* BEGIN_OF_HI_TABLE */
-<ISAA>\\Gamma\         	put((char)161,FALSE,0);
-<ISAA>\\Delta\         	put((char)162,FALSE,0);
-<ISAA>\\Theta\         	put((char)163,FALSE,0);
-<ISAA>LAM\             	put((char)164,FALSE,0);
-<ISAA>\\Pi\            	put((char)165,FALSE,0);
-<ISAA>\\Sigma\         	put((char)166,FALSE,0);
-<ISAA>\\Phi\           	put((char)167,FALSE,0);
-<ISAA>\\Psi\           	put((char)168,FALSE,0);
-<ISAA>\\Omega\         	put((char)169,FALSE,0);
-<ISAA>'a               	put((char)170,FALSE,0);
-<ISAA>'b               	put((char)171,FALSE,0);
-<ISAA>'c               	put((char)172,FALSE,0);
-<ISAA>\\delta\         	put((char)173,FALSE,0);
-<ISAA>\\varepsilon\    	put((char)174,FALSE,0);
-<ISAA>\\zeta\          	put((char)175,FALSE,0);
-<ISAA>\\eta\           	put((char)176,FALSE,0);
-<ISAA>\\vartheta\      	put((char)177,FALSE,0);
-<ISAA>\\kappa\         	put((char)178,FALSE,0);
-<ISAA>%\               	put((char)179,FALSE,0);
-<ISAA>\\mu\            	put((char)180,FALSE,0);
-<ISAA>\\nu\            	put((char)181,FALSE,0);
-<ISAA>\\xi\            	put((char)182,FALSE,0);
-<ISAA>\\pi\            	put((char)183,FALSE,0);
-<ISAA>'r               	put((char)184,FALSE,0);
-<ISAA>'s               	put((char)185,FALSE,0);
-<ISAA>'t               	put((char)186,FALSE,0);
-<ISAA>\\varphi\        	put((char)187,FALSE,0);
-<ISAA>\\chi\           	put((char)188,FALSE,0);
-<ISAA>\\psi\           	put((char)189,FALSE,0);
-<ISAA>\\omega\         	put((char)190,FALSE,0);
-<ISAA>~\               	put((char)191,FALSE,0);
-<ISAA>&\               	put((char)192,FALSE,0);
-<ISAA>\|\              	put((char)193,FALSE,0);
-<ISAA>!\               	put((char)194,FALSE,0);
-<ISAA>\?\              	put((char)195,FALSE,0);
-<ISAA>!!               	put((char)196,FALSE,0);
-<ISAA>\\lceil\         	put((char)197,FALSE,0);
-<ISAA>\\rceil\         	put((char)198,FALSE,0);
-<ISAA>\\lfloor\        	put((char)199,FALSE,0);
-<ISAA>\\rfloor\        	put((char)200,FALSE,0);
-<ISAA>\(\|             	put((char)201,FALSE,0);
-<ISAA>\|\)             	put((char)202,FALSE,0);
-<ISAA>\[\|             	put((char)203,FALSE,0);
-<ISAA>\|\]             	put((char)204,FALSE,0);
-<ISAA>{}               	put((char)205,FALSE,0);
-<ISAA>\ :\             	put((char)206,FALSE,0);
-<ISAA>\subseteq\       	put((char)207,FALSE,0);
-<ISAA>\ Int\           	put((char)208,FALSE,0);
-<ISAA>\ Un\            	put((char)209,FALSE,0);
-<ISAA>Inter\           	put((char)210,FALSE,0);
-<ISAA>Union\           	put((char)211,FALSE,0);
-<ISAA>\sqcap\          	put((char)212,FALSE,0);
-<ISAA>\sqcup\          	put((char)213,FALSE,0);
-<ISAA>glb\             	put((char)214,FALSE,0);
-<ISAA>lub\             	put((char)215,FALSE,0);
-<ISAA>UU               	put((char)216,FALSE,0);
-<ISAA>===              	put((char)217,FALSE,0);
-<ISAA>==               	put((char)218,FALSE,0);
-<ISAA>~=               	put((char)219,FALSE,0);
-<ISAA>\\sqsubset\      	put((char)220,FALSE,0);
-<ISAA><<               	put((char)221,FALSE,0);
-<ISAA>\\prec\          	put((char)222,FALSE,0);
-<ISAA>\\preceq\        	put((char)223,FALSE,0);
-<ISAA>\\succ\          	put((char)224,FALSE,0);
-<ISAA>\\succeq\        	put((char)225,FALSE,0);
-<ISAA>\\sim\           	put((char)226,FALSE,0);
-<ISAA>\\simeq\         	put((char)227,FALSE,0);
-<ISAA>\\le\            	put((char)228,FALSE,0);
-<ISAA>\\ge\            	put((char)229,FALSE,0);
-<ISAA><-               	put((char)230,FALSE,0);
-<ISAA>-@@@@@           	put((char)231,FALSE,0);
-<ISAA>->               	put((char)232,FALSE,0);
-<ISAA>\\Leftarrow\     	put((char)233,FALSE,0);
-<ISAA>=@@@@@           	put((char)234,FALSE,0);
-<ISAA>=>               	put((char)235,FALSE,0);
-<ISAA>->>              	put((char)236,FALSE,0);
-<ISAA>\\mapsto\        	put((char)237,FALSE,0);
-<ISAA>\\leadsto\       	put((char)238,FALSE,0);
-<ISAA>\\uparrow\       	put((char)239,FALSE,0);
-<ISAA>\\downarrow\     	put((char)240,FALSE,0);
-<ISAA>~:               	put((char)241,FALSE,0);
-<ISAA>\\times\         	put((char)242,FALSE,0);
-<ISAA>\\oplus\         	put((char)243,FALSE,0);
-<ISAA>\\ominus\        	put((char)244,FALSE,0);
-<ISAA>\\otimes\        	put((char)245,FALSE,0);
-<ISAA>\\oslash\        	put((char)246,FALSE,0);
-<ISAA>\\natural\       	put((char)247,FALSE,0);
-<ISAA>\\infty\         	put((char)248,FALSE,0);
-<ISAA>\\Box\           	put((char)249,FALSE,0);
-<ISAA>\\Diamond\       	put((char)250,FALSE,0);
-<ISAA>\\circ\          	put((char)251,FALSE,0);
-<ISAA>\\bullet\        	put((char)252,FALSE,0);
-<ISAA>\|\|             	put((char)253,FALSE,0);
-<ISAA>\\tick\          	put((char)254,FALSE,0);
-<ISAA>\\filter\        	put((char)255,FALSE,0);
+<ISAA>\ \             	put((char)160,FALSE,0);
+<ISAA>\\Gamma         	put((char)161,FALSE,0);
+<ISAA>\\Delta         	put((char)162,FALSE,0);
+<ISAA>\\Theta         	put((char)163,FALSE,0);
+<ISAA>LAM\            	put((char)164,FALSE,0);
+<ISAA>\\Pi            	put((char)165,FALSE,0);
+<ISAA>\\Sigma         	put((char)166,FALSE,0);
+<ISAA>\\Phi           	put((char)167,FALSE,0);
+<ISAA>\\Psi           	put((char)168,FALSE,0);
+<ISAA>\\Omega         	put((char)169,FALSE,0);
+<ISAA>'a              	put((char)170,FALSE,0);
+<ISAA>'b              	put((char)171,FALSE,0);
+<ISAA>'c              	put((char)172,FALSE,0);
+<ISAA>\\delta         	put((char)173,FALSE,0);
+<ISAA>\\varepsilon    	put((char)174,FALSE,0);
+<ISAA>\\zeta          	put((char)175,FALSE,0);
+<ISAA>\\eta           	put((char)176,FALSE,0);
+<ISAA>\\vartheta      	put((char)177,FALSE,0);
+<ISAA>\\kappa         	put((char)178,FALSE,0);
+<ISAA>%\              	put((char)179,FALSE,0);
+<ISAA>\\mu            	put((char)180,FALSE,0);
+<ISAA>\\nu            	put((char)181,FALSE,0);
+<ISAA>\\xi            	put((char)182,FALSE,0);
+<ISAA>\\pi            	put((char)183,FALSE,0);
+<ISAA>'r              	put((char)184,FALSE,0);
+<ISAA>'s              	put((char)185,FALSE,0);
+<ISAA>'t              	put((char)186,FALSE,0);
+<ISAA>\\varphi        	put((char)187,FALSE,0);
+<ISAA>\\chi           	put((char)188,FALSE,0);
+<ISAA>\\psi           	put((char)189,FALSE,0);
+<ISAA>\\omega         	put((char)190,FALSE,0);
+<ISAA>~\              	put((char)191,FALSE,0);
+<ISAA>&\              	put((char)192,FALSE,0);
+<ISAA>\|\             	put((char)193,FALSE,0);
+<ISAA>!\              	put((char)194,FALSE,0);
+<ISAA>\?\             	put((char)195,FALSE,0);
+<ISAA>!!              	put((char)196,FALSE,0);
+<ISAA>\\lceil         	put((char)197,FALSE,0);
+<ISAA>\\rceil         	put((char)198,FALSE,0);
+<ISAA>\\lfloor        	put((char)199,FALSE,0);
+<ISAA>\\rfloor        	put((char)200,FALSE,0);
+<ISAA>\|-             	put((char)201,FALSE,0);
+<ISAA>\|=             	put((char)202,FALSE,0);
+<ISAA>\[\|            	put((char)203,FALSE,0);
+<ISAA>\|\]            	put((char)204,FALSE,0);
+<ISAA>\\cdot          	put((char)205,FALSE,0);
+<ISAA>\ :\            	put((char)206,FALSE,0);
+<ISAA>\ \subseteq\    	put((char)207,FALSE,0);
+<ISAA>\ Int\          	put((char)208,FALSE,0);
+<ISAA>\ Un\           	put((char)209,FALSE,0);
+<ISAA>Inter\          	put((char)210,FALSE,0);
+<ISAA>Union\          	put((char)211,FALSE,0);
+<ISAA>\\sqcap         	put((char)212,FALSE,0);
+<ISAA>\\sqcup         	put((char)213,FALSE,0);
+<ISAA>glb\            	put((char)214,FALSE,0);
+<ISAA>LUB\            	put((char)215,FALSE,0);
+<ISAA>UU              	put((char)216,FALSE,0);
+<ISAA>===             	put((char)217,FALSE,0);
+<ISAA>==              	put((char)218,FALSE,0);
+<ISAA>~=              	put((char)219,FALSE,0);
+<ISAA>\\sqsubset      	put((char)220,FALSE,0);
+<ISAA><<              	put((char)221,FALSE,0);
+<ISAA><:              	put((char)222,FALSE,0);
+<ISAA><=:             	put((char)223,FALSE,0);
+<ISAA>:>              	put((char)224,FALSE,0);
+<ISAA>~~              	put((char)225,FALSE,0);
+<ISAA>\\sim\          	put((char)226,FALSE,0);
+<ISAA>\\simeq         	put((char)227,FALSE,0);
+<ISAA><=              	put((char)228,FALSE,0);
+<ISAA>::              	put((char)229,FALSE,0);
+<ISAA><-              	put((char)230,FALSE,0);
+<ISAA>-@@@@@          	put((char)231,FALSE,0);
+<ISAA>->              	put((char)232,FALSE,0);
+<ISAA>\\Leftarrow     	put((char)233,FALSE,0);
+<ISAA>=@@@@@          	put((char)234,FALSE,0);
+<ISAA>=>              	put((char)235,FALSE,0);
+<ISAA>\\frown         	put((char)236,FALSE,0);
+<ISAA>\\mapsto        	put((char)237,FALSE,0);
+<ISAA>\\leadsto       	put((char)238,FALSE,0);
+<ISAA>\\uparrow       	put((char)239,FALSE,0);
+<ISAA>\\downarrow     	put((char)240,FALSE,0);
+<ISAA>~:              	put((char)241,FALSE,0);
+<ISAA>\\times         	put((char)242,FALSE,0);
+<ISAA>\\oplus         	put((char)243,FALSE,0);
+<ISAA>\\ominus        	put((char)244,FALSE,0);
+<ISAA>\\otimes        	put((char)245,FALSE,0);
+<ISAA>\\oslash        	put((char)246,FALSE,0);
+<ISAA>\\subset        	put((char)247,FALSE,0);
+<ISAA>\\infty         	put((char)248,FALSE,0);
+<ISAA>\\Box           	put((char)249,FALSE,0);
+<ISAA>\\Diamond       	put((char)250,FALSE,0);
+<ISAA>\\circ          	put((char)251,FALSE,0);
+<ISAA>\\bullet        	put((char)252,FALSE,0);
+<ISAA>\|\|            	put((char)253,FALSE,0);
+<ISAA>\\tick          	put((char)254,FALSE,0);
+<ISAA>\\filter        	put((char)255,FALSE,0);
   /* END_OF_HI_TABLE */
   /* This is the end of the generated part */
 
   /* The following is generated by the perl script gen-isa2latex. */
   /* Make modifications in configuration file for gen-isa2latex!  */             
   /* BEGIN_OF_SEQ_TABLE */
-<ISA,ISAA>êë          	put((char)32,TRUE,0);
-<ISAA>==>         	put((char)32,TRUE,0);
-<ISA,ISAA>çè          	put((char)32,TRUE,1);
-<ISAA>-->         	put((char)32,TRUE,1);
-<ISA,ISAA>Ã!          	put((char)32,TRUE,2);
-<ISAA>\?!         	put((char)32,TRUE,2);
-<ISA,ISAA>ALL@@@@@    	put((char)32,TRUE,3);
-<ISAA>ALL\        	put((char)32,TRUE,3);
-<ISA,ISAA>EX@@@@@     	put((char)32,TRUE,4);
-<ISAA>EX\         	put((char)32,TRUE,4);
-<ISA,ISAA><\|@@@@@    	put((char)32,TRUE,5);
-<ISAA><\|         	put((char)32,TRUE,5);
-<ISA,ISAA><<\|@@@@@   	put((char)32,TRUE,6);
-<ISAA><<\|        	put((char)32,TRUE,6);
-<ISA,ISAA>éê          	put((char)32,TRUE,7);
-<ISAA><==         	put((char)32,TRUE,7);
-<ISA,ISAA>éë          	put((char)32,TRUE,8);
-<ISAA><=>         	put((char)32,TRUE,8);
-<ISA,ISAA>æç          	put((char)32,TRUE,9);
-<ISAA><--         	put((char)32,TRUE,9);
-<ISA,ISAA>æè          	put((char)32,TRUE,10);
-<ISAA><->         	put((char)32,TRUE,10);
+<ISA,ISAA>êë             	put((char)32,TRUE,0);
+<ISAA>==>                 	put((char)32,TRUE,0);
+<ISA,ISAA>çè             	put((char)32,TRUE,1);
+<ISAA>-->                 	put((char)32,TRUE,1);
+<ISA,ISAA>Ã!             	put((char)32,TRUE,2);
+<ISAA>\?!                 	put((char)32,TRUE,2);
+<ISA,ISAA>ALL@@@@@       	put((char)32,TRUE,3);
+<ISAA>ALL\                	put((char)32,TRUE,3);
+<ISA,ISAA>EX@@@@@        	put((char)32,TRUE,4);
+<ISAA>EX\                 	put((char)32,TRUE,4);
+<ISA,ISAA><<\|           	put((char)32,TRUE,5);
+<ISAA><<\|                	put((char)32,TRUE,5);
+<ISA,ISAA><\|            	put((char)32,TRUE,6);
+<ISAA><\|                 	put((char)32,TRUE,6);
+<ISA,ISAA>éê             	put((char)32,TRUE,7);
+<ISAA><==                 	put((char)32,TRUE,7);
+<ISA,ISAA>éë             	put((char)32,TRUE,8);
+<ISAA><=>                 	put((char)32,TRUE,8);
+<ISA,ISAA>æç             	put((char)32,TRUE,9);
+<ISAA><--                 	put((char)32,TRUE,9);
+<ISA,ISAA>æè             	put((char)32,TRUE,10);
+<ISAA><->                 	put((char)32,TRUE,10);
+<ISA,ISAA>\^-1           	put((char)32,TRUE,11);
+<ISAA>\^-1                	put((char)32,TRUE,11);
+<ISA,ISAA>arities        	put((char)32,TRUE,12);
+<ISAA>@arities            	put((char)32,TRUE,12);
+<ISA,ISAA>axclass        	put((char)32,TRUE,13);
+<ISAA>@axclass            	put((char)32,TRUE,13);
+<ISA,ISAA>constdefs      	put((char)32,TRUE,14);
+<ISAA>@constdefs          	put((char)32,TRUE,14);
+<ISA,ISAA>consts         	put((char)32,TRUE,15);
+<ISAA>@consts             	put((char)32,TRUE,15);
+<ISA,ISAA>datatype       	put((char)32,TRUE,16);
+<ISAA>@datatype           	put((char)32,TRUE,16);
+<ISA,ISAA>defs           	put((char)32,TRUE,17);
+<ISAA>@defs               	put((char)32,TRUE,17);
+<ISA,ISAA>domain         	put((char)32,TRUE,18);
+<ISAA>@domain             	put((char)32,TRUE,18);
+<ISA,ISAA>inductive      	put((char)32,TRUE,19);
+<ISAA>@inductive          	put((char)32,TRUE,19);
+<ISA,ISAA>instance       	put((char)32,TRUE,20);
+<ISAA>@instance           	put((char)32,TRUE,20);
+<ISA,ISAA>primrec        	put((char)32,TRUE,21);
+<ISAA>@primrec            	put((char)32,TRUE,21);
+<ISA,ISAA>recdef         	put((char)32,TRUE,22);
+<ISAA>@recdef             	put((char)32,TRUE,22);
+<ISA,ISAA>rules          	put((char)32,TRUE,23);
+<ISAA>@rules              	put((char)32,TRUE,23);
+<ISA,ISAA>translations   	put((char)32,TRUE,24);
+<ISAA>@translations       	put((char)32,TRUE,24);
+<ISA,ISAA>typedef        	put((char)32,TRUE,25);
+<ISAA>@typedef            	put((char)32,TRUE,25);
+<ISA,ISAA>types          	put((char)32,TRUE,26);
+<ISAA>@types              	put((char)32,TRUE,26);
   /* END_OF_SEQ_TABLE */
   /* This is the end of the generated part */
 
@@ -247,6 +284,8 @@
 void put(char c, int longDetect,int longCode)
 {
   int i;
+  char s[100];
+  extern char *translateHi(int ch, int code);
 
     if (YY_START == LATEX || YY_START == ESC)
         /* do not translate in these modes */ 
@@ -260,7 +299,12 @@
        }
     else /* lexer has not scanned a long sequence */		      
     if (c & 0x80) { /* Hi-bit is set... */
-       fprintf(foutput, "%s", translateHi(c, destCode));
+       strcpy(s, translateHi(c, destCode));
+       i = strlen(s);
+       if((unsigned char)c != 0xa0 &&
+	  i >= 2 && s[i-2] == '\\' && s[i-1] == ' ' && (yytext[0] & 0x80))
+	 s[i-2] ='\0';
+       fprintf(foutput, "%s", s);
         if (destCode == TO_LaTeX && ++cc % tabBlanks == 0)
           tabcount++;
     } 
diff -r c63f261fb025 -r 6b8bbcc9f05f src/Tools/8bit/c-sources/isa2latex/conv-main.c
--- a/src/Tools/8bit/c-sources/isa2latex/conv-main.c	Wed Nov 05 15:42:30 1997 +0100
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-main.c	Wed Nov 05 15:45:51 1997 +0100
@@ -45,7 +45,8 @@
 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_beg0[200],      /* latex command to begin isa environment */
+     isa_env_beg1[200];
 char isa_env_end[200];       /* latex command to end   isa environment */
 int cc;                      /* character counter in line  */
 int tabcount;                /* counter for tab positions  */
@@ -199,14 +200,17 @@
   if (convMode == STANDALONE) {
     if (use2e){
       fprintf(foutput, 
-	 "\\documentclass[a4paper,11pt]{article}\n");
+	 "\\documentclass[]{article}\n");
       fprintf(foutput, 
 	 "\\usepackage{latexsym,amssymb,isa2latex}\n");
     } else {
       fprintf(foutput, 
-	 "\\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article}\n");
+	 "\\documentstyle[10pt,latexsym,amssymb,isa2latex]{article}\n");
     }
-      fprintf(foutput, "\\begin{document}\n");
+      fprintf(foutput, "\\topmargin-8ex\n"
+	               "\\oddsidemargin0ex\n"
+	               "\\textheight158ex\n"
+	               "\\begin{document}\n");
   }
 
   if(texFont[0] != '\0') /* adjust font definition */
@@ -214,18 +218,21 @@
 
   /*
    * 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");
+  strcat(isa_env_beg, "\\kill{}\\hspace{-1.2ex}\n");
   strcpy(isa_env_end, "\n\\end{tabbing}}");
+   */
+  strcpy(isa_env_beg0, "{\\isabegin{}\\noindent ");
+  strcpy(isa_env_beg1, "{\\isabegin{\\isamodify}\\noindent ");
+  strcpy(isa_env_end , "\\isaend}\\noindent ");
   
-  if (convMode == STANDALONE || convMode == INCLUDE)
-    fprintf(foutput, isa_env_beg);
+  if (convMode == STANDALONE || (convMode == INCLUDE) && (destCode != TO_7bit))
+    fprintf(foutput, isa_env_beg0);
 
   /*
    * start the conversion: use lexer in all modes to do the job.
@@ -238,7 +245,7 @@
    * output footers
    */
 
-  if(convMode == STANDALONE || convMode == INCLUDE)
+  if(convMode == STANDALONE || (convMode == INCLUDE) && (destCode != TO_7bit))
     fprintf(foutput, isa_env_end);
 
   if(convMode == STANDALONE) 
diff -r c63f261fb025 -r 6b8bbcc9f05f src/Tools/8bit/c-sources/isa2latex/conv-tables.h
--- a/src/Tools/8bit/c-sources/isa2latex/conv-tables.h	Wed Nov 05 15:42:30 1997 +0100
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-tables.h	Wed Nov 05 15:45:51 1997 +0100
@@ -13,17 +13,17 @@
    "\\ ",
    "!",
    "\x22{}",
-   "\\#",
+   "\\mbox{$\\#$}",
    "\\$",
    "\\%",
-   "\\mbox{$\\&$}",
+   "\\&",
    "'",
-   "(",
-   ")",
-   "\\mbox{$*$}",
-   "\\mbox{$+$}",
+   "\\mbox{$($}",
+   "\\mbox{$)$}",
+   "{*}",
+   "+",
    ",",
-   "\\mbox{$-$}",
+   "-",
    ".",
    "/",
    "0",
@@ -70,10 +70,10 @@
    "Y",
    "Z",
    "\\mbox{$[$}",
-   "\\mbox{$\\backslash$}",
+   "\\ttbackslash{}",
    "\\mbox{$]$}",
    "\\^{}",
-   "\\_",
+   "{\\_\\hspace{.344ex}}",
    "`",
    "a",
    "b",
@@ -101,10 +101,10 @@
    "x",
    "y",
    "z",
-   "\\{",
-   "\\mbox{$|$}",
-   "\\}",
-   "\\~{}"
+   "\\mbox{$\\{$}",
+   "\\mbox{$\\mid$}",
+   "\\mbox{$\\}$}",
+   "\\tttilde{}"
 };
 /* END_OF_LOW_TABLE */
 
@@ -123,10 +123,11 @@
 
 /* BEGIN_OF_HI_TABLE */
 char *translationTableHi[END_HI_TABLE - START_HI_TABLE + 1][2] = {
+   {"  "           ,"\\ \\ "},
    {"\\Gamma"      ,"\\mbox{$\\Gamma$}"},
    {"\\Delta"      ,"\\mbox{$\\Delta$}"},
    {"\\Theta"      ,"\\mbox{$\\Theta$}"},
-   {"LAM"          ,"\\mbox{$\\Lambda$}"},
+   {"LAM "         ,"\\mbox{$\\Lambda$}"},
    {"\\Pi"         ,"\\mbox{$\\Pi$}"},
    {"\\Sigma"      ,"\\mbox{$\\Sigma$}"},
    {"\\Phi"        ,"\\mbox{$\\Phi$}"},
@@ -136,7 +137,7 @@
    {"'b"           ,"\\mbox{$\\beta$}"},
    {"'c"           ,"\\mbox{$\\gamma$}"},
    {"\\delta"      ,"\\mbox{$\\delta$}"},
-   {"\\varepsilon" ,"\\mbox{$\\varepsilon$}"},
+   {"@"            ,"\\mbox{$\\varepsilon$}"},
    {"\\zeta"       ,"\\mbox{$\\zeta$}"},
    {"\\eta"        ,"\\mbox{$\\eta$}"},
    {"\\vartheta"   ,"\\mbox{$\\vartheta$}"},
@@ -145,7 +146,7 @@
    {"\\mu"         ,"\\mbox{$\\mu$}"},
    {"\\nu"         ,"\\mbox{$\\nu$}"},
    {"\\xi"         ,"\\mbox{$\\xi$}"},
-   {"\\pi"         ,"\\mbox{$\\pi$}"},
+   {"\\p"          ,"\\mbox{$\\pi$}"},
    {"'r"           ,"\\mbox{$\\rho$}"},
    {"'s"           ,"\\mbox{$\\sigma$}"},
    {"'t"           ,"\\mbox{$\\tau$}"},
@@ -153,67 +154,67 @@
    {"\\chi"        ,"\\mbox{$\\chi$}"},
    {"\\psi"        ,"\\mbox{$\\psi$}"},
    {"\\omega"      ,"\\mbox{$\\omega$}"},
-   {"~"            ,"\\mbox{$\\neg$}"},
-   {"&"            ,"\\mbox{$\\wedge$}"},
-   {"|"            ,"\\mbox{$\\vee$}"},
-   {"!"            ,"\\mbox{$\\forall$}"},
-   {"?"            ,"\\mbox{$\\exists$}"},
+   {"~ "           ,"\\mbox{$\\neg$}"},
+   {"& "           ,"\\mbox{$\\hspace{-.185ex}\\wedge\\hspace{-.185ex}$}\\ "},
+   {"| "           ,"\\mbox{$\\hspace{-.185ex}\\vee\\hspace{-.185ex}$}\\ "},
+   {"!"            ,"\\mbox{$\\hspace{-.07ex}\\forall$}"},
+   {"? "           ,"\\mbox{$\\hspace{-.07ex}\\exists$}"},
    {"!!"           ,"\\mbox{$\\bigwedge$}"},
    {"\\lceil"      ,"\\mbox{$\\lceil$}"},
    {"\\rceil"      ,"\\mbox{$\\rceil$}"},
    {"\\lfloor"     ,"\\mbox{$\\lfloor$}"},
    {"\\rfloor"     ,"\\mbox{$\\rfloor$}"},
-   {"(|"           ,"\\mbox{$(\\!|$}"},
-   {"|)"           ,"\\mbox{$|\\!)$}"},
-   {"[|"           ,"\\mbox{$[\\![$}"},
-   {"|]"           ,"\\mbox{$]\\!]$}"},
-   {"\\emptyset"   ,"\\mbox{$\\emptyset$}"},
-   {":"            ,"\\mbox{$\\in$}"},
-   {"\\subseteq"   ,"\\mbox{$\\subseteq$}"},
-   {"Int"          ,"\\mbox{$\\cap$}"},
-   {"Un"           ,"\\mbox{$\\cup$}"},
-   {"Inter"        ,"\\mbox{$\\bigcap$}"},
-   {"Union"        ,"\\mbox{$\\bigcup$}"},
-   {"\\sqcap"      ,"\\mbox{$\\sqcap$}"},
-   {"\\sqcup"      ,"\\mbox{$\\sqcup$}"},
-   {"glb"          ,"\\mbox{$\\overline{|\\,\\,|}$}"},
-   {"lub"          ,"\\mbox{$\\bigsqcup$}"},
-   {"UU"           ,"\\mbox{$\\perp$}"},
-   {"==="          ,"\\mbox{$\\doteq$}"},
-   {"=="           ,"\\mbox{$\\equiv$}"},
+   {"|-"           ,"\\mbox{$\\hspace{.49ex}\\vdash\\hspace{.49ex}$}"},
+   {"|="           ,"\\mbox{$\\models$}"},
+   {"[|"           ,"\\mbox{$[\\![\\hspace{.32ex}$}"},
+   {"|]"           ,"\\mbox{$\\hspace{.32ex}]\\!]$}"},
+   {"\\cdot"       ,"\\mbox{$\\hspace{.28ex}\\cdot\\hspace{.28ex}$}"},
+   {":"            ,"\\hspace{.1ex}\\mbox{$\\in$}\\hspace{.1ex}"},
+   {" \\subseteq " ,"\\mbox{$\\subseteq$}"},
+   {" Int "        ,"\\mbox{$\\cap$}"},
+   {" Un "         ,"\\mbox{$\\cup$}"},
+   {"Inter "       ,"\\mbox{$\\bigcap$}"},
+   {"Union "       ,"\\mbox{$\\bigcup$}"},
+   {"\\sqcap"      ,"\\mbox{$\\hspace{.29ex}\\sqcap\\hspace{.29ex}$}"},
+   {"\\sqcup"      ,"\\mbox{$\\hspace{.29ex}\\sqcup\\hspace{.29ex}$}"},
+   {"glb "         ,"\\mbox{$\\overline{|\\,\\,|}$}"},
+   {"LUB "         ,"\\mbox{$\\bigsqcup$}"},
+   {"UU"           ,"\\mbox{$\\bot$}"},
+   {".="           ,"\\mbox{$\\doteq$}"},
+   {"=="           ,"\\mbox{$\\hspace{.29ex}\\equiv\\hspace{.29ex}$}"},
    {"~="           ,"\\mbox{$\\not=$}"},
-   {"\\sqsubset"   ,"\\mbox{$\\sqsubset$}"},
-   {"<<"           ,"\\mbox{$\\sqsubseteq$}"},
-   {"\\prec"       ,"\\mbox{$\\prec$}"},
-   {"\\preceq"     ,"\\mbox{$\\preceq$}"},
-   {"\\succ"       ,"\\mbox{$\\succ$}"},
-   {"\\succeq"     ,"\\mbox{$\\succeq$}"},
-   {"\\sim"        ,"\\mbox{$\\sim$}"},
-   {"\\simeq"      ,"\\mbox{$\\simeq$}"},
-   {"\\le"         ,"\\mbox{$\\le$}"},
-   {"\\ge"         ,"\\mbox{$\\ge$}"},
+   {"\\sqsubset"   ,"\\mbox{$\\hspace{.29ex}\\sqsubset\\hspace{.29ex}$}"},
+   {"<<"           ,"\\mbox{$\\hspace{.29ex}\\sqsubseteq\\hspace{.29ex}$}"},
+   {"<:"           ,"\\mbox{$\\hspace{.29ex}\\prec\\hspace{.29ex}$}\\ "},
+   {"<=:"          ,"\\mbox{$\\hspace{.29ex}\\preceq\\hspace{.29ex}$}"},
+   {":>"           ,"\\mbox{$\\hspace{.29ex}\\succ\\hspace{.29ex}$}\\ "},
+   {"~~"           ,"\\mbox{$\\hspace{.29ex}\\approx\\hspace{.29ex}$}"},
+   {"\\sim "       ,"\\mbox{$\\hspace{.29ex}\\sim\\hspace{.29ex}$}\\ "},
+   {"\\simeq"      ,"\\mbox{$\\hspace{.29ex}\\simeq\\hspace{.29ex}$}"},
+   {"<="           ,"\\mbox{$\\hspace{.29ex}\\le\\hspace{.29ex}$}"},
+   {"::"           ,"\\mbox{$\\hspace{-.1ex}:\\hspace{-.07ex}:\\hspace{.1ex}$}"},
    {"<-"           ,"\\mbox{$\\leftarrow$}"},
    {"-"            ,"\\mbox{$-$}"},
    {"->"           ,"\\mbox{$\\rightarrow$}"},
    {"<="           ,"\\mbox{$\\Leftarrow$}"},
    {"="            ,"\\mbox{$=$}"},
-   {"=>"           ,"\\mbox{$\\Rightarrow$}"},
-   {"->>"          ,"\\mbox{$\\twoheadrightarrow$}"},
-   {"\\mapsto"     ,"\\mbox{$\\mapsto$}"},
-   {"\\leadsto"    ,"\\mbox{$\\leadsto$}"},
+   {"=>"           ,"\\mbox{$\\hspace{.12ex}\\Rightarrow$}"},
+   {"\\frown"      ,"\\mbox{$\\frown$}"},
+   {"|->"          ,"\\mbox{$\\mapsto$}"},
+   {"~>"           ,"\\mbox{$\\hspace{.05ex}\\leadsto$}"},
    {"\\uparrow"    ,"\\mbox{$\\uparrow$}"},
    {"\\downarrow"  ,"\\mbox{$\\downarrow$}"},
    {"~:"           ,"\\mbox{$\\notin$}"},
-   {"*"            ,"\\mbox{$\\times$}"},
-   {"++"           ,"\\mbox{$\\oplus$}"},
-   {"\\ominus"     ,"\\mbox{$\\ominus$}"},
-   {"**"           ,"\\mbox{$\\otimes$}"},
-   {"\\oslash"     ,"\\mbox{$\\oslash$}"},
-   {"\\natural"    ,"\\mbox{$\\natural$}"},
+   {"*"            ,"\\mbox{$\\hspace{-.29ex}\\times\\hspace{-.29ex}$}"},
+   {"++"           ,"\\mbox{$\\hspace{.29ex}\\oplus\\hspace{.29ex}$}"},
+   {"--"           ,"\\mbox{$\\hspace{.29ex}\\ominus\\hspace{.29ex}$}"},
+   {"**"           ,"\\mbox{$\\hspace{.29ex}\\otimes\\hspace{.29ex}$}"},
+   {"//"           ,"\\mbox{$\\hspace{.29ex}\\oslash\\hspace{.29ex}$}"},
+   {"\\subset"     ,"\\mbox{$\\subset$}"},
    {"\\infty"      ,"\\mbox{$\\infty$}"},
    {"\\Box"        ,"\\mbox{$\\Box$}"},
-   {"\\Diamond"    ,"\\mbox{$\\Diamond$}"},
-   {"\\circ"       ,"\\mbox{$\\circ$}"},
+   {"<>"           ,"\\mbox{$\\hspace{.29ex}\\Diamond\\hspace{.29ex}$}"},
+   {" o "          ,"\\mbox{$\\circ$}"},
    {"\\bullet"     ,"\\mbox{$\\bullet$}"},
    {"||"           ,"\\mbox{$\\parallel$}"},
    {"\\tick"       ,"\\mbox{$\\surd$}"},
@@ -236,17 +237,33 @@
 
 /* BEGIN_OF_SEQ_TABLE */
 char *translationTableSeq[SEQ_TABLE][2] = {
-   {"==>"                        ,"\\mbox{$\\Longrightarrow$}"},
-   {"-->"                        ,"\\mbox{$\\longrightarrow$}"},
-   {"?!"                         ,"\\mbox{$\\exists$}!"},
-   {"ALL"                        ,"\\mbox{$\\forall$}"},
-   {"EX"                         ,"\\mbox{$\\exists$}"},
-   {"<|"                         ,"\\mbox{$<\\!\\mid$}"},
-   {"<<|"                        ,"\\mbox{$\\ll\\!\\mid$}"},
-   {"<=="                        ,"\\mbox{$\\Longleftarrow$}"},
-   {"<=>"                        ,"\\mbox{$\\Leftrightarrow$}"},
-   {"<--"                        ,"\\mbox{$\\longleftarrow$}"},
-   {"<->"                        ,"\\mbox{$\\leftrightarrow$}"}
+   {"==>"                                         ,"\\mbox{$\\hspace{-.083ex}\\Longrightarrow$}"},
+   {"-->"                                         ,"\\mbox{$\\longrightarrow$}"},
+   {"?!"                                          ,"\\mbox{$\\exists_1$}"},
+   {"ALL "                                        ,"\\mbox{$\\forall$}"},
+   {"EX "                                         ,"\\mbox{$\\exists$}"},
+   {"<<|"                                         ,"\\mbox{$\\ll\\!\\mid$}"},
+   {"<|"                                          ,"\\mbox{$<\\!\\mid$}"},
+   {"<=="                                         ,"\\mbox{$\\Longleftarrow$}"},
+   {"<=>"                                         ,"\\mbox{$\\Leftrightarrow$}"},
+   {"<--"                                         ,"\\mbox{$\\longleftarrow$}"},
+   {"<->"                                         ,"\\mbox{$\\leftrightarrow$}"},
+   {"^-1"                                         ,"\\mbox{$^{\\tt -1}$}"},
+   {"arities"                                     ,"\\mbox{\\bf arities}"},
+   {"axclass"                                     ,"\\mbox{\\bf axclass}"},
+   {"constdefs"                                   ,"\\mbox{\\bf constdefs}"},
+   {"consts"                                      ,"\\mbox{\\bf consts}"},
+   {"datatype"                                    ,"\\mbox{\\bf datatype}"},
+   {"defs"                                        ,"\\mbox{\\bf defs}"},
+   {"domain"                                      ,"\\mbox{\\bf domain}"},
+   {"inductive"                                   ,"\\mbox{\\bf inductive}"},
+   {"instance"                                    ,"\\mbox{\\bf instance}"},
+   {"primrec"                                     ,"\\mbox{\\bf primrec}"},
+   {"recdef"                                      ,"\\mbox{\\bf recdef}"},
+   {"rules"                                       ,"\\mbox{\\bf rules}"},
+   {"translations"                                ,"\\mbox{\\bf translations}"},
+   {"typedef"                                     ,"\\mbox{\\bf typedef}"},
+   {"types"                                       ,"\\mbox{\\bf types}"}
 };
 /* END_OF_SEQ_TABLE */
 
diff -r c63f261fb025 -r 6b8bbcc9f05f src/Tools/8bit/c-sources/isa2latex/isa2latex
Binary file src/Tools/8bit/c-sources/isa2latex/isa2latex has changed