equal
deleted
inserted
replaced
18 case other: User_Error => message == other.getMessage |
18 case other: User_Error => message == other.getMessage |
19 case _ => false |
19 case _ => false |
20 } |
20 } |
21 override def hashCode: Int = message.hashCode |
21 override def hashCode: Int = message.hashCode |
22 |
22 |
23 override def toString: String = "\n" + Output.error_text(message) |
23 override def toString: String = "\n" + Output.error_message_text(message) |
24 } |
24 } |
25 |
25 |
26 object ERROR |
26 object ERROR |
27 { |
27 { |
28 def apply(message: String): User_Error = new User_Error(message) |
28 def apply(message: String): User_Error = new User_Error(message) |