root / trunk / extensions / extScripting / scripts / jython / console / history.py @ 11445
History | View | Annotate | Download (1.78 KB)
1 | 5782 | jmvivo | """
|
---|---|---|---|
2 | history.py - Handles the History of the jython console
|
||
3 | Copyright (C) 2001 Carlos Quiroz
|
||
4 |
|
||
5 | This program is free software; you can redistribute it and/or
|
||
6 | modify it under the terms of the GNU General Public License
|
||
7 | as published by the Free Software Foundation; either version 2
|
||
8 | of the License, or any later version.
|
||
9 |
|
||
10 | This program is distributed in the hope that it will be useful,
|
||
11 | but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||
12 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||
13 | GNU General Public License for more details.
|
||
14 |
|
||
15 | You should have received a copy of the GNU General Public License
|
||
16 | along with this program; if not, write to the Free Software
|
||
17 | Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
|
||
18 | """
|
||
19 | #from org.gjt.sp.jedit.gui import HistoryModel
|
||
20 | |||
21 | class History: |
||
22 | """
|
||
23 | The class history handles the history management basically wrapping the
|
||
24 | built-in jEdit's history capabilities
|
||
25 | """
|
||
26 | |||
27 | def __init__(self, console): |
||
28 | self.history = []
|
||
29 | self.console = console
|
||
30 | self.index = 0 |
||
31 | self.last = "" |
||
32 | |||
33 | def append(self, line): |
||
34 | if line == '\n' or len(line) == 0: return |
||
35 | ## if line == self.last: # avoid duplicates
|
||
36 | ## self.index = len(self.history) - 1
|
||
37 | ## return
|
||
38 | |||
39 | self.last = line
|
||
40 | self.history.append(line)
|
||
41 | self.index = len(self.history) - 1 |
||
42 | |||
43 | def historyUp(self, event): |
||
44 | if len(self.history) > 0 and self.console.inLastLine(): |
||
45 | self.console.replaceRow(self.history[self.index]) |
||
46 | self.index = max(self.index - 1, 0) |
||
47 | |||
48 | def historyDown(self, event): |
||
49 | if len(self.history) > 0 and self.console.inLastLine(): |
||
50 | if self.index == len(self.history) - 1: |
||
51 | self.console.replaceRow("") |
||
52 | else:
|
||
53 | self.index += 1 |
||
54 | self.console.replaceRow(self.history[self.index]) |