# HG changeset patch
# User blanchet
# Date 1380631225 -7200
# Node ID 427b7723874677f5fbfe28734ca2f78f650b09cf
# Parent  5ac1495fed4e6d9c32f53de4e6656c29079de37d
new version of MaSh that really honors the --port option and that checks for file name mismatches

diff -r 5ac1495fed4e -r 427b77238746 src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Tue Oct 01 14:29:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Tue Oct 01 14:40:25 2013 +0200
@@ -39,7 +39,7 @@
     logger = logging.getLogger('start_server')
     logger.info('Starting Server.')
     path = dirname(realpath(__file__))
-    spawnDaemon(os.path.join(path,'server.py'))
+    spawnDaemon(os.path.join(path,'server.py'),os.path.join(path,'server.py'),host,str(port))
     serverIsUp=False
     for _i in range(20):
         # Test if server is up
@@ -91,13 +91,17 @@
 
     # If server is not running, start it.
     startedServer = False
-    try:
-        sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
-        sock.connect((args.host,args.port))       
-        sock.close()
-    except:
+    received = communicate(' '.join(('ping',args.modelFile,args.dictsFile)),args.host,args.port)
+    if received == -1:
         startedServer = start_server(args.host,args.port)
-        
+    elif received.startswith('Files do not match'):
+        logger.error('Filesnames do not match!')
+        logger.error('Modelfile server: '+ received.split()[-2])
+        logger.error('Modelfile argument: '+ args.modelFile)
+        logger.error('Dictsfile server: '+ received.split()[-1])
+        logger.error('Dictsfile argument: '+ args.dictsFile)
+        return
+    
     if args.init or startedServer:
         logger.info('Initializing Server.')
         data = "i "+";".join(argv)
diff -r 5ac1495fed4e -r 427b77238746 src/HOL/Tools/Sledgehammer/MaSh/src/server.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Tue Oct 01 14:29:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Tue Oct 01 14:40:25 2013 +0200
@@ -5,7 +5,7 @@
 #
 # The MaSh Server.
 
-import SocketServer,os,string,logging
+import SocketServer,os,string,logging,sys
 from multiprocessing import Manager
 from threading import Timer
 from time import time
@@ -167,6 +167,12 @@
                 self.shutdown()         
             elif self.data == 'save':
                 self.server.save()       
+            elif self.data.startswith('ping'):
+                mFile, dFile = self.data.split()[1:]
+                if mFile == self.server.args.modelFile and dFile == self.server.args.dictsFile:
+                    self.request.sendall('All good.')
+                else:
+                    self.request.sendall('Files do not match '+' '.join((self.server.args.modelFile,self.server.args.dictsFile)))
             elif self.data.startswith('i'):            
                 self.init(self.data[2:])
             elif self.data.startswith('!'):
@@ -187,9 +193,10 @@
             self.server.lock.release()
 
 if __name__ == "__main__":
-    HOST, PORT = "localhost", 9255
+    HOST, PORT = sys.argv[1:]    
+    #HOST, PORT = "localhost", 9255
     SocketServer.TCPServer.allow_reuse_address = True
-    server = ThreadingTCPServer((HOST, PORT), MaShHandler)
+    server = ThreadingTCPServer((HOST, int(PORT)), MaShHandler)
     server.serve_forever()        
 
 
diff -r 5ac1495fed4e -r 427b77238746 src/HOL/Tools/Sledgehammer/MaSh/src/spawnDaemon.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/spawnDaemon.py	Tue Oct 01 14:29:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/spawnDaemon.py	Tue Oct 01 14:40:25 2013 +0200
@@ -28,8 +28,9 @@
         os._exit(0)
 
     # and finally let's execute the executable for the daemon!
-    try:
-        os.execv(path_to_executable, [path_to_executable])
+    try:        
+        #os.execv(path_to_executable, [path_to_executable])
+        os.execv(path_to_executable, args)
     except Exception, e:
         # oops, we're cut off from the world, let's just give up
         os._exit(255)