+ private void close_log_file() {
+ if (log_file != null) {
+ try {
+ log_file.close();
+ } catch (IOException io) {
+ }
+ log_file = null;
+ }
+ }
+
+ void close() {
+ close_log_file();
+ if (log_thread != null) {
+ log_thread.interrupt();
+ log_thread = null;
+ }