# HG changeset patch
# User blanchet
# Date 1382096335 -7200
# Node ID 942bb9d9b7a8e3e58afd16f03b8d5c7cc9d08ecf
# Parent  70456a8f5e6e3a75c1f9719d84dad59985e8104f
MaSh error handling

diff -r 70456a8f5e6e -r 942bb9d9b7a8 src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
--- 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:
diff -r 70456a8f5e6e -r 942bb9d9b7a8 src/HOL/Tools/Sledgehammer/MaSh/src/server.py
--- 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()