(* 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);