# HG changeset patch
# User blanchet
# Date 1382085355 -7200
# Node ID 0fadd32e8d50425f733eff0f82a387920775b6b1
# Parent  18def1c73c79a4a2fb58dac146b1e5852e3d4343
accept very long lines in MaSh

diff -r 18def1c73c79 -r 0fadd32e8d50 src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Fri Oct 18 00:05:31 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Fri Oct 18 10:35:55 2013 +0200
@@ -25,15 +25,13 @@
     sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
     try:
         sock.connect((host,port))
-        sock.sendall(data)
+        sock.sendall(data+'\n')        
         received = ''
         cont = True
         counter = 0
         while cont and counter < 100000:
             rec = sock.recv(4096)
-            if rec == 'stop':
-                cont = False
-            elif rec.endswith('stop'):
+            if rec.endswith('stop'):
                 cont = False
                 received += rec[:-4]
             else:
diff -r 18def1c73c79 -r 0fadd32e8d50 src/HOL/Tools/Sledgehammer/MaSh/src/server.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Fri Oct 18 00:05:31 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Fri Oct 18 10:35:55 2013 +0200
@@ -50,7 +50,7 @@
         self.save()          
         self.shutdown()
 
-class MaShHandler(SocketServer.BaseRequestHandler):
+class MaShHandler(SocketServer.StreamRequestHandler):
 
     def init(self,argv):
         if argv == '':
@@ -164,15 +164,15 @@
 
     def handle(self):
         # self.request is the TCP socket connected to the client
-        self.data = self.request.recv(134217728).strip()
         self.server.lock.acquire()
+        self.data = self.rfile.readline().strip()
         try:
             # Update idle shutdown timer
             self.server.idle_timer.cancel()
             self.server.idle_timer = Timer(self.server.idle_timeout, self.server.save_and_shutdown)
             self.server.idle_timer.start()        
 
-            self.startTime = time()  
+            self.startTime = time()
             if self.data == 'shutdown':
                 self.shutdown()         
             elif self.data == 'save':
@@ -198,7 +198,7 @@
                 self.request.sendall(self.server.stats.printAvg())            
             else:
                 self.request.sendall('Unspecified input format: \n%s',self.data)
-            self.server.callCounter += 1
+            self.server.callCounter += 1            
             self.request.sendall('stop')
         finally:
             self.server.lock.release()