src/Tools/8bit/c-sources/isa2latex/conv-tables.h
author paulson
Tue, 05 Sep 2000 10:16:03 +0200
changeset 9841 ca3173f87b5c
parent 6026 649b98cf9bc3
permissions -rw-r--r--
safe_meson_tac -> meson_tac
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     1
/*
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     2
 * translation table for the low-8-bit ascii codes
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     3
 * translation takes place only if destCode is TO_LaTeX
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     4
 *
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     5
 * the row number + START_LOW_TABLE -1 is the ascii code !!
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     6
 */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     7
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     8
/* do not edit the lines between BEGIN_OF_LOW_TABLE and END_OF_LOW_TABLE  */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     9
/* these lines are automatically generated by gen-isa2latex               */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    10
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    11
/* BEGIN_OF_LOW_TABLE */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    12
char *translationTableLow[END_LOW_TABLE - START_LOW_TABLE + 1] = {
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    13
   "\\ ",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    14
   "!",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    15
   "\x22{}",
4773
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
    16
   "\\#",
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    17
   "\\$",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    18
   "\\%",
4170
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
    19
   "\\&",
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    20
   "'",
4773
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
    21
   "(",
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
    22
   ")",
4170
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
    23
   "{*}",
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
    24
   "+",
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    25
   ",",
4170
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
    26
   "-",
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    27
   ".",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    28
   "/",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    29
   "0",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    30
   "1",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    31
   "2",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    32
   "3",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    33
   "4",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    34
   "5",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    35
   "6",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    36
   "7",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    37
   "8",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    38
   "9",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    39
   ":",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    40
   ";",
4773
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
    41
   "<",
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
    42
   "=",
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
    43
   ">",
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    44
   "?",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    45
   "@",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    46
   "A",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    47
   "B",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    48
   "C",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    49
   "D",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    50
   "E",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    51
   "F",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    52
   "G",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    53
   "H",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    54
   "I",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    55
   "J",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    56
   "K",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    57
   "L",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    58
   "M",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    59
   "N",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    60
   "O",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    61
   "P",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    62
   "Q",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    63
   "R",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    64
   "S",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    65
   "T",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    66
   "U",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    67
   "V",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    68
   "W",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    69
   "X",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    70
   "Y",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    71
   "Z",
4773
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
    72
   "[",
4170
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
    73
   "\\ttbackslash{}",
4773
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
    74
   "]",
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    75
   "\\^{}",
4170
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
    76
   "{\\_\\hspace{.344ex}}",
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    77
   "`",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    78
   "a",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    79
   "b",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    80
   "c",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    81
   "d",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    82
   "e",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    83
   "f",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    84
   "g",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    85
   "h",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    86
   "i",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    87
   "j",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    88
   "k",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    89
   "l",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    90
   "m",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    91
   "n",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    92
   "o",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    93
   "p",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    94
   "q",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    95
   "r",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    96
   "s",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    97
   "t",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    98
   "u",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    99
   "v",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   100
   "w",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   101
   "x",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   102
   "y",
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   103
   "z",
4773
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
   104
   "\\{",
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
   105
   "|",
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
   106
   "\\}",
4170
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   107
   "\\tttilde{}"
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   108
};
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   109
/* END_OF_LOW_TABLE */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   110
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   111
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   112
/*
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   113
 * conversion table for Hi-8-bit table
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   114
 *
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   115
 * the row number + START_HIGH_TABLE -1 is the ascii code !!
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   116
 * 
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   117
 * first  column is used if destCode is TO_7bit
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   118
 * second column is used if destCode is TO_LaTeX
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   119
 */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   120
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   121
/* do not edit the lines between BEGIN_OF_HI_TABLE and END_OF_HI_TABLE  */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   122
/* these lines are automatically generated by gen-isa2latex             */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   123
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   124
/* BEGIN_OF_HI_TABLE */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   125
char *translationTableHi[END_HI_TABLE - START_HI_TABLE + 1][2] = {
4826
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   126
   {"  "          ,"\\ \\ "},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   127
   {"\\Gamma"     ,"\\mbox{$\\Gamma$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   128
   {"\\Delta"     ,"\\mbox{$\\Delta$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   129
   {"\\Theta"     ,"\\mbox{$\\Theta$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   130
   {"LAM "        ,"\\mbox{$\\Lambda$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   131
   {"\\Pi"        ,"\\mbox{$\\Pi$}"},
6026
649b98cf9bc3 better representation of Sigma
oheimb
parents: 5675
diff changeset
   132
   {"SIGMA"       ,"\\mbox{$\\Sigma$}"},
4826
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   133
   {"\\Phi"       ,"\\mbox{$\\Phi$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   134
   {"\\Psi"       ,"\\mbox{$\\Psi$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   135
   {"\\Omega"     ,"\\mbox{$\\Omega$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   136
   {"'a"          ,"\\mbox{$\\alpha$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   137
   {"'b"          ,"\\mbox{$\\beta$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   138
   {"'c"          ,"\\mbox{$\\gamma$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   139
   {"\\delta"     ,"\\mbox{$\\delta$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   140
   {"@"           ,"\\mbox{$\\varepsilon$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   141
   {"\\zeta"      ,"\\mbox{$\\zeta$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   142
   {"\\eta"       ,"\\mbox{$\\eta$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   143
   {"\\vartheta"  ,"\\mbox{$\\vartheta$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   144
   {"\\kappa"     ,"\\mbox{$\\kappa$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   145
   {"%"           ,"\\mbox{$\\lambda$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   146
   {"\\mu"        ,"\\mbox{$\\mu$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   147
   {"\\nu"        ,"\\mbox{$\\nu$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   148
   {"\\xi"        ,"\\mbox{$\\xi$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   149
   {"\\p"         ,"\\mbox{$\\pi$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   150
   {"'r"          ,"\\mbox{$\\rho$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   151
   {"'s"          ,"\\mbox{$\\sigma$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   152
   {"'t"          ,"\\mbox{$\\tau$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   153
   {"\\varphi"    ,"\\mbox{$\\varphi$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   154
   {"\\chi"       ,"\\mbox{$\\chi$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   155
   {"\\psi"       ,"\\mbox{$\\psi$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   156
   {"\\omega"     ,"\\mbox{$\\omega$}"},
5436
cff7d1e98376 improved spacing
oheimb
parents: 4826
diff changeset
   157
   {"~ "          ,"\\mbox{$\\hspace{-.33ex}\\neg$}"},
4826
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   158
   {"& "          ,"\\mbox{$\\hspace{-.185ex}\\wedge\\hspace{-.185ex}$}\\ "},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   159
   {"| "          ,"\\mbox{$\\hspace{-.185ex}\\vee\\hspace{-.185ex}$}\\ "},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   160
   {"!"           ,"\\mbox{$\\hspace{-.07ex}\\forall$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   161
   {"? "          ,"\\mbox{$\\hspace{-.07ex}\\exists$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   162
   {"!!"          ,"\\mbox{$\\bigwedge$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   163
   {"\\lceil"     ,"\\mbox{$\\lceil$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   164
   {"\\rceil"     ,"\\mbox{$\\rceil$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   165
   {"\\lfloor"    ,"\\mbox{$\\lfloor$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   166
   {"\\rfloor"    ,"\\mbox{$\\rfloor$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   167
   {"|-"          ,"\\mbox{$\\hspace{.49ex}\\vdash\\hspace{.49ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   168
   {"|="          ,"\\mbox{$\\models$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   169
   {"[|"          ,"\\mbox{$[\\![\\hspace{.32ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   170
   {"|]"          ,"\\mbox{$\\hspace{.32ex}]\\!]$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   171
   {"."           ,"\\mbox{$\\hspace{.28ex}\\cdot\\hspace{.28ex}$}"},
5436
cff7d1e98376 improved spacing
oheimb
parents: 4826
diff changeset
   172
   {":"           ,"\\mbox{$\\hspace{.445ex}\\in\\hspace{.445ex}$}"},
4826
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   173
   {" <= "        ,"\\mbox{$\\subseteq$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   174
   {" Int "       ,"\\mbox{$\\cap$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   175
   {" Un "        ,"\\mbox{$\\cup$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   176
   {"INT "        ,"\\mbox{$\\bigcap$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   177
   {"UN "         ,"\\mbox{$\\bigcup$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   178
   {"\\sqcap"     ,"\\mbox{$\\hspace{.29ex}\\sqcap\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   179
   {"\\sqcup"     ,"\\mbox{$\\hspace{.29ex}\\sqcup\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   180
   {"glb "        ,"\\mbox{$\\overline{|\\,\\,|}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   181
   {"LUB "        ,"\\mbox{$\\bigsqcup$}"},
5436
cff7d1e98376 improved spacing
oheimb
parents: 4826
diff changeset
   182
   {"UU"          ,"\\mbox{$\\hspace{-.29ex}\\bot\\hspace{-.29ex}$}"},
4826
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   183
   {".="          ,"\\mbox{$\\doteq$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   184
   {"=="          ,"\\mbox{$\\hspace{.29ex}\\equiv\\hspace{.29ex}$}"},
5436
cff7d1e98376 improved spacing
oheimb
parents: 4826
diff changeset
   185
   {"~="          ,"\\mbox{$\\hspace{-.34ex}\\not\\hspace{-.3ex}\\mbox{=}$}"},
4826
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   186
   {"\\sqsubset"  ,"\\mbox{$\\hspace{.29ex}\\sqsubset\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   187
   {"<<"          ,"\\mbox{$\\hspace{.29ex}\\sqsubseteq\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   188
   {"<:"          ,"\\mbox{$\\hspace{.29ex}\\prec\\hspace{.29ex}$}\\ "},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   189
   {"<=:"         ,"\\mbox{$\\hspace{.29ex}\\preceq\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   190
   {":>"          ,"\\mbox{$\\hspace{.29ex}\\succ\\hspace{.29ex}$}\\ "},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   191
   {"~~"          ,"\\mbox{$\\hspace{.29ex}\\approx\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   192
   {"\\sim "      ,"\\mbox{$\\hspace{.29ex}\\sim\\hspace{.29ex}$}\\ "},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   193
   {"\\simeq"     ,"\\mbox{$\\hspace{.29ex}\\simeq\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   194
   {"<="          ,"\\mbox{$\\hspace{.29ex}\\le\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   195
   {"::"          ,"\\mbox{$:\\hspace{-.07ex}:$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   196
   {"<-"          ,"\\mbox{$\\leftarrow$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   197
   {"-"           ,"\\mbox{$-$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   198
   {"->"          ,"\\mbox{$\\rightarrow$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   199
   {"<="          ,"\\mbox{$\\Leftarrow$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   200
   {"="           ,"\\mbox{$=$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   201
   {"=>"          ,"\\mbox{$\\hspace{.12ex}\\Rightarrow$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   202
   {"\\frown"     ,"\\mbox{$\\frown$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   203
   {"|->"         ,"\\mbox{$\\mapsto$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   204
   {"~>"          ,"\\mbox{$\\hspace{.05ex}\\leadsto$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   205
   {"\\uparrow"   ,"\\mbox{$\\uparrow$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   206
   {"\\downarrow" ,"\\mbox{$\\downarrow$}"},
5436
cff7d1e98376 improved spacing
oheimb
parents: 4826
diff changeset
   207
   {"~:"          ,"\\mbox{$\\hspace{.445ex}\\notin\\hspace{.445ex}$}"},
4826
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   208
   {"*"           ,"\\mbox{$\\hspace{-.29ex}\\times\\hspace{-.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   209
   {"++"          ,"\\mbox{$\\hspace{.29ex}\\oplus\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   210
   {"--"          ,"\\mbox{$\\hspace{.29ex}\\ominus\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   211
   {"**"          ,"\\mbox{$\\hspace{.29ex}\\otimes\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   212
   {"//"          ,"\\mbox{$\\hspace{.29ex}\\oslash\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   213
   {"\\subset"    ,"\\mbox{$\\subset$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   214
   {"\\infty"     ,"\\mbox{$\\infty$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   215
   {"\\Box"       ,"\\mbox{$\\Box$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   216
   {"<>"          ,"\\mbox{$\\hspace{.29ex}\\Diamond\\hspace{.29ex}$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   217
   {" o "         ,"\\mbox{$\\circ$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   218
   {"\\bullet"    ,"\\mbox{$\\bullet$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   219
   {"||"          ,"\\mbox{$\\parallel$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   220
   {"\\tick"      ,"\\mbox{$\\surd$}"},
44d38b2737e2 added ASCII translation of subseteq
oheimb
parents: 4773
diff changeset
   221
   {"\\filter"    ,"\\mbox{\\copyright}"}
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   222
};
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   223
/* END_OF_HI_TABLE */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   224
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   225
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   226
/*
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   227
 * conversion table for long ascii and 8bit sequences scanned by lexer
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   228
 * 
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   229
 * first  column is used if destCode is TO_7bit
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   230
 * second column is used if destCode is TO_LaTeX
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   231
 *
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   232
 * Row - 1 is the code (longCode) used by the lexer
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   233
 */      
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   234
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   235
/* do not edit the lines between BEGIN_OF_SEQ_TABLE and END_OF_SEQ_TABLE  */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   236
/* these lines are automatically generated by gen-isa2latex               */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   237
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   238
/* BEGIN_OF_SEQ_TABLE */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   239
char *translationTableSeq[SEQ_TABLE][2] = {
4170
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   240
   {"==>"                                         ,"\\mbox{$\\hspace{-.083ex}\\Longrightarrow$}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   241
   {"-->"                                         ,"\\mbox{$\\longrightarrow$}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   242
   {"?!"                                          ,"\\mbox{$\\exists_1$}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   243
   {"ALL "                                        ,"\\mbox{$\\forall$}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   244
   {"EX "                                         ,"\\mbox{$\\exists$}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   245
   {"<<|"                                         ,"\\mbox{$\\ll\\!\\mid$}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   246
   {"<|"                                          ,"\\mbox{$<\\!\\mid$}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   247
   {"<=="                                         ,"\\mbox{$\\Longleftarrow$}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   248
   {"<=>"                                         ,"\\mbox{$\\Leftrightarrow$}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   249
   {"<--"                                         ,"\\mbox{$\\longleftarrow$}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   250
   {"<->"                                         ,"\\mbox{$\\leftrightarrow$}"},
5675
000879172ee4 added keyword 'and'
oheimb
parents: 5436
diff changeset
   251
   {"and"                                         ,"\\mbox{\\bf and}"},
4170
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   252
   {"arities"                                     ,"\\mbox{\\bf arities}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   253
   {"axclass"                                     ,"\\mbox{\\bf axclass}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   254
   {"constdefs"                                   ,"\\mbox{\\bf constdefs}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   255
   {"consts"                                      ,"\\mbox{\\bf consts}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   256
   {"datatype"                                    ,"\\mbox{\\bf datatype}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   257
   {"defs"                                        ,"\\mbox{\\bf defs}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   258
   {"domain"                                      ,"\\mbox{\\bf domain}"},
4773
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
   259
   {"end"                                         ,"\\mbox{\\bf end}"},
4170
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   260
   {"inductive"                                   ,"\\mbox{\\bf inductive}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   261
   {"instance"                                    ,"\\mbox{\\bf instance}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   262
   {"primrec"                                     ,"\\mbox{\\bf primrec}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   263
   {"recdef"                                      ,"\\mbox{\\bf recdef}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   264
   {"rules"                                       ,"\\mbox{\\bf rules}"},
4773
b6729feb8a5d improved \tt appearance of many ASCII special symbols like #
oheimb
parents: 4170
diff changeset
   265
   {"syntax"                                      ,"\\mbox{\\bf syntax}"},
4170
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   266
   {"translations"                                ,"\\mbox{\\bf translations}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   267
   {"typedef"                                     ,"\\mbox{\\bf typedef}"},
6b8bbcc9f05f several minor improvements
oheimb
parents: 1826
diff changeset
   268
   {"types"                                       ,"\\mbox{\\bf types}"}
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   269
};
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   270
/* END_OF_SEQ_TABLE */
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   271
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   272