# HG changeset patch
# User blanchet
# Date 1381258417 -7200
# Node ID cb33b304e743a35cef5ba8d5fd2a22bc7c2910b2
# Parent  1d371c3f2703520997278de7d1ca6dfcb0929c8c
handle huge MaSh requests gracefully

diff -r 1d371c3f2703 -r cb33b304e743 src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Tue Oct 08 16:40:03 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Tue Oct 08 20:53:37 2013 +0200
@@ -26,7 +26,19 @@
     try:
         sock.connect((host,port))
         sock.sendall(data)
-        received = sock.recv(4194304)
+        received = ''
+        cont = True
+        counter = 0
+        while cont and counter < 100000:
+            rec = sock.recv(4096)
+            if rec == 'stop':
+                cont = False
+            elif rec.endswith('stop'):
+                cont = False
+                received += rec[:-4]
+            else:
+                received += rec
+            counter += 1
     except:
         logger = logging.getLogger('communicate')
         logger.warning('Communication with server failed.')
diff -r 1d371c3f2703 -r cb33b304e743 src/HOL/Tools/Sledgehammer/MaSh/src/server.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Tue Oct 08 16:40:03 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Tue Oct 08 20:53:37 2013 +0200
@@ -150,7 +150,7 @@
         #predictionValues = [str(x) for x in predictionValues[:numberOfPredictions]]
         #predictionsStringList = ['%s=%s' % (predictionNames[i],predictionValues[i]) for i in range(len(predictionNames))]
         #predictionsString = string.join(predictionsStringList,' ')
-        predictionsString = string.join(predictionNames,' ')
+        predictionsString = string.join(predictionNames,' ')        
         outString = '%s: %s' % (name,predictionsString)
         self.request.sendall(outString)
     
@@ -164,7 +164,7 @@
 
     def handle(self):
         # self.request is the TCP socket connected to the client
-        self.data = self.request.recv(4194304).strip()
+        self.data = self.request.recv(134217728).strip()
         self.server.lock.acquire()
         try:
             # Update idle shutdown timer
@@ -199,6 +199,7 @@
             else:
                 self.request.sendall('Unspecified input format: \n%s',self.data)
             self.server.callCounter += 1
+            self.request.sendall('stop')
         finally:
             self.server.lock.release()