equal
deleted
inserted
replaced
|
1 (* all messages are encoded to integers for the multi-language system |
|
2 use"Frontend/messages.sml"; |
|
3 use"messages.sml"; |
|
4 *) |
|
5 |
|
6 datatype language = English | German | Japanese; |
|
7 fun language2str English = "English" |
|
8 | language2str German = "German" |
|
9 | language2str Japanese = "Japanese"; |
|
10 |
|
11 val language = English; |
|
12 |
|
13 (*1000 system*) |
|
14 fun msg2str 1000 English = |
|
15 "msg 1000 English" |
|
16 | msg2str 1000 German = |
|
17 "msg 1000 German" |
|
18 |
|
19 (*2000 user in model- and specify-phase*) |
|
20 | msg2str 2020 English = |
|
21 "Kernel cannot propose a tactic (helpless!)" |
|
22 |
|
23 |
|
24 (*3000 user in solve-phase*) |
|
25 |
|
26 (*4000 general*) |
|
27 |
|
28 (*5000 general*) |
|
29 |
|
30 (*6000 general*) |
|
31 |
|
32 (*7000 general*) |
|
33 |
|
34 (*1000 general*) |
|
35 |
|
36 (*1000 general*) |
|
37 |
|
38 (*1000 general*) |
|
39 |
|
40 (*1000 general*) |
|
41 |
|
42 | msg2str i l = raise error ("no message for No. "^ |
|
43 string_of_int i^" "^language2str l); |