# HG changeset patch # User wenzelm # Date 897472621 -7200 # Node ID 235f8508d4406af77fe5ffb8d80a6368e03a2ff5 # Parent e0f605038a9fa63dc31561cad89a0ad768d63767 added exnMessage; diff -r e0f605038a9f -r 235f8508d440 src/Pure/basis.ML --- a/src/Pure/basis.ML Wed Jun 10 11:56:23 1998 +0200 +++ b/src/Pure/basis.ML Wed Jun 10 11:57:01 1998 +0200 @@ -3,11 +3,9 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Basis Library emulation. - -Needed for Poly/ML and Standard ML of New Jersey version 0.93 to 1.08. - -Full compatibility cannot be obtained using a file: what about char constants? +Basis Library emulation. Needed for Poly/ML and Standard ML of New +Jersey version 0.93 to 1.08. Full compatibility cannot be obtained +using a file: what about char constants? *) exception Subscript; @@ -144,3 +142,37 @@ fun print s = (output (std_out, s); flush_out std_out); + + +structure General = +struct + +local + fun raised name = "exception " ^ name ^ " raised"; + fun raised_msg name msg = raised name ^ ": " ^ msg; +in + fun exnMessage Match = raised_msg "Match" "nonexhaustive match failure" + | exnMessage Bind = raised_msg "Bind" "nonexhaustive binding failure" + | exnMessage Interrupt = "Interrupt" + | exnMessage (Io msg) = "I/O error: " ^ msg + | exnMessage Neg = raised "Neg" + | exnMessage Sum = raised "Sum" + | exnMessage Diff = raised "Diff" + | exnMessage Prod = raised "Prod" + | exnMessage Quot = raised "Quot" + | exnMessage Abs = raised "Abs" + | exnMessage Div = raised "Div" + | exnMessage Mod = raised "Mod" + | exnMessage Floor = raised "Floor" + | exnMessage Sqrt = raised "Sqrt" + | exnMessage Exp = raised "Exp" + | exnMessage Ln = raised "Ln" + | exnMessage Ord = raised "Ord" + | exnMessage Subscript = raised_msg "Subscript " "subscript out of bounds" + | exnMessage Option.Option = raised "Option.Option" + | exnMessage List.Empty = raised "List.Empty" + | exnMessage (TextIO.Io {name, ...}) = raised_msg "TextIO.Io" name + | exnMessage exn = raised "???"; +end; + +end;