author | Walther Neuper <neuper@ist.tugraz.at> |
Tue, 28 Sep 2010 09:06:56 +0200 | |
branch | isac-update-Isa09-2 |
changeset 38031 | 460c24a6a6ba |
parent 37947 | 22235e4dbe5f |
permissions | -rw-r--r-- |
neuper@37906 | 1 |
(* all messages are encoded to integers for the multi-language system |
neuper@37947 | 2 |
use"Frontend/messages.sml"; |
neuper@37906 | 3 |
use"messages.sml"; |
neuper@37906 | 4 |
*) |
neuper@37906 | 5 |
|
neuper@37906 | 6 |
datatype language = English | German | Japanese; |
neuper@37906 | 7 |
fun language2str English = "English" |
neuper@37906 | 8 |
| language2str German = "German" |
neuper@37906 | 9 |
| language2str Japanese = "Japanese"; |
neuper@37906 | 10 |
|
neuper@37906 | 11 |
val language = English; |
neuper@37906 | 12 |
|
neuper@37906 | 13 |
(*1000 system*) |
neuper@37906 | 14 |
fun msg2str 1000 English = |
neuper@37906 | 15 |
"msg 1000 English" |
neuper@37906 | 16 |
| msg2str 1000 German = |
neuper@37906 | 17 |
"msg 1000 German" |
neuper@37906 | 18 |
|
neuper@37906 | 19 |
(*2000 user in model- and specify-phase*) |
neuper@37906 | 20 |
| msg2str 2020 English = |
neuper@37906 | 21 |
"Kernel cannot propose a tactic (helpless!)" |
neuper@37906 | 22 |
|
neuper@37906 | 23 |
|
neuper@37906 | 24 |
(*3000 user in solve-phase*) |
neuper@37906 | 25 |
|
neuper@37906 | 26 |
(*4000 general*) |
neuper@37906 | 27 |
|
neuper@37906 | 28 |
(*5000 general*) |
neuper@37906 | 29 |
|
neuper@37906 | 30 |
(*6000 general*) |
neuper@37906 | 31 |
|
neuper@37906 | 32 |
(*7000 general*) |
neuper@37906 | 33 |
|
neuper@37906 | 34 |
(*1000 general*) |
neuper@37906 | 35 |
|
neuper@37906 | 36 |
(*1000 general*) |
neuper@37906 | 37 |
|
neuper@37906 | 38 |
(*1000 general*) |
neuper@37906 | 39 |
|
neuper@37906 | 40 |
(*1000 general*) |
neuper@37906 | 41 |
|
neuper@38031 | 42 |
| msg2str i l = error ("no message for No. "^ |
neuper@37906 | 43 |
string_of_int i^" "^language2str l); |