(* all messages are encoded to integers for the multi-language system

    use"Frontend/messages.sml";

    use"messages.sml";

    *)

 datatype language = English | German | Japanese;

 fun language2str English = "English"

   | language2str German = "German"

   | language2str Japanese = "Japanese";

 val language = English;

 (*1000 system*)

 fun msg2str 1000 English =

     "msg 1000 English"

   | msg2str 1000 German =

     "msg 1000 German"

 (*2000 user in model- and specify-phase*)

   | msg2str 2020 English =

     "Kernel cannot propose a tactic (helpless!)"

 (*3000 user in solve-phase*)

 (*4000 general*)

 (*5000 general*)

 (*6000 general*)

 (*7000 general*)

 (*1000 general*)

 (*1000 general*)

 (*1000 general*)

 (*1000 general*)

   | msg2str i l = raise error ("no message for No. "^

 			string_of_int i^" "^language2str l);