1 (* all messages are encoded to integers for the multi-language system
2 use"Frontend/messages.sml";
6 datatype language = English | German | Japanese;
7 fun language2str English = "English"
8 | language2str German = "German"
9 | language2str Japanese = "Japanese";
11 val language = English;
14 fun msg2str 1000 English =
16 | msg2str 1000 German =
19 (*2000 user in model- and specify-phase*)
20 | msg2str 2020 English =
21 "Kernel cannot propose a tactic (helpless!)"
24 (*3000 user in solve-phase*)
42 | msg2str i l = error ("no message for No. "^
43 string_of_int i^" "^language2str l);