##// END OF EJS Templates
Replace exit command set with regex.
Thomas Kluyver -
Show More
@@ -88,11 +88,10 b' class HistoryManager(Configurable):'
88 _ii = Unicode(u'')
88 _ii = Unicode(u'')
89 _iii = Unicode(u'')
89 _iii = Unicode(u'')
90
90
91 # A set with all forms of the exit command, so that we don't store them in
91 # A regex matching all forms of the exit command, so that we don't store
92 # the history (it's annoying to rewind the first entry and land on an exit
92 # them in the history (it's annoying to rewind the first entry and land on
93 # call).
93 # an exit call).
94 _exit_commands = Instance(set, args=(['Quit', 'quit', 'Exit', 'exit',
94 _exit_re = re.compile(r"(exit|quit)(\s*\(.*\))?$")
95 '%Quit', '%quit', '%Exit', '%exit'],))
96
95
97 def __init__(self, shell, config=None, **traits):
96 def __init__(self, shell, config=None, **traits):
98 """Create a new history manager associated with a shell instance.
97 """Create a new history manager associated with a shell instance.
@@ -377,7 +376,7 b' class HistoryManager(Configurable):'
377 source_raw = source_raw.rstrip('\n')
376 source_raw = source_raw.rstrip('\n')
378
377
379 # do not store exit/quit commands
378 # do not store exit/quit commands
380 if source_raw.strip() in self._exit_commands:
379 if self._exit_re.match(source_raw.strip()):
381 return
380 return
382
381
383 self.input_hist_parsed.append(source)
382 self.input_hist_parsed.append(source)
General Comments 0
You need to be logged in to leave comments. Login now