1 package acl2s.plugin.editors.session;
2
3 import org.eclipse.core.runtime.CoreException;
4 import org.eclipse.jface.action.IAction;
5 import org.eclipse.jface.preference.IPreferenceStore;
6 import org.eclipse.jface.resource.ColorRegistry;
7 import org.eclipse.jface.text.BadLocationException;
8 import org.eclipse.jface.text.DocumentEvent;
9 import org.eclipse.jface.text.IDocumentListener;
10 import org.eclipse.jface.text.IRegion;
11 import org.eclipse.jface.text.Region;
12 import org.eclipse.jface.text.source.CompositeRuler;
13 import org.eclipse.jface.text.source.IOverviewRuler;
14 import org.eclipse.jface.text.source.ISharedTextColors;
15 import org.eclipse.jface.viewers.DoubleClickEvent;
16 import org.eclipse.jface.viewers.IColorProvider;
17 import org.eclipse.jface.viewers.IDoubleClickListener;
18 import org.eclipse.jface.viewers.ILabelProvider;
19 import org.eclipse.jface.viewers.ILabelProviderListener;
20 import org.eclipse.jface.viewers.ISelection;
21 import org.eclipse.jface.viewers.IStructuredSelection;
22 import org.eclipse.jface.viewers.ITreeContentProvider;
23 import org.eclipse.jface.viewers.SelectionChangedEvent;
24 import org.eclipse.jface.viewers.StructuredSelection;
25 import org.eclipse.jface.viewers.TreeViewer;
26 import org.eclipse.jface.viewers.Viewer;
27 import org.eclipse.swt.SWT;
28 import org.eclipse.swt.custom.StyledText;
29 import org.eclipse.swt.events.VerifyEvent;
30 import org.eclipse.swt.events.VerifyListener;
31 import org.eclipse.swt.graphics.Color;
32 import org.eclipse.swt.graphics.Image;
33 import org.eclipse.swt.graphics.Point;
34 import org.eclipse.swt.widgets.Composite;
35 import org.eclipse.swt.widgets.Display;
36 import org.eclipse.swt.widgets.Shell;
37 import org.eclipse.ui.IEditorInput;
38 import org.eclipse.ui.IEditorSite;
39 import org.eclipse.ui.PartInitException;
40 import org.eclipse.ui.texteditor.AbstractTextEditor;
41 import org.eclipse.ui.texteditor.ITextEditorActionDefinitionIds;
42 import org.eclipse.ui.views.contentoutline.ContentOutlinePage;
43 import org.eclipse.ui.views.contentoutline.IContentOutlinePage;
44
45 import acl2s.lib.session.IStatusInfo;
46 import acl2s.plugin.Acl2sPlugin;
47 import acl2s.plugin.IPeerDocument;
48 import acl2s.plugin.ISessionDocument;
49 import acl2s.plugin.editors.A2sEditor;
50 import acl2s.plugin.editors.session.SessionDocument.DoneElement;
51 import acl2s.plugin.misc.Colors;
52 import acl2s.plugin.parse.LispTokens;
53 import acl2s.plugin.prefs.InteractionPrefs;
54 import acl2s.plugin.prefs.SessionPrefs;
55 import acl2s.uilib.cmd.ResolvedInput;
56 import acl2s.uilib.session.IInputInfo;
57 import acl2s.uilib.session.ISessionStatusListener;
58 import acl2s.uilib.session.RedoInput;
59 import acl2s.uilib.session.StartupInputAndEnv;
60 import acl2s.uilib.session.UndoInput;
61
62 public class SessionEditor extends A2sEditor
63 implements ISessionStatusListener, VerifyListener, IDocumentListener {
64 public static final String id = "acl2s.plugin.editors.session";
65
66 protected final Display display = Display.getDefault();
67 protected SessionSourceViewerConfiguration ssvc = null;
68 protected SessionDocument model = null;
69 protected boolean gotoEnd = false;
70 protected SessionContentOutlinePage outlinePage = null;
71
72 /*========================== some accessors ==========================*/
73 public SessionDocument getDocument() {
74 return model;
75 }
76
77 public IPeerDocument getPeerDocument() {
78 return getDocument().getPeer();
79 }
80
81 public ISessionDocument getSessionDocument() {
82 return model;
83 }
84
85 /*======================= outline view support =======================*/
86
87 protected class SessionContentOutlinePage extends ContentOutlinePage
88 implements ITreeContentProvider, ILabelProvider, IColorProvider,
89 IDoubleClickListener, IDocumentListener {
90 ColorRegistry colorReg = Acl2sPlugin.getDefault().getWorkbench().getThemeManager().getCurrentTheme().getColorRegistry();
91 int completedSeen = 0;
92 boolean curHasInput = false;
93
94 @Override
95 public void createControl(Composite parent) {
96 super.createControl(parent);
97 model.addDocumentListener(this);
98 TreeViewer tv = getTreeViewer();
99 tv.setLabelProvider(this);
100 tv.setContentProvider(this);
101 tv.setInput(model);
102 tv.addDoubleClickListener(this);
103 update();
104 }
105
106 @Override
107 public void dispose() {
108 Acl2sPlugin.maybeWarnOutline3_3();
109 TreeViewer tv = getTreeViewer();
110 tv.removeDoubleClickListener(this);
111 model.removeDocumentListener(this);
112 super.dispose();
113 }
114
115 public void documentAboutToBeChanged(DocumentEvent event) { }
116
117 public void documentChanged(DocumentEvent event) {
118 update();
119 }
120
121 public void update() {
122 int nowCompleted = model.countCompletedCmds();
123 if (nowCompleted == completedSeen) {
124 if ((model.cur.input != null) != curHasInput) {
125 getTreeViewer().update(new Integer(completedSeen), null);
126 }
127 return;
128 }
129 final TreeViewer tv = getTreeViewer();
130 if (nowCompleted < completedSeen || completedSeen == 0) {
131 completedSeen = nowCompleted;
132 tv.refresh();
133 Acl2sPlugin.getDisplay().asyncExec(outlineUpdaterForCursor);
134 return;
135 }
136 // otherwise, try to do incremental update
137 tv.update(new Integer(completedSeen), null);
138 do {
139 completedSeen++;
140 tv.add(tv.getInput(), new Integer(completedSeen));
141 } while (completedSeen < nowCompleted);
142 Acl2sPlugin.getDisplay().asyncExec(outlineUpdaterForCursor);
143 }
144
145 public Object[] getElements(Object inputElement) {
146 Object[] elts = new Object[completedSeen+1];
147 for (int i = 0; i <= completedSeen; i++) {
|
Event do_not_call: |
"java.lang.Integer(int arg1)" is not recommended for performance reasons. Consider using Integer.valueOf(int) instead. |
148 elts[i] = new Integer(i);
149 }
150 return elts;
151 }
152
153 Image img_event_very_bad = Acl2sPlugin.getImage("icons/event_very_bad.gif");
154 Image img_event_bad = Acl2sPlugin.getImage("icons/event_bad.gif");
155 Image img_compute_bad = Acl2sPlugin.getImage("icons/compute_bad.gif");
156 Image img_inspect_bad = Acl2sPlugin.getImage("icons/inspect_bad.gif");
157
158 Image img_compute = Acl2sPlugin.getImage("icons/compute.gif");
159 Image img_inspect = Acl2sPlugin.getImage("icons/inspect.gif");
160 Image img_event_compute = Acl2sPlugin.getImage("icons/event_compute.gif");
161 Image img_event = Acl2sPlugin.getImage("icons/event.gif");
162 Image img_book_open = Acl2sPlugin.getImage("icons/book_open.gif");
163 Image img_pkg_open = Acl2sPlugin.getImage("icons/pkg_open.gif");
164 Image img_event_gear = Acl2sPlugin.getImage("icons/event_gear.gif");
165 Image img_event_unknown = Acl2sPlugin.getImage("icons/event_unknown.gif");
166
167 Image img_redo = Acl2sPlugin.getImage("icons/redo.gif");
168 Image img_undo = Acl2sPlugin.getImage("icons/undo.gif");
169
170
171 public Image getImage(Object element) {
172 if (element instanceof Integer) {
173 int idx = ((Integer)element).intValue();
174 IInputInfo input = model.getInput(idx);
175 if (input == null) {
176 return null;
177 }
178 String typeStr = input.getInputTypeString();
179 if (typeStr == null) {
180 return null;
181 }
182 if (typeStr.equals("BAD")) {
183 return img_event_very_bad;
184 }
185 //IStatusInfo status = model.getStatus(idx);
186 if (input instanceof ResolvedInput) {
187 ResolvedInput input2 = (ResolvedInput)input;
188 //if (status.wasSuccess()) {
189 switch (input2.getType()) {
190 case ResolvedInput.VALUE:
191 return img_compute;
192 case ResolvedInput.QUERY:
193 return img_inspect;
194 case ResolvedInput.VALTRIP:
195 return img_event_compute;
196 case ResolvedInput.EVENT:
197 return img_event;
198 case ResolvedInput.BEGIN_BOOK:
199 return img_book_open;
200 case ResolvedInput.IN_PACKAGE:
201 return img_pkg_open;
202 case ResolvedInput.COMMAND:
203 return img_event_gear;
204 case ResolvedInput.ACTION:
205 case ResolvedInput.RAW:
206 default:
207 return img_event_unknown;
208 }
209 /*
210 } else {
211 switch (input2.getType()) {
212 case ResolvedInput.VALUE:
213 return img_compute_bad;
214 case ResolvedInput.QUERY:
215 return img_inspect_bad;
216 case ResolvedInput.VALTRIP:
217 case ResolvedInput.EVENT:
218 case ResolvedInput.BEGIN_BOOK:
219 case ResolvedInput.IN_PACKAGE:
220 case ResolvedInput.COMMAND:
221 case ResolvedInput.ACTION:
222 case ResolvedInput.RAW:
223 default:
224 return img_event_bad;
225 }
226 }*/
227 }
228 if (input instanceof RedoInput) {
229 return img_redo;
230 }
231 if (input instanceof UndoInput) {
232 return img_undo;
233 }
234 }
235 // otherwise
236 return null;
237 }
238
239 public String getText(Object element) {
240 if (element instanceof Integer) {
241 int idx = ((Integer)element).intValue();
242 IInputInfo input = model.getInput(idx);
243 if (input == null) {
244 if (idx == completedSeen) {
245 return "<prompt>";
246 } else {
247 return "<session beginning>";
248 }
249 } else {
250 String inputStr = input.getInputString();
251 if (inputStr == null) {
252 return "<session startup>";
253 } else {
254 return firstLine(inputStr);
255 }
256 }
257 } else {
258 return null;
259 }
260 }
261
262
263 public Color getBackground(Object element) {
264 return null;
265 }
266
267 public Color getForeground(Object element) {
268 if (element instanceof Integer) {
269 int idx = ((Integer)element).intValue();
270 if (idx < model.countCompletedCmds()) {
271 IStatusInfo status = model.getStatus(idx);
272 if (status != null) {
273 if (status.wasSuccess()) {
274 return colorReg.get("acl2s.plugin.color.output");
275 } else {
276 return colorReg.get("acl2s.plugin.color.outputerr");
277 }
278 }
279 }
280 }
281 return Colors.BLACK;
282 }
283
284 public void doubleClick(DoubleClickEvent event) {
285 Object src = ((IStructuredSelection)event.getSelection()).getFirstElement();
286 if (src instanceof Integer) {
287 int midx = ((Integer)src).intValue();
288 if (midx < completedSeen || curHasInput) {
289 setDocCaret(model.getOffsetOfModelIdx(midx));
290 } else {
291 setDocCaret(model.readOnlyPoint());
292 }
293 SessionEditor.this.setFocus();
294 }
295 }
296
297 @Override
298 public void selectionChanged(SelectionChangedEvent event) {
299 super.selectionChanged(event);
300 if (!inReverseSelect) {
301 Object src = ((IStructuredSelection)event.getSelection()).getFirstElement();
302 if (src instanceof Integer) {
303 revealRange(model.getOffsetOfModelIdx(((Integer)src).intValue()),1);
304 }
305 }
306 }
307
308 boolean inReverseSelect = false;
309
310 public void select(final int midx) {
311 TreeViewer tv = getTreeViewer();
312 ISelection s = tv.getSelection();
313 if (s instanceof IStructuredSelection) {
314 IStructuredSelection ss = (IStructuredSelection) s;
315 Object sel = new Integer(midx);
316 if (!ss.toList().contains(sel)) {
317 inReverseSelect = true;
318 tv.setSelection(new StructuredSelection(sel), true);
319 inReverseSelect = false;
320 }
321 }
322 }
323
324 public Object getParent(Object element) { return null; }
325
326 public Object[] getChildren(Object parentElement) { return emptyArray; }
327
328 public boolean hasChildren(Object element) { return false; }
329
330 public void inputChanged(Viewer viewer, Object oldInput, Object newInput) { }
331
332 public boolean isLabelProperty(Object element, String property) { return false; }
333
334 public void addListener(ILabelProviderListener listener) { }
335
336 public void removeListener(ILabelProviderListener listener) { }
337 }
338
339 static final Object[] emptyArray = new Object[0];
340
341 static String firstLine(String str) {
342 int returnPos = str.indexOf('\r');
343 int newlinePos = str.indexOf('\n');
344 if (returnPos >= 0) {
345 if (newlinePos >= 0 && newlinePos < returnPos) {
346 return str.substring(0, newlinePos);
347 }
348 return str.substring(0, returnPos);
349 } else {
350 if (newlinePos >= 0) {
351 return str.substring(0, newlinePos);
352 } else {
353 return str;
354 }
355 }
356 }
357
358 protected Runnable outlineUpdaterForCursor = new Runnable() {
359 public void run() {
360 try {
361 if (outlinePage != null) {
362 int midx = model.getModelIdxOfOffset(getDocCaret());
363 outlinePage.select(midx);
364 }
365 } finally {
366 outlineUpdaterPending = false;
367 }
368 }
369 };
370
371 private boolean outlineUpdaterPending = false;
372
373 @Override
374 protected void handleCursorPositionChanged() {
375 super.handleCursorPositionChanged();
376 if (outlinePage != null && !outlineUpdaterPending) {
377 Acl2sPlugin.getDisplay().asyncExec(outlineUpdaterForCursor);
378 outlineUpdaterPending = true;
379 }
380 }
381
382 @SuppressWarnings("unchecked") // Eclipse complains without this
383 @Override
384 public Object getAdapter(Class adapter) {
385 if (adapter == IContentOutlinePage.class) {
386 if (outlinePage == null) {
387 outlinePage = new SessionContentOutlinePage();
388 }
389 return outlinePage;
390 }
391 return super.getAdapter(adapter);
392 }
393
394
395
396 /*======================= make the thing read-only ==================*/
397 protected void setupSourceViewer() {
398 super.setupSourceViewer();
399 text.addVerifyListener(this);
400 setViewport(VIEWPORT_ALL);
401 }
402
403 public void createPartControl(Composite parent) {
404 super.createPartControl(parent);
405 gotoEnd();
406 }
407
408
409 /*===================== get rid of vertical rulers ==================*/
410 protected boolean isLineNumberRulerVisible() { return false; }
411
412 protected boolean isPrefQuickDiffAlwaysOn() { return false; }
413
414 protected CompositeRuler createCompositeRuler() {
415 CompositeRuler ruler= new CompositeRuler();
416 return ruler;
417 }
418
419 protected boolean isOverviewRulerVisible() { return false; }
420
421 protected IOverviewRuler createOverviewRuler(ISharedTextColors sharedColors) {
422 return null;
423 }
424
425 @Override
426 protected void updateContributedRulerColumns(CompositeRuler ruler) {
427 // don't add anything to composite ruler
428 }
429
430
431
432
433 protected class SessionLineStartAction extends LineStartAction {
434 protected boolean doSelect;
435
436 public SessionLineStartAction(StyledText textWidget, boolean doSelect) {
437 super(textWidget, doSelect);
438 this.doSelect = doSelect;
439 }
440
441 public void run() {
442 boolean isSmartHomeEndEnabled= false;
443 IPreferenceStore store= getPreferenceStore();
444 if (store != null)
445 isSmartHomeEndEnabled= store.getBoolean(AbstractTextEditor.PREFERENCE_NAVIGATION_SMART_HOME_END);
446
447 //StyledText text= sv.getTextWidget();
448 if (text == null || text.isDisposed())
449 return;
450
451 int caretOffset= text.getCaretOffset();
452 int lineNumber= text.getLineAtOffset(caretOffset);
453 int lineOffset= text.getOffsetAtLine(lineNumber);
454
455 int lineLength;
456 int caretOffsetInDocument;
457 int immediateOffset;
458
459 try {
460 caretOffsetInDocument= widgetOffset2ModelOffset(sv, caretOffset);
461 lineLength= model.getLineInformationOfOffset(caretOffsetInDocument).getLength();
462
463 immediateOffset = modelOffset2WidgetOffset(sv, model.dumpLength + 1);
464 } catch (BadLocationException ex) {
465 return;
466 }
467
468 String line= ""; //$NON-NLS-1$
469 if (lineLength > 0) {
470 int end= lineOffset + lineLength - 1;
471 end= Math.min(end, text.getCharCount() -1);
472 line= text.getText(lineOffset, end);
473 }
474
475 // Compute the line start offset
476 int index= getLineStartPosition(model, line, lineLength, caretOffsetInDocument);
477
478 // Remember current selection
479 Point oldSelection= text.getSelection();
480
481 // Compute new caret position
482 int newCaretOffset= -1;
483 if (lineOffset < immediateOffset && lineOffset+lineLength >= immediateOffset) {
484 if (caretOffset == immediateOffset)
485 // to beginning of line
486 newCaretOffset= lineOffset;
487 else
488 // to beginning of immediate
489 newCaretOffset= immediateOffset;
490 } else {
491 if (isSmartHomeEndEnabled) {
492 if (caretOffset - lineOffset == index)
493 // to beginning of line
494 newCaretOffset= lineOffset;
495 else
496 // to beginning of text
497 newCaretOffset= lineOffset + index;
498 } else {
499 if (caretOffset > lineOffset)
500 // to beginning of line
501 newCaretOffset= lineOffset;
502 }
503 }
504
505 if (newCaretOffset == -1)
506 newCaretOffset= caretOffset;
507 else
508 text.setCaretOffset(newCaretOffset);
509
510 if (doSelect) {
511 if (caretOffset < oldSelection.y)
512 text.setSelection(oldSelection.y, newCaretOffset);
513 else
514 text.setSelection(oldSelection.x, newCaretOffset);
515 } else
516 text.setSelection(newCaretOffset);
517
518 fireSelectionChanged(oldSelection);
519 }
520 }
521
522 protected void createActions() {
523 super.createActions();
524 IAction action;
525 action= new SessionLineStartAction(text, false);
526 action.setActionDefinitionId(ITextEditorActionDefinitionIds.LINE_START);
527 setAction(ITextEditorActionDefinitionIds.LINE_START, action);
528
529 action= new SessionLineStartAction(text, true);
530 action.setActionDefinitionId(ITextEditorActionDefinitionIds.SELECT_LINE_START);
531 setAction(ITextEditorActionDefinitionIds.SELECT_LINE_START, action);
532 }
533
534 protected void initializeKeyBindingScopes() {
535 setKeyBindingScopes(new String[] {
536 "acl2s.plugin.editors.session.context",
537 "org.eclipse.ui.textEditorScope"
538 });
539 }
540
541 private boolean sessionReady() {
542 switch (model.getManager().getStatus()) {
543 case ISessionStatusListener.READY_CMD_SESSION:
544 case ISessionStatusListener.READY_MISC_SESSION:
545 return true;
546 default:
547 return false;
548 }
549 }
550
551 public void verifyText(final VerifyEvent e) {
552 int max = model.readOnlyPoint();
553 if (!sessionReady()) {
554 e.doit = false;
555 return;
556 }
557 int end = widgetOffset2ModelOffset(sv, e.end);
558 int start = widgetOffset2ModelOffset(sv, e.start);
559 if (end < max || start < max) {
560 e.doit = false;
561 if (end < max) {
562 display.asyncExec(new Runnable() {
563 public void run() {
564 model.replace2(model.getLength(),0,e.text);
565 gotoEnd();
566 }
567 });
568 }
569 return;
570 }
571 }
572
573 public void verifyKey(VerifyEvent e) {
574 if (e.keyCode == '\r' || e.keyCode == '\n') {
575 if (e.stateMask == 0) {
576 Shell parent = getEditorSite().getShell();
577
578 if (getDocCaret() >= model.getLength() ?
579 InteractionPrefs.getEnterAttemptSubmitEnd(parent, model) :
580 InteractionPrefs.getEnterAttemptSubmitMiddle(parent, model)) {
581 if (model.trySubmitImmediate(this)) {
582 e.doit = false;
583 return;
584 }
585 }
586 if (!InteractionPrefs.getEnterInsert(parent, model)) {
587 e.doit = false;
588 return;
589 }
590 } else if (e.stateMask == SWT.SHIFT) {
591 // always insert literal newline
592 // no-op here; let it fall through
593 } else {
594 // always try submitting
595 e.doit = false;
596 model.trySubmitImmediate(this);
597 return;
598 }
599 }
600 super.verifyKey(e);
601 }
602
603 public boolean isSaveAsAllowed() {
604 return false;
605 }
606
607
608
609 /*========================= initialization stuff ==========================*/
610 public void init(IEditorSite site, IEditorInput input) throws PartInitException {
611 ssvc = new SessionSourceViewerConfiguration(this);
612 setSourceViewerConfiguration(ssvc);
613 setDocumentProvider(Acl2sPlugin.getA2sDocumentProvider());
614 super.init(site,input);
615 }
616
617 protected void preSetInput(IEditorInput input) throws CoreException {
618 Acl2sPlugin.newA2sEditorInput(input);
619 }
620
621 protected void postSetInput(IEditorInput input) throws CoreException {
622 model = (SessionDocument) (getDocumentProvider().getDocument(input));
623 model.getManager().addSessionStatusListener(this);
624 model.addDocumentListener(this);
625 model.addDescriptionListener(this);
626 ssvc.setDoc(model);
627 //if (text != null) System.err.println(text.getCharCount());
628 }
629
630 public void dispose() {
631 if (!text.isDisposed()) {
632 text.removeVerifyListener(this);
633 }
634 //model.getManager().removeSessionStatusListener(this);
635 model.removeDocumentListener(this);
636 model.removeDescriptionListener(this);
637 super.dispose();
638 Acl2sPlugin.disconnectedFrom(model);
639 }
640
641 /*========================= viewport stuff ==========================*/
642 protected int viewport;
643
644 public static final int VIEWPORT_ALL = 0;
645 public static final int VIEWPORT_LAST_SESSION = 1;
646 public static final int VIEWPORT_LAST_FAILED_PROOF = 2;
647 public static final int VIEWPORT_LAST_PROOF = 3;
648 public static final int VIEWPORT_LAST_INPUT = 4;
649
650 public void setViewport(int type) {
651 viewport = type;
652 updateViewport();
653 }
654
655 public void updateViewport() {
656 if (viewport == VIEWPORT_ALL) {
657 sv.resetVisibleRegion();
658 } else {
659 int first = model.countCompletedCmds();
660 while (first > 0 &&
661 !(model.getInput(first-1) instanceof StartupInputAndEnv) &&
662 (model.getStatus(first-1).wasSuccess() ||
663 model.getProofTree(first-1).length() == 0)) {
664 first--;
665 }
666 int start = model.getOffsetOfModelIdx(first);
667 sv.setVisibleRegion(start, model.getLength() - start);
668 }
669 }
670
671 /*======================= status change stuff =======================*/
672
673 public void sessionStatusChanged(final int status) {
674 //resetUndoStuff();
675 if (sv != null) updateViewport();
676 if (status == BUSY_SESSION &&
677 SessionPrefs.getTrackEndPref(getEditorSite().getShell(), model) == SessionPrefs.TRACK_END_JUMP) {
678 gotoEnd();
679 }
680 }
681
682
683 /*==================== document listening ======================*/
684 public void documentAboutToBeChanged(DocumentEvent event) {
685 gotoEnd = (event.getOffset() == model.dumpLength) && atEnd();
686 }
687
688 protected boolean atEnd() {
689 try {
690 int readOnly = model.readOnlyPoint();
691 if (readOnly <= 1) return true;
692 int caret = getDocCaret();
693 if (caret >= readOnly) return true;
694 int cline = model.getLineOfOffset(caret);
695 int rline = model.getLineOfOffset(readOnly-1);
696 return cline >= rline;
697 } catch (BadLocationException e) {
698 // nada
699 return true;
700 }
701 }
702
703 public void documentChanged(DocumentEvent event) {
704 if (gotoEnd) {
705 gotoEnd();
706 }
707 }
708
709
710
711 /*========================== actions ============================*/
712 public void cleanSessionAction() {
713 model.cleanSession(this);
714 }
715
716 public void forgetRedoAction() {
717 model.forgetRedo(this);
718 }
719
720 public void restartSessionAction() {
721 model.restartSession(this);
722 }
723
724 public void interruptSessionAction() {
725 model.interruptSession(this);
726 }
727
728 public void killSessionAction() {
729 model.killSession(this);
730 }
731
732 protected boolean warnOnNoPeer() {
733 if (model.getPeer() == null) {
734 infoMessageBox("No associated source file",
735 "The requested action is not available because this " +
736 "session has no associated source file.");
737 return true;
738 } else {
739 return false;
740 }
741 }
742
743 public void advanceTodoAction() {
744 if (warnOnNoPeer()) return;
745 model.getPeer().advanceTodo(this);
746 }
747
748 public void allTodoAction() {
749 if (warnOnNoPeer()) return;
750 model.getPeer().allTodo(this);
751 }
752
753 public void cancelTodoAction() {
754 if (warnOnNoPeer()) return;
755 model.getPeer().cancelTodo(this);
756 }
757
758 public void retreatLineAction() {
759 if (warnOnNoPeer()) return;
760 model.getPeer().retreatLine(this);
761 }
762
763 public void resetLineAction() {
764 if (warnOnNoPeer()) return;
765 model.getPeer().resetLineAndTodo(this);
766 }
767
768
769 public void navigatePrevInputAction() {
770 text.setCaretOffset(model.getPrevInputIdx(text.getCaretOffset()));
771 text.showSelection();
772 }
773
774 public void navigateNextInputAction() {
775 text.setCaretOffset(model.getNextInputIdx(text.getCaretOffset()));
776 text.showSelection();
777 }
778
779 public void navigatePrevCheckpointAction() {
780 text.setCaretOffset(model.getPrevCheckpointIdx(text.getCaretOffset()));
781 text.showSelection();
782 }
783
784 public void navigateNextCheckpointAction() {
785 text.setCaretOffset(model.getNextCheckpointIdx(text.getCaretOffset()));
786 text.showSelection();
787 }
788
789 public void prevCmdAction() {
790 if (!sessionReady()) return;
791 model.cmdPrevious();
792 gotoEnd();
793 }
794
795 public void nextCmdAction() {
796 if (!sessionReady()) return;
797 model.cmdNext();
798 gotoEnd();
799 }
800
801 public void lastCmdAction() {
802 if (!sessionReady()) return;
803 model.cmdLast();
804 gotoEnd();
805 }
806
807 public void suckCmdAction() {
808 if (warnOnNoPeer()) return;
809 if (!sessionReady()) return;
810 String sucked = model.getPeer().suckForm(this);
811 if (sucked == null) return;
812 model.cmdLast();
813 model.replaceImmediate(sucked);
814 gotoEnd();
815 }
816
817 public void lowercaseSexpAction() {
818 LispTokens toks = model.getTokens();
819 IRegion sel = getSelectedRegion();
820 if (sel.getLength() == 0) {
821 toks.lowercaseFromOffset(sel.getOffset());
822 } else {
823 toks.lowercaseRegion(sel);
824 }
825 }
826
827 public void expandSexpSelectionAction() {
828 IRegion r = getSelectedRegion();
829 setSelectedRegion(model.getTokens().expandSelection(r));
830 }
831
832
833 //changed by harshrc
834 //to navigate checkpoint to the subgoal, thus
835 public void navigateToCheckpoint(int modelIdx, String withGoal, boolean focus) {
836 int off2 = model.findCheckpointOffset(modelIdx, withGoal);
837 String goalname = "^^illegal-goal-name^^"; //initialise
838 //String outputstr = model.getOutput(modelIdx);
839
840 //the following if-else code fragment determines the exact name of the goal
841 if (modelIdx == model.done.size()) {
842 for (int i = 0; i < model.cur.chkptNames.size(); i++) {
843 if (withGoal.contains(model.cur.chkptNames.get(i)) &&
844 withGoal.contains(model.cur.chkptNames.get(i) + " ")) {
845 goalname = model.cur.chkptNames.get(i);
846 break;
847 }
848 }
849 }
850 else {
851 DoneElement e = model.done.get(modelIdx);
852 for (int i = 0; i < e.chkptNames.length; i++) {
853 if (withGoal.contains(e.chkptNames[i]) &&
854 withGoal.contains(e.chkptNames[i] + " ")) {
855 goalname = e.chkptNames[i];
856 break;
857 }
858 }
859 }
860
861 //reverse search for goal name in entire text, this gives the correct offset in the session output.
862 //but ideally TODO: Just to reverse search in the cur element output and then add to it the rest
863 //of the relative to the origin of output offset.
864 //int off3 = model.getOutput(modelIdx).lastIndexOf(goalname, off2); //reverse search for goal name
865 //int off4 = off3 + model.getOffsetOfModelIdx(modelIdx);
866 int off = -1; //init
867 if (withGoal.contains("INDUCT"))
868 off = off2; //if it containts INDUCT, then current checkpointing output is fine
869 else
870 off = model.get().lastIndexOf(goalname, off2); //o.w get the first occurrence in reverse search
871
872 if (off >= 0) {
873 try {
874 int line = model.getLineOfOffset(off);
875 int llen = model.getLineLength(line);
876 setSelectedRegion(new Region(off,llen-1));
877 revealRange(off,llen);
878 } catch (BadLocationException e) {
879 // impossible, but whatever
880 setDocCaret(off);
881 revealRange(off,0);
882 }
883 }
884 if (focus) setFocus();
885 }
886
887 public void cleanOutputFilesAction() {
888 if (warnOnNoPeer()) return;
889 model.getPeer().cleanOutputFiles(this);
890 }
891
892 public void cleanCmdHistAction() {
893 model.cleanCmdHist();
894 }
895 }