package acl2s.plugin.editors.session;
	
	import org.eclipse.core.runtime.CoreException;
	import org.eclipse.jface.action.IAction;
	import org.eclipse.jface.preference.IPreferenceStore;
	import org.eclipse.jface.resource.ColorRegistry;
	import org.eclipse.jface.text.BadLocationException;
	import org.eclipse.jface.text.DocumentEvent;
	import org.eclipse.jface.text.IDocumentListener;
	import org.eclipse.jface.text.IRegion;
	import org.eclipse.jface.text.Region;
	import org.eclipse.jface.text.source.CompositeRuler;
	import org.eclipse.jface.text.source.IOverviewRuler;
	import org.eclipse.jface.text.source.ISharedTextColors;
	import org.eclipse.jface.viewers.DoubleClickEvent;
	import org.eclipse.jface.viewers.IColorProvider;
	import org.eclipse.jface.viewers.IDoubleClickListener;
	import org.eclipse.jface.viewers.ILabelProvider;
	import org.eclipse.jface.viewers.ILabelProviderListener;
	import org.eclipse.jface.viewers.ISelection;
	import org.eclipse.jface.viewers.IStructuredSelection;
	import org.eclipse.jface.viewers.ITreeContentProvider;
	import org.eclipse.jface.viewers.SelectionChangedEvent;
	import org.eclipse.jface.viewers.StructuredSelection;
	import org.eclipse.jface.viewers.TreeViewer;
	import org.eclipse.jface.viewers.Viewer;
	import org.eclipse.swt.SWT;
	import org.eclipse.swt.custom.StyledText;
	import org.eclipse.swt.events.VerifyEvent;
	import org.eclipse.swt.events.VerifyListener;
	import org.eclipse.swt.graphics.Color;
	import org.eclipse.swt.graphics.Image;
	import org.eclipse.swt.graphics.Point;
	import org.eclipse.swt.widgets.Composite;
	import org.eclipse.swt.widgets.Display;
	import org.eclipse.swt.widgets.Shell;
	import org.eclipse.ui.IEditorInput;
	import org.eclipse.ui.IEditorSite;
	import org.eclipse.ui.PartInitException;
	import org.eclipse.ui.texteditor.AbstractTextEditor;
	import org.eclipse.ui.texteditor.ITextEditorActionDefinitionIds;
	import org.eclipse.ui.views.contentoutline.ContentOutlinePage;
	import org.eclipse.ui.views.contentoutline.IContentOutlinePage;
	
	import acl2s.lib.session.IStatusInfo;
	import acl2s.plugin.Acl2sPlugin;
	import acl2s.plugin.IPeerDocument;
	import acl2s.plugin.ISessionDocument;
	import acl2s.plugin.editors.A2sEditor;
	import acl2s.plugin.editors.session.SessionDocument.DoneElement;
	import acl2s.plugin.misc.Colors;
	import acl2s.plugin.parse.LispTokens;
	import acl2s.plugin.prefs.InteractionPrefs;
	import acl2s.plugin.prefs.SessionPrefs;
	import acl2s.uilib.cmd.ResolvedInput;
	import acl2s.uilib.session.IInputInfo;
	import acl2s.uilib.session.ISessionStatusListener;
	import acl2s.uilib.session.RedoInput;
	import acl2s.uilib.session.StartupInputAndEnv;
	import acl2s.uilib.session.UndoInput;
	
	public class SessionEditor extends A2sEditor
	implements ISessionStatusListener, VerifyListener, IDocumentListener {
		public static final String id = "acl2s.plugin.editors.session";
		
		protected final Display display = Display.getDefault();
		protected SessionSourceViewerConfiguration ssvc = null;
		protected SessionDocument model = null;
		protected boolean gotoEnd = false;
		protected SessionContentOutlinePage outlinePage = null;
		
		/*========================== some accessors ==========================*/
		public SessionDocument getDocument() {
			return model;
		}
		
		public IPeerDocument getPeerDocument() {
			return getDocument().getPeer();
		}
	
		public ISessionDocument getSessionDocument() {
			return model;
		}
	
		/*======================= outline view support =======================*/
	
		protected class SessionContentOutlinePage extends ContentOutlinePage
		implements ITreeContentProvider, ILabelProvider, IColorProvider, 
		           IDoubleClickListener, IDocumentListener {
			ColorRegistry colorReg = Acl2sPlugin.getDefault().getWorkbench().getThemeManager().getCurrentTheme().getColorRegistry();
			int completedSeen = 0;
			boolean curHasInput = false;
			
			@Override
			public void createControl(Composite parent) {
				super.createControl(parent);
				model.addDocumentListener(this);
				TreeViewer tv = getTreeViewer();
				tv.setLabelProvider(this);
				tv.setContentProvider(this);
				tv.setInput(model);
				tv.addDoubleClickListener(this);
				update();
			}
			
			@Override
			public void dispose() {
				Acl2sPlugin.maybeWarnOutline3_3();
				TreeViewer tv = getTreeViewer();
				tv.removeDoubleClickListener(this);
				model.removeDocumentListener(this);
				super.dispose();
			}
	
			public void documentAboutToBeChanged(DocumentEvent event) { }
	
			public void documentChanged(DocumentEvent event) {
				update();
			}
	
			public void update() {
				int nowCompleted = model.countCompletedCmds();
				if (nowCompleted == completedSeen) {
					if ((model.cur.input != null) != curHasInput) {
						getTreeViewer().update(new Integer(completedSeen), null);
					}
					return;
				}
				final TreeViewer tv = getTreeViewer();
				if (nowCompleted < completedSeen || completedSeen == 0) {
					completedSeen = nowCompleted;
					tv.refresh();
					Acl2sPlugin.getDisplay().asyncExec(outlineUpdaterForCursor);
					return;
				}
				// otherwise, try to do incremental update
				tv.update(new Integer(completedSeen), null);
				do {
					completedSeen++;
					tv.add(tv.getInput(), new Integer(completedSeen));
				} while (completedSeen < nowCompleted);
				Acl2sPlugin.getDisplay().asyncExec(outlineUpdaterForCursor);
			}
			
			public Object[] getElements(Object inputElement) {
				Object[] elts = new Object[completedSeen+1];
				for (int i = 0; i <= completedSeen; i++) {
					elts[i] = new Integer(i);
				}
				return elts;
			}
	
			Image img_event_very_bad = Acl2sPlugin.getImage("icons/event_very_bad.gif");
			Image img_event_bad =      Acl2sPlugin.getImage("icons/event_bad.gif");
			Image img_compute_bad =    Acl2sPlugin.getImage("icons/compute_bad.gif");
			Image img_inspect_bad =    Acl2sPlugin.getImage("icons/inspect_bad.gif");
	
			Image img_compute =        Acl2sPlugin.getImage("icons/compute.gif");
			Image img_inspect =        Acl2sPlugin.getImage("icons/inspect.gif");
			Image img_event_compute =  Acl2sPlugin.getImage("icons/event_compute.gif");
			Image img_event =          Acl2sPlugin.getImage("icons/event.gif");
			Image img_book_open =      Acl2sPlugin.getImage("icons/book_open.gif");
			Image img_pkg_open =       Acl2sPlugin.getImage("icons/pkg_open.gif");
			Image img_event_gear =     Acl2sPlugin.getImage("icons/event_gear.gif");
			Image img_event_unknown =  Acl2sPlugin.getImage("icons/event_unknown.gif");
	
			Image img_redo =           Acl2sPlugin.getImage("icons/redo.gif");
			Image img_undo =           Acl2sPlugin.getImage("icons/undo.gif");
	
			
			public Image getImage(Object element) {
				if (element instanceof Integer) {
					int idx = ((Integer)element).intValue();
					IInputInfo input = model.getInput(idx);
					if (input == null) {
						return null;
					}
					String typeStr = input.getInputTypeString();
					if (typeStr == null) {
						return null;
					}
					if (typeStr.equals("BAD")) {
						return img_event_very_bad;
					}
					//IStatusInfo status = model.getStatus(idx);
					if (input instanceof ResolvedInput) {
						ResolvedInput input2 = (ResolvedInput)input;
						//if (status.wasSuccess()) {
							switch (input2.getType()) {
							case ResolvedInput.VALUE:
								return img_compute;
							case ResolvedInput.QUERY:
								return img_inspect;
							case ResolvedInput.VALTRIP:
								return img_event_compute;
							case ResolvedInput.EVENT:
								return img_event;
							case ResolvedInput.BEGIN_BOOK:
								return img_book_open;
							case ResolvedInput.IN_PACKAGE:
								return img_pkg_open;
							case ResolvedInput.COMMAND:
								return img_event_gear;
							case ResolvedInput.ACTION:
							case ResolvedInput.RAW:
							default:
								return img_event_unknown;
							}
						/*
						} else {
							switch (input2.getType()) {
							case ResolvedInput.VALUE:
								return img_compute_bad;
							case ResolvedInput.QUERY:
								return img_inspect_bad;
							case ResolvedInput.VALTRIP:
							case ResolvedInput.EVENT:
							case ResolvedInput.BEGIN_BOOK:
							case ResolvedInput.IN_PACKAGE:
							case ResolvedInput.COMMAND:
							case ResolvedInput.ACTION:
							case ResolvedInput.RAW:
							default:
								return img_event_bad;
							}
						}*/
					}
					if (input instanceof RedoInput) {
						return img_redo;
					}
					if (input instanceof UndoInput) {
						return img_undo;
					}
				}
				// otherwise
				return null;
			}
	
			public String getText(Object element) {
				if (element instanceof Integer) {
					int idx = ((Integer)element).intValue();
					IInputInfo input = model.getInput(idx);
					if (input == null) {
						if (idx == completedSeen) {
							return "<prompt>";
						} else {
							return "<session beginning>";
						}
					} else {
						String inputStr = input.getInputString();
						if (inputStr == null) {
							return "<session startup>";
						} else {
							return firstLine(inputStr);
						}
					}
				} else {
					return null;
				}
			}
	
	
			public Color getBackground(Object element) {
				return null;
			}
	
			public Color getForeground(Object element) {
				if (element instanceof Integer) {
					int idx = ((Integer)element).intValue();
					if (idx < model.countCompletedCmds()) {
						IStatusInfo status = model.getStatus(idx);
						if (status != null) {
							if (status.wasSuccess()) {
								return colorReg.get("acl2s.plugin.color.output");
							} else {
								return colorReg.get("acl2s.plugin.color.outputerr");
							}
						}
					}
				}
				return Colors.BLACK;
			}
			
			public void doubleClick(DoubleClickEvent event) {
				Object src = ((IStructuredSelection)event.getSelection()).getFirstElement();
				if (src instanceof Integer) {
					int midx = ((Integer)src).intValue();
					if (midx < completedSeen || curHasInput) {
						setDocCaret(model.getOffsetOfModelIdx(midx));
					} else {
						setDocCaret(model.readOnlyPoint());
					}
					SessionEditor.this.setFocus();
				}
			}
			
			@Override
			public void selectionChanged(SelectionChangedEvent event) {
				super.selectionChanged(event);
				if (!inReverseSelect) {
					Object src = ((IStructuredSelection)event.getSelection()).getFirstElement();
					if (src instanceof Integer) {
						revealRange(model.getOffsetOfModelIdx(((Integer)src).intValue()),1);
					}
				}
			}
			
			boolean inReverseSelect = false;
			
			public void select(final int midx) {
				TreeViewer tv = getTreeViewer();
				ISelection s = tv.getSelection();
				if (s instanceof IStructuredSelection) {
					IStructuredSelection ss = (IStructuredSelection) s;

					Object sel = new Integer(midx);
					if (!ss.toList().contains(sel)) {
						inReverseSelect = true;
						tv.setSelection(new StructuredSelection(sel), true);
						inReverseSelect = false;
					}
				}
			}
			
			public Object getParent(Object element) { return null; }
	
			public Object[] getChildren(Object parentElement) { return emptyArray; }
	
			public boolean hasChildren(Object element) { return false; }
	
			public void inputChanged(Viewer viewer, Object oldInput, Object newInput) { }
	
			public boolean isLabelProperty(Object element, String property) { return false; }
	
			public void addListener(ILabelProviderListener listener) { }
	
			public void removeListener(ILabelProviderListener listener) { }
		}
	
		static final Object[] emptyArray = new Object[0];
	
		static String firstLine(String str) {
			int returnPos = str.indexOf('\r');
			int newlinePos = str.indexOf('\n');
			if (returnPos >= 0) {
				if (newlinePos >= 0 && newlinePos < returnPos) {
					return str.substring(0, newlinePos);
				}
				return str.substring(0, returnPos);
			} else {
				if (newlinePos >= 0) {
					return str.substring(0, newlinePos);
				} else {
					return str;
				}
			}
		}
	
		protected Runnable outlineUpdaterForCursor = new Runnable() {
			public void run() {
				try {
					if (outlinePage != null) {
						int midx = model.getModelIdxOfOffset(getDocCaret());
						outlinePage.select(midx);
					}
				} finally {
					outlineUpdaterPending = false;
				}
			}
		};
	
		private boolean outlineUpdaterPending = false; 
		
		@Override
		protected void handleCursorPositionChanged() {
			super.handleCursorPositionChanged();
			if (outlinePage != null && !outlineUpdaterPending) {
				Acl2sPlugin.getDisplay().asyncExec(outlineUpdaterForCursor);
				outlineUpdaterPending = true;
			}
		}
	
		@SuppressWarnings("unchecked") // Eclipse complains without this
		@Override
		public Object getAdapter(Class adapter) {
			if (adapter == IContentOutlinePage.class) {
				if (outlinePage == null) {
					outlinePage = new SessionContentOutlinePage();
				}
				return outlinePage;
			}
			return super.getAdapter(adapter);
		}
	
		
	
		/*======================= make the thing read-only ==================*/
		protected void setupSourceViewer() {
			super.setupSourceViewer();
			text.addVerifyListener(this);
			setViewport(VIEWPORT_ALL);
		}
	
		public void createPartControl(Composite parent) {
			super.createPartControl(parent);
			gotoEnd();
		}
	
		
		/*===================== get rid of vertical rulers ==================*/
		protected boolean isLineNumberRulerVisible() { return false; }
	
		protected boolean isPrefQuickDiffAlwaysOn() { return false; }
	
		protected CompositeRuler createCompositeRuler() {
			CompositeRuler ruler= new CompositeRuler();
			return ruler;
		}
	
		protected boolean isOverviewRulerVisible() { return false; }
		
		protected IOverviewRuler createOverviewRuler(ISharedTextColors sharedColors) {
			return null;
		}
	
		@Override
		protected void updateContributedRulerColumns(CompositeRuler ruler) {
			// don't add anything to composite ruler
		}
	
	
	
	
		protected class SessionLineStartAction extends LineStartAction {
			protected boolean doSelect;
			
			public SessionLineStartAction(StyledText textWidget, boolean doSelect) {
				super(textWidget, doSelect);
				this.doSelect = doSelect;
			}
	
			public void run() {
				boolean isSmartHomeEndEnabled= false;
				IPreferenceStore store= getPreferenceStore();
				if (store != null)
					isSmartHomeEndEnabled= store.getBoolean(AbstractTextEditor.PREFERENCE_NAVIGATION_SMART_HOME_END);
	
				//StyledText text= sv.getTextWidget();
				if (text == null || text.isDisposed())
					return;
	
				int caretOffset= text.getCaretOffset();
				int lineNumber= text.getLineAtOffset(caretOffset);
				int lineOffset= text.getOffsetAtLine(lineNumber);
	
				int lineLength;
				int caretOffsetInDocument;
				int immediateOffset;
				
				try {
					caretOffsetInDocument= widgetOffset2ModelOffset(sv, caretOffset);
					lineLength= model.getLineInformationOfOffset(caretOffsetInDocument).getLength();
					
					immediateOffset = modelOffset2WidgetOffset(sv, model.dumpLength + 1);
				} catch (BadLocationException ex) {
					return;
				}
	
				String line= ""; //$NON-NLS-1$
				if (lineLength > 0) {
					int end= lineOffset + lineLength - 1;
					end= Math.min(end, text.getCharCount() -1);
					line= text.getText(lineOffset, end);
				}
	
				// Compute the line start offset
				int index= getLineStartPosition(model, line, lineLength, caretOffsetInDocument);
	
				// Remember current selection
				Point oldSelection= text.getSelection();
	
				// Compute new caret position
				int newCaretOffset= -1;
				if (lineOffset < immediateOffset && lineOffset+lineLength >= immediateOffset) {
						if (caretOffset == immediateOffset)
							// to beginning of line
							newCaretOffset= lineOffset;
						else
							// to beginning of immediate
							newCaretOffset= immediateOffset;
				} else {
					if (isSmartHomeEndEnabled) {
						if (caretOffset - lineOffset == index)
							// to beginning of line
							newCaretOffset= lineOffset;
						else
							// to beginning of text
							newCaretOffset= lineOffset + index;
					} else {
						if (caretOffset > lineOffset)
							// to beginning of line
							newCaretOffset= lineOffset;
					}
				}
	
				if (newCaretOffset == -1)
					newCaretOffset= caretOffset;
				else
					text.setCaretOffset(newCaretOffset);
	
				if (doSelect) {
					if (caretOffset < oldSelection.y)
						text.setSelection(oldSelection.y, newCaretOffset);
					else
						text.setSelection(oldSelection.x, newCaretOffset);
				} else
					text.setSelection(newCaretOffset);
	
				fireSelectionChanged(oldSelection);
			}
		}
		
		protected void createActions() {
			super.createActions();
			IAction action;
			action= new SessionLineStartAction(text, false);
			action.setActionDefinitionId(ITextEditorActionDefinitionIds.LINE_START);
			setAction(ITextEditorActionDefinitionIds.LINE_START, action);
	
			action= new SessionLineStartAction(text, true);
			action.setActionDefinitionId(ITextEditorActionDefinitionIds.SELECT_LINE_START);
			setAction(ITextEditorActionDefinitionIds.SELECT_LINE_START, action);
		}
	
		protected void initializeKeyBindingScopes() {
			setKeyBindingScopes(new String[] {
					"acl2s.plugin.editors.session.context",
					"org.eclipse.ui.textEditorScope"
			});
		}
	
		private boolean sessionReady() {
			switch (model.getManager().getStatus()) {
			case ISessionStatusListener.READY_CMD_SESSION:
			case ISessionStatusListener.READY_MISC_SESSION:
				return true;
			default:
				return false;
			}
		}
		
		public void verifyText(final VerifyEvent e) {
			int max = model.readOnlyPoint();
			if (!sessionReady()) {
				e.doit = false;
				return;
			}
			int end = widgetOffset2ModelOffset(sv, e.end);
			int start = widgetOffset2ModelOffset(sv, e.start);
			if (end < max || start < max) {
				e.doit = false;
				if (end < max) {
					display.asyncExec(new Runnable() {
						public void run() {
							model.replace2(model.getLength(),0,e.text);
							gotoEnd();
						}
					});
				}
				return;
			}
		}
	
		public void verifyKey(VerifyEvent e) {
			if (e.keyCode == '\r' || e.keyCode == '\n') {
				if (e.stateMask == 0) {
					Shell parent = getEditorSite().getShell();
					
					if (getDocCaret() >= model.getLength() ?
							InteractionPrefs.getEnterAttemptSubmitEnd(parent, model) :
								InteractionPrefs.getEnterAttemptSubmitMiddle(parent, model)) {
						if (model.trySubmitImmediate(this)) {
							e.doit = false;
							return;
						}
					}
					if (!InteractionPrefs.getEnterInsert(parent, model)) {
						e.doit = false;
						return;
					}
				} else if (e.stateMask == SWT.SHIFT) {
					// always insert literal newline
					// no-op here; let it fall through
				} else {
					// always try submitting
					e.doit = false;
					model.trySubmitImmediate(this);
					return;
				} 
			}
			super.verifyKey(e);
		}
		
		public boolean isSaveAsAllowed() {
			return false;
		}
		
	
	
		/*========================= initialization stuff ==========================*/
		public void init(IEditorSite site, IEditorInput input) throws PartInitException {
			ssvc = new SessionSourceViewerConfiguration(this);
			setSourceViewerConfiguration(ssvc);
			setDocumentProvider(Acl2sPlugin.getA2sDocumentProvider());
			super.init(site,input);
		}
	
		protected void preSetInput(IEditorInput input) throws CoreException {
			Acl2sPlugin.newA2sEditorInput(input);
		}
	
		protected void postSetInput(IEditorInput input) throws CoreException {
			model = (SessionDocument) (getDocumentProvider().getDocument(input));
			model.getManager().addSessionStatusListener(this);
			model.addDocumentListener(this);
			model.addDescriptionListener(this);
			ssvc.setDoc(model);
			//if (text != null) System.err.println(text.getCharCount());
		}
	
		public void dispose() {
			if (!text.isDisposed()) {
				text.removeVerifyListener(this);
			}
			//model.getManager().removeSessionStatusListener(this);
			model.removeDocumentListener(this);
			model.removeDescriptionListener(this);
			super.dispose();
			Acl2sPlugin.disconnectedFrom(model);
		}
	
		/*========================= viewport stuff ==========================*/
		protected int viewport;
		
		public static final int VIEWPORT_ALL = 0;
		public static final int VIEWPORT_LAST_SESSION = 1;
		public static final int VIEWPORT_LAST_FAILED_PROOF = 2;
		public static final int VIEWPORT_LAST_PROOF = 3;
		public static final int VIEWPORT_LAST_INPUT = 4;
		
		public void setViewport(int type) {
			viewport = type;
			updateViewport();
		}
		
		public void updateViewport() {
			if (viewport == VIEWPORT_ALL) {
				sv.resetVisibleRegion();
			} else {
				int first = model.countCompletedCmds();
				while (first > 0 &&
						!(model.getInput(first-1) instanceof StartupInputAndEnv) && 
						(model.getStatus(first-1).wasSuccess() ||
						 model.getProofTree(first-1).length() == 0)) {
					first--;
				}
				int start = model.getOffsetOfModelIdx(first);
				sv.setVisibleRegion(start, model.getLength() - start);
			}
		}
		
		/*======================= status change stuff =======================*/
		
		public void sessionStatusChanged(final int status) {
			//resetUndoStuff();
			if (sv != null) updateViewport();
			if (status == BUSY_SESSION && 
					SessionPrefs.getTrackEndPref(getEditorSite().getShell(), model) == SessionPrefs.TRACK_END_JUMP) {
				gotoEnd();
			}
		}
	    
		
		/*==================== document listening ======================*/
		public void documentAboutToBeChanged(DocumentEvent event) {
			gotoEnd = (event.getOffset() == model.dumpLength) && atEnd();
		}
		
		protected boolean atEnd() {
			try {
				int readOnly = model.readOnlyPoint();
				if (readOnly <= 1) return true;
				int caret = getDocCaret();
				if (caret >= readOnly) return true;
				int cline = model.getLineOfOffset(caret);
				int rline = model.getLineOfOffset(readOnly-1);
				return cline >= rline;
			} catch (BadLocationException e) {
				// nada
				return true;
			}
		}
	
		public void documentChanged(DocumentEvent event) {
			if (gotoEnd) {
				gotoEnd();
			}
		}
	
		
		
		/*========================== actions ============================*/
		public void cleanSessionAction() {
			model.cleanSession(this);
		}
	
		public void forgetRedoAction() {
			model.forgetRedo(this);
		}
	
		public void restartSessionAction() {
			model.restartSession(this);
		}
	
		public void interruptSessionAction() {
			model.interruptSession(this);
		}
	
		public void killSessionAction() {
			model.killSession(this);
		}
	
		protected boolean warnOnNoPeer() {
			if (model.getPeer() == null) {
				infoMessageBox("No associated source file",
						"The requested action is not available because this " +
						"session has no associated source file.");
				return true;
			} else {
				return false;
			}
		}
		
		public void advanceTodoAction() {
			if (warnOnNoPeer()) return;
			model.getPeer().advanceTodo(this);
		}
	
		public void allTodoAction() {
			if (warnOnNoPeer()) return;
			model.getPeer().allTodo(this);
		}
	
		public void cancelTodoAction() {
			if (warnOnNoPeer()) return;
			model.getPeer().cancelTodo(this);
		}
	
		public void retreatLineAction() {
			if (warnOnNoPeer()) return;
			model.getPeer().retreatLine(this);
		}
	
		public void resetLineAction() {
			if (warnOnNoPeer()) return;
			model.getPeer().resetLineAndTodo(this);
		}
	
		
		public void navigatePrevInputAction() {
			text.setCaretOffset(model.getPrevInputIdx(text.getCaretOffset()));
			text.showSelection();
		}
		
		public void navigateNextInputAction() {
			text.setCaretOffset(model.getNextInputIdx(text.getCaretOffset()));
			text.showSelection();
		}
		
		public void navigatePrevCheckpointAction() {
			text.setCaretOffset(model.getPrevCheckpointIdx(text.getCaretOffset()));
			text.showSelection();
		}
		
		public void navigateNextCheckpointAction() {
			text.setCaretOffset(model.getNextCheckpointIdx(text.getCaretOffset()));
			text.showSelection();
		}
		
		public void prevCmdAction() {
			if (!sessionReady()) return;
			model.cmdPrevious();
			gotoEnd();
		}
		
		public void nextCmdAction() {
			if (!sessionReady()) return;
			model.cmdNext();
			gotoEnd();
		}
		
		public void lastCmdAction() {
			if (!sessionReady()) return;
			model.cmdLast();
			gotoEnd();
		}
		
		public void suckCmdAction() {
			if (warnOnNoPeer()) return;
			if (!sessionReady()) return;
			String sucked = model.getPeer().suckForm(this);
			if (sucked == null) return;
			model.cmdLast();
			model.replaceImmediate(sucked);
			gotoEnd();
		}
		
		public void lowercaseSexpAction() {
			LispTokens toks = model.getTokens();
			IRegion sel = getSelectedRegion();
			if (sel.getLength() == 0) {
				toks.lowercaseFromOffset(sel.getOffset());
			} else {
				toks.lowercaseRegion(sel);
			}
		}
	
		public void expandSexpSelectionAction() {
			IRegion r = getSelectedRegion();
			setSelectedRegion(model.getTokens().expandSelection(r));
		}
	
		
		//changed by harshrc
		//to navigate checkpoint to the subgoal, thus 
		public void navigateToCheckpoint(int modelIdx, String withGoal, boolean focus) {
			int off2 = model.findCheckpointOffset(modelIdx, withGoal);
			String goalname = "^^illegal-goal-name^^"; //initialise
			//String outputstr = model.getOutput(modelIdx);
			
			//the following if-else code fragment determines the exact name of the goal
			if (modelIdx == model.done.size()) {
				for (int i = 0; i < model.cur.chkptNames.size(); i++) {
					if (withGoal.contains(model.cur.chkptNames.get(i)) &&
							withGoal.contains(model.cur.chkptNames.get(i) + " ")) {
						goalname = model.cur.chkptNames.get(i); 
						break;
					}
				}
			} 
			else {
				DoneElement e = model.done.get(modelIdx);
				for (int i = 0; i < e.chkptNames.length; i++) {
					if (withGoal.contains(e.chkptNames[i]) &&
							withGoal.contains(e.chkptNames[i] + " ")) {
						goalname = e.chkptNames[i];
						break;
					}
				}	
			}
			
			//reverse search for goal name in entire text, this gives the correct offset in the session output.
			//but ideally TODO: Just to reverse search in the cur element output and then add to it the rest
			//of the relative to the origin of output offset.
			//int off3 = model.getOutput(modelIdx).lastIndexOf(goalname, off2); //reverse search for goal name
			//int off4 = off3 + model.getOffsetOfModelIdx(modelIdx);
			int off = -1; //init
			if (withGoal.contains("INDUCT"))
				off = off2; //if it containts INDUCT, then current checkpointing output is fine 
			else
				off = model.get().lastIndexOf(goalname, off2); //o.w get the first occurrence in reverse search
				
			if (off >= 0) {
				try {
					int line = model.getLineOfOffset(off);
					int llen = model.getLineLength(line);
					setSelectedRegion(new Region(off,llen-1));
					revealRange(off,llen);
				} catch (BadLocationException e) {
					// impossible, but whatever
					setDocCaret(off);
					revealRange(off,0);
				}
			}
			if (focus) setFocus();
		}
	
		public void cleanOutputFilesAction() {
			if (warnOnNoPeer()) return;
			model.getPeer().cleanOutputFiles(this);
		}
	
		public void cleanCmdHistAction() {
			model.cleanCmdHist();
		}
	}