--- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py Fri Oct 18 13:30:09 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py Fri Oct 18 13:38:55 2013 +0200
@@ -22,7 +22,8 @@
from parameters import init_parser
def communicate(data,host,port):
- sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
+ logger = logging.getLogger('communicate')
+ sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
try:
sock.connect((host,port))
sock.sendall(data+'\n')
@@ -37,8 +38,9 @@
else:
received += rec
counter += 1
- except:
- logger = logging.getLogger('communicate')
+ if rec == '':
+ logger.warning('No response from server. Check server log for details.')
+ except:
logger.warning('Communication with server failed.')
received = -1
finally:
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/server.py Fri Oct 18 13:30:09 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/server.py Fri Oct 18 13:38:55 2013 +0200
@@ -198,8 +198,11 @@
self.request.sendall(self.server.stats.printAvg())
else:
self.request.sendall('Unspecified input format: \n%s',self.data)
- self.server.callCounter += 1
- self.request.sendall('stop')
+ self.server.callCounter += 1
+ self.request.sendall('stop')
+ except: # catch exceptions
+ #print 'Caught an error. Check %s for more details' % (self.server.args.log+'server')
+ logging.exception('')
finally:
self.server.lock.release()