diff --git a/gui/.gitignore b/gui/.gitignore
index 0d20b64..e380cb5 100644
--- a/gui/.gitignore
+++ b/gui/.gitignore
@@ -1 +1,3 @@
 *.pyc
+progressbar.py
+Cache
diff --git a/gui/Scyther/Misc.py b/gui/Scyther/Misc.py
index 2f9a344..494e17e 100644
--- a/gui/Scyther/Misc.py
+++ b/gui/Scyther/Misc.py
@@ -64,6 +64,40 @@ def sorted(li):
     return result
 
 
+# ensurePath: does what os.makedirs should do.
+def ensurePath(pt):
+    """
+    Make sure the path exists: if not, create the directories one by one
+
+    By example:
+
+    Call with "dog/cat/bone" ensures that afterwards, this subdirectory structure (dog/cat/bone) exists, with 'bone' a directory.
+    It ensures this by doing the procedure for "dog", then "dog/cat", etc...
+    """
+
+    ptn = os.path.normpath(pt)
+
+    # First we see what needs to exist overall
+    todo = [ptn]
+    tail = "x"
+    while len(tail) > 0:
+        (head,tail) = os.path.split(ptn)
+        if len(head) > 0:
+            todo.append(head)
+            ptn = head
+        else:
+            break
+
+    # Reverse list: path prefixes first
+    todo.reverse()
+
+    # Create bottom-up
+    for pt in todo:
+        if not os.path.isdir(pt):
+            # Note that os.path.exists(pt) may still hold. In this case the next command will cause an error.
+            os.mkdir(pt)
+
+
 # path
 def mypath(file):
     """ Construct a file path relative to the scyther-gui main directory
diff --git a/gui/Scyther/Scyther.py b/gui/Scyther/Scyther.py
index 80aa116..24441dd 100755
--- a/gui/Scyther/Scyther.py
+++ b/gui/Scyther/Scyther.py
@@ -30,7 +30,12 @@ import os.path
 import sys
 import StringIO
 import tempfile
-
+try:
+    import hashlib
+    HASHLIB = True
+except ImportError:
+    HASHLIB = False
+    pass
 
 #---------------------------------------------------------------------------
 
@@ -235,6 +240,73 @@ class Scyther(object):
             self.options += " %s" % (arg)
 
     def doScytherCommand(self, spdl, args):
+        """
+        Cached version of the 'real' below
+        """
+        global HASHLIB
+
+        if not HASHLIB:
+            return self.doScytherCommandReal(spdl,args)
+
+        # So we have the hashing libs
+        m = hashlib.sha256()
+        if spdl == None:
+            m.update("[spdl:None]")
+        else:
+            m.update(spdl)
+        if args == None:
+            m.update("[args:None]")
+        else:
+            m.update(args)
+
+        uid = m.hexdigest()
+
+        # Split the uid to make (256?) subdirectories
+        prefixlen = 2
+        uid1 = uid[:prefixlen]
+        uid2 = uid[prefixlen:]
+
+        # Possibly we could also decide to store input and arguments in the cache to analyze things later
+
+        path = "Cache/%s/" % (uid1)
+        name1 = "%s.out" % (uid2)
+        name2 = "%s.err" % (uid2)
+
+        fname1 = path + name1
+        fname2 = path + name2
+
+        try:
+            """
+            Try to retrieve the result from the cache
+            """
+            fh1 = open(fname1,"r")
+            out = fh1.read()
+            fh1.close()
+            fh2 = open(fname2,"r")
+            err = fh2.read()
+            fh2.close()
+            return (out,err)
+        except:
+            """
+            Something went wrong, do the real thing and cache afterwards
+            """
+            (out,err) = self.doScytherCommandReal(spdl,args)
+
+            # Store result in cache
+            ensurePath(path)
+
+            fh1 = open(fname1,"w")
+            fh1.write(out)
+            fh1.close()
+
+            fh2 = open(fname2,"w")
+            fh2.write(err)
+            fh2.close()
+
+            return (out,err)
+
+
+    def doScytherCommandReal(self, spdl, args):
         """ 
         Run Scyther backend on the input