82 |
* Each marked cell is represented as a <code>gzz.view.Mark</code> |
* Each marked cell is represented as a <code>gzz.view.Mark</code> |
83 |
* object. We don't have support for multiple mark sets yet. |
* object. We don't have support for multiple mark sets yet. |
84 |
*/ |
*/ |
85 |
public java.util.List marks = new ArrayList(); |
public static java.util.List marks = new ArrayList(); |
86 |
|
|
87 |
/** The set of all marked cells. |
/** The set of all marked cells. |
88 |
* This is the set of all cells in the <code>Mark</code> objects |
* This is the set of all cells in the <code>Mark</code> objects |
90 |
* the whole list for all cells on the screen scales badly. |
* the whole list for all cells on the screen scales badly. |
91 |
* We want to be able to have big mark sets. |
* We want to be able to have big mark sets. |
92 |
*/ |
*/ |
93 |
public Set markedCells = new HashSet(); |
public static Set markedCells = new HashSet(); |
94 |
|
|
95 |
/** The last client exception that occurred, if any. |
/** The last client exception that occurred, if any. |
96 |
*/ |
*/ |
274 |
} else if(k.equals("Ctrl-E")) { |
} else if(k.equals("Ctrl-E")) { |
275 |
editPlainText(fallback.windows[1].cursor); |
editPlainText(fallback.windows[1].cursor); |
276 |
} else if(k.equals("Ctrl-L")) { |
} else if(k.equals("Ctrl-L")) { |
277 |
makeLink(1); |
makeLink(fallback, 1); |
278 |
} else if(k.equals("Alt-L")) { |
} else if(k.equals("Alt-L")) { |
279 |
makeLink(-1); |
makeLink(fallback, -1); |
280 |
} else if(k.equals("Ctrl-F")) { |
} else if(k.equals("Ctrl-F")) { |
281 |
fallback.mode = fallback.SEARCH; |
fallback.mode = fallback.SEARCH; |
282 |
buffer = ""; |
buffer = ""; |
368 |
} |
} |
369 |
} else if(k.equals("Ctrl-0")) { |
} else if(k.equals("Ctrl-0")) { |
370 |
// totally temporary! |
// totally temporary! |
371 |
createPageSpan(); |
createPageSpan(fallback); |
372 |
} |
} |
373 |
} |
} |
374 |
|
|
485 |
} |
} |
486 |
} |
} |
487 |
|
|
488 |
public void makeLink(int dir) { |
public static void makeLink(Fallback fallback, int dir) { |
489 |
Cell c = fallback.windows[1].cursor; |
Cell c = fallback.windows[1].cursor; |
490 |
VStreamCellTexter ct = (VStreamCellTexter)c.space.getCellTexter(); |
VStreamCellTexter ct = (VStreamCellTexter)c.space.getCellTexter(); |
491 |
Enfilade1D from = ct.getEnfilade(c, null); |
Enfilade1D from = ct.getEnfilade(c, null); |
492 |
|
|
493 |
makeLink(dir, from); |
makeLink(fallback, dir, from); |
494 |
} |
} |
495 |
|
|
496 |
public void makeLink(int dir, Enfilade1D from) { |
public static void makeLink(Fallback fallback, int dir, Enfilade1D from) { |
497 |
Enfilade1D to = from.getMaker().makeEnfilade(); |
Enfilade1D to = from.getMaker().makeEnfilade(); |
498 |
for(Iterator i=marks.iterator(); i.hasNext();) { |
for(Iterator i=marks.iterator(); i.hasNext();) { |
499 |
Mark m = (Mark)i.next(); |
Mark m = (Mark)i.next(); |
517 |
* system property <code>user.editor</code>, or alternatively uses |
* system property <code>user.editor</code>, or alternatively uses |
518 |
* an AWT window with a multiline text area (XXX not implemented). |
* an AWT window with a multiline text area (XXX not implemented). |
519 |
*/ |
*/ |
520 |
public void editPlainText(Cell c) { |
public static void editPlainText(Cell c) { |
521 |
VStreamCellTexter texter = (VStreamCellTexter)c.space.getCellTexter(); |
VStreamCellTexter texter = (VStreamCellTexter)c.space.getCellTexter(); |
522 |
gzz.fuzzy.EnfiladeAligner.Instance aligner = |
gzz.fuzzy.EnfiladeAligner.Instance aligner = |
523 |
texter.startEnfiladeAligner(c); |
texter.startEnfiladeAligner(c); |
576 |
} |
} |
577 |
texter.setEnfilade(c, aligner.getEnfilade(text)); |
texter.setEnfilade(c, aligner.getEnfilade(text)); |
578 |
} |
} |
579 |
private boolean is_ok; |
private static boolean is_ok; |
580 |
|
|
581 |
/** Execute the external editor with the given input and return the |
/** Execute the external editor with the given input and return the |
582 |
* output. |
* output. |
594 |
* may well work. |
* may well work. |
595 |
* @returns The edited text. |
* @returns The edited text. |
596 |
*/ |
*/ |
597 |
String execExternalEditor(String editor, String text, String encoding) { |
static String execExternalEditor(String editor, String text, String encoding) { |
598 |
File tmp = null; |
File tmp = null; |
599 |
|
|
600 |
try { |
try { |
634 |
* accursed in the right window. (Note: This doesn't have |
* accursed in the right window. (Note: This doesn't have |
635 |
* to be a page scroll, can be text or anything else...) |
* to be a page scroll, can be text or anything else...) |
636 |
*/ |
*/ |
637 |
void createPageSpan() { |
static void createPageSpan(Fallback fallback) { |
638 |
try { |
try { |
639 |
pa("Enter id of span block to put in this cell:"); |
pa("Enter id of span block to put in this cell:"); |
640 |
BufferedReader r = new BufferedReader(new InputStreamReader(System.in)); |
BufferedReader r = new BufferedReader(new InputStreamReader(System.in)); |