# HG changeset patch
# User oheimb
# Date 891590088 -7200
# Node ID b6729feb8a5d47b01a84e946f17bcd62c28c354c
# Parent  8c7e7eaffbdfc2b6f16f01a436456a3beb339ae9
improved \tt appearance of many ASCII special symbols like #
isabelle theory file keywords now appear bold only when at begin of line

diff -r 8c7e7eaffbdf -r b6729feb8a5d src/Tools/8bit/c-sources/isa2latex/conv-defs.h
--- a/src/Tools/8bit/c-sources/isa2latex/conv-defs.h	Thu Apr 02 17:19:02 1998 +0200
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-defs.h	Fri Apr 03 09:54:48 1998 +0200
@@ -56,6 +56,6 @@
 #define END_LOW_TABLE   126
 #define START_HI_TABLE  160
 #define END_HI_TABLE    255
-#define SEQ_TABLE       27
+#define SEQ_TABLE       28
 /* END gen-isa2latex */
 
diff -r 8c7e7eaffbdf -r b6729feb8a5d src/Tools/8bit/c-sources/isa2latex/conv-lex.x
--- a/src/Tools/8bit/c-sources/isa2latex/conv-lex.x	Thu Apr 02 17:19:02 1998 +0200
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-lex.x	Fri Apr 03 09:54:48 1998 +0200
@@ -202,60 +202,62 @@
   /* 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>\^-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);
+<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>^arities        	put((char)32,TRUE,11);
+<ISAA>^@arities            	put((char)32,TRUE,11);
+<ISA,ISAA>^axclass        	put((char)32,TRUE,12);
+<ISAA>^@axclass            	put((char)32,TRUE,12);
+<ISA,ISAA>^constdefs      	put((char)32,TRUE,13);
+<ISAA>^@constdefs          	put((char)32,TRUE,13);
+<ISA,ISAA>^consts         	put((char)32,TRUE,14);
+<ISAA>^@consts             	put((char)32,TRUE,14);
+<ISA,ISAA>^datatype       	put((char)32,TRUE,15);
+<ISAA>^@datatype           	put((char)32,TRUE,15);
+<ISA,ISAA>^defs           	put((char)32,TRUE,16);
+<ISAA>^@defs               	put((char)32,TRUE,16);
+<ISA,ISAA>^domain         	put((char)32,TRUE,17);
+<ISAA>^@domain             	put((char)32,TRUE,17);
+<ISA,ISAA>^end            	put((char)32,TRUE,18);
+<ISAA>^@end                	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>^syntax         	put((char)32,TRUE,24);
+<ISAA>^@syntax             	put((char)32,TRUE,24);
+<ISA,ISAA>^translations   	put((char)32,TRUE,25);
+<ISAA>^@translations       	put((char)32,TRUE,25);
+<ISA,ISAA>^typedef        	put((char)32,TRUE,26);
+<ISAA>^@typedef            	put((char)32,TRUE,26);
+<ISA,ISAA>^types          	put((char)32,TRUE,27);
+<ISAA>^@types              	put((char)32,TRUE,27);
   /* END_OF_SEQ_TABLE */
   /* This is the end of the generated part */
 
diff -r 8c7e7eaffbdf -r b6729feb8a5d src/Tools/8bit/c-sources/isa2latex/conv-tables.h
--- a/src/Tools/8bit/c-sources/isa2latex/conv-tables.h	Thu Apr 02 17:19:02 1998 +0200
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-tables.h	Fri Apr 03 09:54:48 1998 +0200
@@ -13,13 +13,13 @@
    "\\ ",
    "!",
    "\x22{}",
-   "\\mbox{$\\#$}",
+   "\\#",
    "\\$",
    "\\%",
    "\\&",
    "'",
-   "\\mbox{$($}",
-   "\\mbox{$)$}",
+   "(",
+   ")",
    "{*}",
    "+",
    ",",
@@ -38,9 +38,9 @@
    "9",
    ":",
    ";",
-   "\\mbox{$<$}",
-   "\\mbox{$=$}",
-   "\\mbox{$>$}",
+   "<",
+   "=",
+   ">",
    "?",
    "@",
    "A",
@@ -69,9 +69,9 @@
    "X",
    "Y",
    "Z",
-   "\\mbox{$[$}",
+   "[",
    "\\ttbackslash{}",
-   "\\mbox{$]$}",
+   "]",
    "\\^{}",
    "{\\_\\hspace{.344ex}}",
    "`",
@@ -101,9 +101,9 @@
    "x",
    "y",
    "z",
-   "\\mbox{$\\{$}",
-   "\\mbox{$\\mid$}",
-   "\\mbox{$\\}$}",
+   "\\{",
+   "|",
+   "\\}",
    "\\tttilde{}"
 };
 /* END_OF_LOW_TABLE */
@@ -168,13 +168,13 @@
    {"|="           ,"\\mbox{$\\models$}"},
    {"[|"           ,"\\mbox{$[\\![\\hspace{.32ex}$}"},
    {"|]"           ,"\\mbox{$\\hspace{.32ex}]\\!]$}"},
-   {"\\cdot"       ,"\\mbox{$\\hspace{.28ex}\\cdot\\hspace{.28ex}$}"},
+   {"."            ,"\\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$}"},
+   {"INT "         ,"\\mbox{$\\bigcap$}"},
+   {"UN "          ,"\\mbox{$\\bigcup$}"},
    {"\\sqcap"      ,"\\mbox{$\\hspace{.29ex}\\sqcap\\hspace{.29ex}$}"},
    {"\\sqcup"      ,"\\mbox{$\\hspace{.29ex}\\sqcup\\hspace{.29ex}$}"},
    {"glb "         ,"\\mbox{$\\overline{|\\,\\,|}$}"},
@@ -192,7 +192,7 @@
    {"\\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{$:\\hspace{-.07ex}:$}"},
    {"<-"           ,"\\mbox{$\\leftarrow$}"},
    {"-"            ,"\\mbox{$-$}"},
    {"->"           ,"\\mbox{$\\rightarrow$}"},
@@ -248,7 +248,6 @@
    {"<=>"                                         ,"\\mbox{$\\Leftrightarrow$}"},
    {"<--"                                         ,"\\mbox{$\\longleftarrow$}"},
    {"<->"                                         ,"\\mbox{$\\leftrightarrow$}"},
-   {"^-1"                                         ,"\\mbox{$^{\\tt -1}$}"},
    {"arities"                                     ,"\\mbox{\\bf arities}"},
    {"axclass"                                     ,"\\mbox{\\bf axclass}"},
    {"constdefs"                                   ,"\\mbox{\\bf constdefs}"},
@@ -256,11 +255,13 @@
    {"datatype"                                    ,"\\mbox{\\bf datatype}"},
    {"defs"                                        ,"\\mbox{\\bf defs}"},
    {"domain"                                      ,"\\mbox{\\bf domain}"},
+   {"end"                                         ,"\\mbox{\\bf end}"},
    {"inductive"                                   ,"\\mbox{\\bf inductive}"},
    {"instance"                                    ,"\\mbox{\\bf instance}"},
    {"primrec"                                     ,"\\mbox{\\bf primrec}"},
    {"recdef"                                      ,"\\mbox{\\bf recdef}"},
    {"rules"                                       ,"\\mbox{\\bf rules}"},
+   {"syntax"                                      ,"\\mbox{\\bf syntax}"},
    {"translations"                                ,"\\mbox{\\bf translations}"},
    {"typedef"                                     ,"\\mbox{\\bf typedef}"},
    {"types"                                       ,"\\mbox{\\bf types}"}
diff -r 8c7e7eaffbdf -r b6729feb8a5d src/Tools/8bit/config/conv-tables.inp
--- a/src/Tools/8bit/config/conv-tables.inp	Thu Apr 02 17:19:02 1998 +0200
+++ b/src/Tools/8bit/config/conv-tables.inp	Fri Apr 03 09:54:48 1998 +0200
@@ -86,13 +86,13 @@
 #>  "\\x22{}"		double quotes are not removed 
 >  "\x22{}"		double quotes are not removed 
 #
->  "\mbox{$\#$}"
+>  "\#"
 >  "\$"
 >  "\%"
 >  "\&"
 >  "'"
->  "\mbox{$($}"
->  "\mbox{$)$}"
+>  "("
+>  ")"
 >  "{*}"
 >  "+"
 >  ","
@@ -111,9 +111,9 @@
 >  "9"
 >  ":"
 >  ";"
->  "\mbox{$<$}"
->  "\mbox{$=$}"
->  "\mbox{$>$}"
+>  "<"
+>  "="
+>  ">"
 >  "?"
 >  "@"
 >  "A"
@@ -142,9 +142,9 @@
 >  "X"
 >  "Y"
 >  "Z"
->  "\mbox{$[$}"
+>  "["
 >  "\ttbackslash{}" #?????
->  "\mbox{$]$}"
+>  "]"
 >  "\^{}"			
 >  "{\_\hspace{.344ex}}"
 >  "`"
@@ -174,9 +174,9 @@
 >  "x"
 >  "y"
 >  "z"
->  "\mbox{$\{$}" #"\ttlbrace{}"
->  "\mbox{$\mid$}"
->  "\mbox{$\}$}" #"\ttrbrace{}"
+>  "\{" #"\ttlbrace{}"
+>  "|"
+>  "\}" #"\ttrbrace{}"
 >  "\tttilde{}"
 END_LOW_TABLE
 
@@ -398,32 +398,34 @@
 >  "EX@@@@@"	"EX\ "		"EX "		"\mbox{$\exists$}" 
 
 #HOLCF
->  "<<\|"	"<<\|"		"<<|"		"\mbox{$\ll\!\mid$}"
->  "<\|"	"<\|"		"<|"		"\mbox{$<\!\mid$}"
+>  "<<\|"	"@<<\|"		"<<|"		"\mbox{$\ll\!\mid$}"
+>  "<\|"	"@<\|"		"<|"		"\mbox{$<\!\mid$}"
 
 # misc ?
 >  "éê"		"<=="		"<=="		"\mbox{$\Longleftarrow$}"
 >  "éë"		"<=>"		"<=>"		"\mbox{$\Leftrightarrow$}"
 >  "æç"		"<--"		"<--"		"\mbox{$\longleftarrow$}"
 >  "æè"		"<->"		"<->"		"\mbox{$\leftrightarrow$}"
->  "\^-1"	"\^-1"		"^-1"		"\mbox{$^{\tt -1}$}" 
+#>  "\^-1"	"@\^-1"		"^-1"		"\mbox{$^{\tt -1}$}" 
 
 #Isabelle
->  "arities"	"@arities"	"arities"	"\mbox{\bf arities}"
->  "axclass"	"@axclass"	"axclass"	"\mbox{\bf axclass}"
->  "constdefs"	"@constdefs"	"constdefs"	"\mbox{\bf constdefs}"
->  "consts"	"@consts"	"consts"	"\mbox{\bf consts}"
->  "datatype"	"@datatype"	"datatype"	"\mbox{\bf datatype}"
->  "defs"	"@defs"		"defs"		"\mbox{\bf defs}"
->  "domain"	"@domain"	"domain"	"\mbox{\bf domain}"
->  "inductive"	"@inductive"	"inductive"	"\mbox{\bf inductive}"
->  "instance"	"@instance"	"instance"	"\mbox{\bf instance}"
->  "primrec"	"@primrec"	"primrec"	"\mbox{\bf primrec}"
->  "recdef"	"@recdef"	"recdef"	"\mbox{\bf recdef}"
->  "rules"	"@rules"	"rules"		"\mbox{\bf rules}"
->  "translations""@translations""translations"	"\mbox{\bf translations}"
->  "typedef"	"@typedef"	"typedef"	"\mbox{\bf typedef}"
->  "types"	"@types"	"types"		"\mbox{\bf types}"
+>  "^arities"	"^@arities"	"arities"	"\mbox{\bf arities}"
+>  "^axclass"	"^@axclass"	"axclass"	"\mbox{\bf axclass}"
+>  "^constdefs"	"^@constdefs"	"constdefs"	"\mbox{\bf constdefs}"
+>  "^consts"	"^@consts"	"consts"	"\mbox{\bf consts}"
+>  "^datatype"	"^@datatype"	"datatype"	"\mbox{\bf datatype}"
+>  "^defs"	"^@defs"	"defs"		"\mbox{\bf defs}"
+>  "^domain"	"^@domain"	"domain"	"\mbox{\bf domain}"
+>  "^end"	"^@end"		"end"		"\mbox{\bf end}"
+>  "^inductive"	"^@inductive"	"inductive"	"\mbox{\bf inductive}"
+>  "^instance"	"^@instance"	"instance"	"\mbox{\bf instance}"
+>  "^primrec"	"^@primrec"	"primrec"	"\mbox{\bf primrec}"
+>  "^recdef"	"^@recdef"	"recdef"	"\mbox{\bf recdef}"
+>  "^rules"	"^@rules"	"rules"		"\mbox{\bf rules}"
+>  "^syntax"	"^@syntax"	"syntax"	"\mbox{\bf syntax}"
+>  "^translations""^@translations""translations""\mbox{\bf translations}"
+>  "^typedef"	"^@typedef"	"typedef"	"\mbox{\bf typedef}"
+>  "^types"	"^@types"	"types"		"\mbox{\bf types}"
 END_SEQ_TABLE