package acl2s.plugin.editors.session;
	
	import java.io.ByteArrayInputStream;
	import java.io.ByteArrayOutputStream;
	import java.io.EOFException;
	import java.io.File;
	import java.io.IOException;
	import java.io.InputStream;
	import java.io.ObjectInputStream;
	import java.io.ObjectOutputStream;
	import java.io.Serializable;
	import java.util.ArrayList;
	
	import org.eclipse.jface.text.BadLocationException;
	import org.eclipse.jface.text.DocumentEvent;
	import org.eclipse.jface.text.IDocument;
	import org.eclipse.jface.text.IRegion;
	import org.eclipse.jface.text.ITypedRegion;
	import org.eclipse.jface.text.Region;
	import org.eclipse.swt.SWT;
	
	import acl2s.lib.parse.ParseException;
	import acl2s.lib.parse.StringParser;
	import acl2s.lib.parse.obj.LispObject;
	import acl2s.lib.parse.obj.Sym;
	import acl2s.lib.session.IEnvInfo;
	import acl2s.lib.session.IResultInfo;
	import acl2s.lib.session.IStatusInfo;
	import acl2s.lib.session.MyInteractiveSessionConfig;
	import acl2s.lib.session.SessionDeadException;
	import acl2s.lib.session.SessionException;
	import acl2s.lib.session.SessionMode;
	import acl2s.lib.session.SessionStateException;
	import acl2s.plugin.Acl2sPlugin;
	import acl2s.plugin.IPeerDocument;
	import acl2s.plugin.ISessionDocument;
	import acl2s.plugin.editors.A2sDocument;
	import acl2s.plugin.editors.A2sEditor;
	import acl2s.plugin.editors.AbstractDocumentPartitioner;
	import acl2s.plugin.editors.MyDocumentProvider;
	import acl2s.plugin.editors.MyTypedRegion;
	import acl2s.plugin.editors.lisp.LineMode;
	import acl2s.plugin.prefs.Acl2Prefs;
	import acl2s.plugin.prefs.InteractionPrefs;
	import acl2s.plugin.prefs.SessionPrefs;
	import acl2s.uilib.cmd.BadCmdException;
	import acl2s.uilib.cmd.ResolvableUserInput;
	import acl2s.uilib.cmd.ResolvedInput;
	import acl2s.uilib.cmd.UnresolvedKeywordCmd;
	import acl2s.uilib.cmd.WormholeWrappedInput;
	import acl2s.uilib.session.IInputInfo;
	import acl2s.uilib.session.ISessionClient;
	import acl2s.uilib.session.ISessionModel;
	import acl2s.uilib.session.ISessionStatusListener;
	import acl2s.uilib.session.InteractiveSessionManager;
	import acl2s.uilib.session.StartupInputAndEnv;
	
	public class SessionDocument extends A2sDocument
	implements ISessionModel, ISessionDocument, ISessionClient, ISessionStatusListener {
		public static final String ID = SessionDocument.class.getCanonicalName();
		
		protected static final char versionId = 19;
		
		protected IPeerDocument peer = null;
		protected MyInteractiveSessionConfig config = null;
		protected InteractiveSessionManager session = null;
	
		protected Partitioner partitioner;
	
		protected CurElement cur;
		protected final ArrayList<DoneElement> done;
		protected int dumpLength;
		protected int newDumpLength;
	
		protected final ArrayList<Integer> inputIdxs;
		protected final ArrayList<Integer> checkpointIdxs;
		
		protected final ArrayList<String> cmdHistory;
		protected int cmdPos;
		protected final ArrayList<String> miscHistory;
		protected int miscPos;
		
		public SessionDocument(MyDocumentProvider dp) {
			super(dp);
			
			//setTextStore(new StringBuilderTextStore());
			
			session = new InteractiveSessionManager(Acl2sPlugin.getDefault(),this,this);
	
			done = new ArrayList<DoneElement>();
			inputIdxs = new ArrayList<Integer>();
			checkpointIdxs = new ArrayList<Integer>();
	
			cmdHistory = new ArrayList<String>();
			cmdHistory.add("");
			cmdPos = 0;
			miscHistory = new ArrayList<String>();
			miscHistory.add("");
			miscPos = 0;
			
			tokens = new SessionDocumentLispTokens();
			tokens.connect(this);
			
			session.addSessionStatusListener(this);
			
			reset();
		}
		
		/*public void setInput(IFileEditorInput input) {
			this.input = input;
		}*/
		
		public void setPeer(IPeerDocument p) {
			peer = p;
			config.setMode(getAcl2Mode());
		}
	
		public IPeerDocument getPeer() { return peer; }
		
		public InteractiveSessionManager getManager() { return session; }
	
		public ISessionModel getModel() { return this; }
		
		//public int getDumpLength() { return dumpLength; }
		
		public int getNewDumpLength() { return newDumpLength; }
		
		public boolean appendingDump() { return newDumpLength > dumpLength; }
		
		public String getImmediate() {
			return get2(dumpLength+1,getLength()-dumpLength-1);
		}
		
		public int readOnlyPoint() { return dumpLength + 1; }
		
		public boolean allowReplace(int pos, int length, String text) {
			// currently dumping I/O
			if (appendingDump()) return true;
			
			// otherwise, status must be ready for input
			int status = session.getStatus();
			if (status != READY_CMD_SESSION && status != READY_MISC_SESSION) return false;
			
			// allow if in immediate region
			return (pos > dumpLength) ||
			
			// allow if updating separator & immediate (see UpdateSeparatorStrategy)
			       (pos == dumpLength && text.length() > 0 && Character.isWhitespace(text.charAt(0)));
		}
	
		public SessionDocumentProvider getProvider() {
			return Acl2sPlugin.getA2sDocumentProvider();
		}
		
		/*
		public File getProjectWorkingDir() {
			IPath p = getOSPath();
			IFile f = ResourcesPlugin.getWorkspace().getRoot().getFileForLocation(p);
			if (f == null) { // not in a project; return containing dir
				return p.toFile().getParentFile();
			} else {         // in a project; return project root
				return f.getProject().getLocation().toFile();
			}
		}*/
	
		public File getDesiredCBD() {
			File me = getOSFile();
			if (me == null) {
				return new File(System.getProperty("user.dir")); // best we can do
			} else {
				return me.getParentFile();
			}
		}
		
		public IInputInfo nextInputOption() {
			if (peer != null) {
				return peer.nextInputOption();
			} else {
				return null;
			}
		}
	
		public void ping() {
			session.ping();
		}
	
		public void commandCompleted(IInputInfo in, IStatusInfo status, int modelIdx) {
			if (peer != null) {
				peer.commandCompleted(in,status,modelIdx);
			}
		}
	
		
	
		// description stuff
		transient int cachedStatus = 0;
		
		static final String[] descriptions = new String[] {
			"(not running)",
			"Starting up...",
			"Ready for command input",
			"Busy...",
			"**Error in session**",
			"Ready for non-command input"
		};
		
		protected String doGetDescription() {
			String desc = "";
			if (!peer.getLineMode().equals(LineMode.getDefault()))
			{
				desc = " (" + peer.getLineMode().getName() + ")";
			}
			return descriptions[cachedStatus] + "   " +  peer.getAcl2Mode().getName() + " Mode" + desc;
		}
		
		public void sessionStatusChanged(int status) {

			if (status != cachedStatus) {
				cachedStatus = status;
				updateDescriptions();

				if (peer != null && status == NO_SESSION || status == ERROR_SESSION) {

					peer.resetLine();
				}
			}
			resetUndoStuff();
		}
		
		// actions
		public void cleanSession(A2sEditor ctx) {
			session.killSession();
			if (peer != null) {
				peer.resetLine();
			}
			reset();
			if (ctx instanceof SessionEditor) {
				ctx.gotoEnd();
			}
		}
	
		public void restartSession(A2sEditor ctx) {
			SessionMode mode = getConfig().getMode();
			if (mode != null && !mode.getUsable()) {
				Acl2sPlugin.popupMessage("Session mode not installed",
						"The session cannot be started because its mode, \"" +
						mode.getName() + "\", is not installed under this Eclipse/ACL2s.  To " +
						"be able to start a session in this mode, you will need to install that mode.  "+
						"(Ask the person you got the file from.)",
						SWT.ICON_WARNING);
			} else {
				String pref;
				if (done.size() > 0) {
					pref = SessionPrefs.getRestartPref(ctx.getEditorSite().getShell(), this, session.isAlive());
				} else {
					pref = SessionPrefs.RESTART_EXTEND;
				}
				if (pref == SessionPrefs.RESTART_CANCEL) {
					return;
				}
				if (pref == SessionPrefs.RESTART_CLEAN) {
					cleanSession(ctx);
				} else {
					session.killSession();
					if (peer != null) {
						peer.resetLine();
					}
				}
				DoneElement d = cur.forceFinish();
				done.add(d);
				session.startNewSession(this,getConfig());
			}
		}
	
		public void interruptSession(A2sEditor ctx) {
			try {
				getManager().interruptSession();
			} catch (SessionDeadException e) {
				// ignore
			}
		}
	
		public void killSession(A2sEditor ctx) {
			getManager().killSession();
		}
	
		
		public void forgetRedo(A2sEditor ctx) {
			try {
				/*(void)*/ session.systemCmd("(acl2s::clear-reverted-super-history acl2::state)");
				cur.env.forgetRedo();
			} catch (SessionStateException sse) {
				ctx.errorMessageBox("Session busy", "Can't forget redo information while session is busy.");
			}
		}
		
	
		/*====================== Saving/Loading =======================*/
		public void reset() {
			done.clear();
			inputIdxs.clear();
			checkpointIdxs.clear();
			inputIdxs.add(Integer.valueOf(0));
			checkpointIdxs.add(Integer.valueOf(0));
			
			if (partitioner != null) {
				partitioner.disconnect();
				setDocumentPartitioner(null);
			}
			newDumpLength = 0;
			set(" ");
			dumpLength = 0;
			partitioner = new Partitioner();
			partitioner.connect(this);
			setDocumentPartitioner(partitioner);
	
			cmdPos = cmdHistory.size()-1;
			miscPos = miscHistory.size()-1;
			
			cur = new CurElement();
			cur.connect(this);
	
			if (peer != null) {
				peer.resetLine();
			}
			
			if (config == null) {
				config = new MyInteractiveSessionConfig(Acl2sPlugin.getBaseConfig(), Acl2sPlugin.getSessionSupportDir());
			}
			config.setMode(getAcl2Mode());
			
			for (IProofTreeListener l : listeners) {
				l.sessionCleaned();
			}
		}
		
		// returns true if initially dirty
		public void loadFrom(InputStream stream) {
			ObjectInputStream in;
			try {
				try {
					in = new ObjectInputStream(stream);
					int x = in.readInt();
					int m = x & 0xffff0000;
					int v = x & 0xffff;
					if (m != 0x0a250000) {
						throw new ClassCastException("Invalid magic number for a2s file.");
					}
					if (v != versionId) {
						throw new ClassCastException("Incompatible version number for a2s file.");
					}
				} catch (EOFException eofe) {
					reset();
					return; // just an empty file
				}
				if (partitioner != null) {
					partitioner.disconnect();
					setDocumentPartitioner(null);
				}
				set("");
	
				String data = (String)in.readObject();
				partitioner = (Partitioner) in.readObject();
				config = (MyInteractiveSessionConfig) in.readObject();
				config.setBaseConfig(Acl2sPlugin.getBaseConfig());
				cur = (CurElement) in.readObject();
				done.clear();
				for (Object o : (Iterable<?>) in.readObject()) {
					done.add((DoneElement) o);
				}
				dumpLength = in.readInt();
				newDumpLength = dumpLength;
				inputIdxs.clear();
				for (Object o : (Iterable<?>) in.readObject()) {
					inputIdxs.add((Integer) o);
				}
				checkpointIdxs.clear();
				for (Object o : (Iterable<?>) in.readObject()) {
					checkpointIdxs.add((Integer) o);
				}
				cmdHistory.clear();
				for (Object o : (Iterable<?>) in.readObject()) {
					cmdHistory.add((String) o);
				}
				cmdPos = in.readInt();
				miscHistory.clear();
				for (Object o : (Iterable<?>) in.readObject()) {
					miscHistory.add((String) o);
				}
				miscPos = in.readInt();
				in.close();
				
				set(data);
				partitioner.connect(this);
				setDocumentPartitioner(partitioner);
				cur.connect(this);
			} catch (ClassCastException cce) {
				Acl2sPlugin.logWarning("Data error while reading in session history.  Discarding previous history.", cce);
				reset();
				ensureDirty();
				return;
			} catch (ClassNotFoundException e) {
				Acl2sPlugin.logWarning("Data error while reading in session history.  Discarding previous history.", e);
				reset();
				ensureDirty();
				return;
			} catch (IOException ioe) {
				Acl2sPlugin.logWarning("I/O error while reading in session history.  Discarding previous history.", ioe);
				reset();
				ensureDirty();
				return;
			}
		}
	
		public InputStream getDumpStream() {
			try {
				ByteArrayOutputStream bytes = new ByteArrayOutputStream();
				ObjectOutputStream out = new ObjectOutputStream(bytes);
				out.writeInt(0x0a250000 + versionId);
				out.writeObject(get());
				out.writeObject(partitioner);
				out.writeObject(config);
				out.writeObject(cur);
				out.writeObject(done);
				out.writeInt(dumpLength);
				out.writeObject(inputIdxs);
				out.writeObject(checkpointIdxs);
				out.writeObject(cmdHistory);
				out.writeInt(cmdPos);
				out.writeObject(miscHistory);
				out.writeInt(miscPos);
				out.close();
				return new ByteArrayInputStream(bytes.toByteArray());
			} catch (IOException e) {
				Acl2sPlugin.logError("Error building session dump stream.", e);
				return null;
			}
		}
	
		
		
		/*===================== state building ======================*/
		private void doProcessOutputLine(String s) {
			if (s.length() == 0) return;
			if (cur.inProofTree) {
				int i = s.indexOf("#>\\>");
				if (i >= 0) {
					if (i > 0) {
						doProcessOutputLine(s.substring(0,i) + '\n');
					}
					cur.endProofTree();
					doProcessOutputLine(s.substring(i + 4));
				} else {
					doProcessOutputLine2(s);
				}
			} else {
				if (s.startsWith("#<\\<0")) {
					cur.startProofTree();
					doProcessOutputLine(s.substring(5));
				} else {
					doProcessOutputLine2(s);
				}
			}
		}
		
		private void doProcessOutputLine2(String s) {
			if (s.length() == 0) return;
			if (s.endsWith("$\n")) {
				/*if (s.endsWith("$ClAuSe{$\n")) {
					// TODO: clause stuff
				} else*/
				if (s.startsWith("$ChEcKpOiNt{$") &&
						s.endsWith("$ChEcKpOiNt}$\n")) {
					cur.layDownCheckpoint(s.substring(13,s.length() - 14));
					return;
				}
			}
			cur.appendOutput(s);
		}
	
		public void appendOutputLine(String s) {
			doProcessOutputLine(s);
			cur.flushOutput();
		}
		
		public void appendOutputLines(Iterable<String> ss) {
			for (String s: ss) {
				doProcessOutputLine(s);
			}
			cur.flushOutput();
		}
	
		protected transient String savedCmd = null;
		
		public int finishOutput(IStatusInfo statusInfo, IEnvInfo envInfo) {
			DoneElement d = cur.finish(statusInfo);
			done.add(d);
			cur.init(envInfo);
			replaceImmediate(cmdHistory.get(cmdPos));
			return done.size() - 1;
		}
	
		public void updateLastEnv(IEnvInfo envInfo) {
			cur.env = envInfo;
		}
	
		public void nextInput(IInputInfo in) {
			cur.nextInput(in);
			cmdHistory.set(cmdPos,getImmediate().trim());
			replaceImmediate(miscHistory.get(miscPos));
		}
	
		public void newSession() {
			cur.init(StartupInputAndEnv.instance);
			cur.nextInput(StartupInputAndEnv.instance);
		}
		
		
		/*========================== accessing stuff ========================*/
		public IEnvInfo getEnv(int idx) {
			if (idx == done.size()) {
				return cur.getEnv();
			} else { 
				return done.get(idx).getEnv();
			}
		}
	
		public IInputInfo getInput(int idx) {
			if (idx == done.size()) {
				return cur.getInput();
			} else {
				return done.get(idx).getInput();
			}
		}
	
		public String getOutput(int idx) {
			if (idx == done.size()) {
				return cur.getOutput();
			} else {
				return done.get(idx).getOutput();
			}
		}
	
		public String getProofTree(int idx) {
			if (idx == done.size()) {
				return cur.proofTree.toString();
			} else {
				return done.get(idx).getFinalProofTree();
			}
		}
	
		public IStatusInfo getStatus(int idx) {
			return done.get(idx).getStatus();
		}
	
		
		public int countCompletedCmds() {
			return done.size();
		}
	
		
		
		public int findCheckpointOffset(int idx, String withGoal) {
			int base = inputIdxs.get(idx).intValue();
			int len = getLength();
			try {
				for (; base < len;) {
					ITypedRegion r = getPartition(base);
					if (r.getType().equals(OUTPUT)) break;
					if (r.getType().equals(OUTPUTERR)) break;
					base = r.getOffset() + r.getLength();
				}
			} catch (BadLocationException e1) {
				// impossible
			}
			
			if (idx == done.size()) {
				for (int i = 0; i < cur.chkptNames.size(); i++) {
					if (withGoal.contains(cur.chkptNames.get(i)) &&
							withGoal.contains(cur.chkptNames.get(i) + " ")) {
						return base + cur.chkptOffsets.get(i).intValue();
					}
				}
				return -1;
			} else {
				DoneElement e = done.get(idx);
				for (int i = 0; i < e.chkptNames.length; i++) {
					if (withGoal.contains(e.chkptNames[i]) &&
							withGoal.contains(e.chkptNames[i] + " ")) {
						return base + e.chkptOffsets[i];
					}
				}
				return -1;
			}
		}
		
		
		/*========================= misc ==========================*/
		public SessionMode getAcl2Mode() {
			if (peer != null) {
				return peer.getAcl2Mode();
			} else {
				return config.getMode();
			}
		}
		
		public MyInteractiveSessionConfig getConfig() {
			config.setMode(getAcl2Mode());
			config.setBaseConfig(Acl2sPlugin.getBaseConfig());
			config.setAcl2CustomizationOverride(Acl2Prefs.getCustomizationOverride(null, this));
			config.setSuperHistoryEnabled(peer != null && peer.getLineMode().cancelOnError());
			config.setSuperHistoryTrackMonitorsOverride(InteractionPrefs.getTrackMonitorsOverride(null, this));
			config.setSuperHistoryTrackPresentationOverride(InteractionPrefs.getTrackPresentationOverride(null, this));
			return config;
		}
		
		public void setAcl2Mode(SessionMode mode) {
			if (peer != null) {
				peer.setAcl2Mode(mode);
			} else {
				config.setMode(mode);
			}
		}
		
		void append(String s, String typ) {
			if (s.length() == 0) return;
			partitioner.preAppend(typ);
			newDumpLength = dumpLength + s.length();
			replace2(dumpLength, 0, s);
			dumpLength = newDumpLength;
		}
		
		protected void doFireDocumentChanged2(DocumentEvent event) {
			super.doFireDocumentChanged2(event);
			/*if (event.fOffset > dumpLength &&
					(event.fText.equals("\r") || event.fText.equals("\n"))) {
				trySubmitImmediate();
			}*/
		}
		
		/*transient boolean replacingSep = false;
		public void updateSep() {
			String immediate = getImmediate();
			if (immediate.indexOf('\n') >= 0 || immediate.indexOf('\r') >= 0) {
				if (getChar2(dumpLength) == ' ') {
					replacingSep = true;
					replace2(dumpLength, 1, "\n");
					replacingSep = false;
				}
			} else {
				if (getChar2(dumpLength) != ' ') {
					replacingSep = true;
					replace2(dumpLength, 1, " ");
					replacingSep = false;
				}
			}
		}*/
		
		static final Sym U_KEYWORD = Sym.createKeyword("U");
		static final Sym UBT_KEYWORD = Sym.createKeyword("UBT");
		static final Sym UBTB_KEYWORD = Sym.createKeyword("UBT!");
		static final Sym UBU_KEYWORD = Sym.createKeyword("UBU");
		static final Sym UBUB_KEYWORD = Sym.createKeyword("UBU!");
		
		public boolean trySubmitImmediate(SessionEditor ctx) {
			String immediate = getImmediate() + "\n";
			StringParser p = new StringParser(null, immediate); // assign here to fix warning (!) 
			try {
				switch (session.getStatus()) {
					case ISessionStatusListener.READY_CMD_SESSION:
					{
						p = new StringParser(session.getCurrentEnv().getParseContext(), immediate);
						ResolvableUserInput preCmd = ResolvableUserInput.parse(p,ID,this);
						p.skipSpaceAndComments();
						String rest = immediate.substring(p.getPos());
						
						// special cases:
						boolean handledSpecially = false;
						if (preCmd instanceof UnresolvedKeywordCmd && getPeer() != null) {
							UnresolvedKeywordCmd preKeyCmd = (UnresolvedKeywordCmd) preCmd;
							Sym key = preKeyCmd.getKeyword();
							LispObject[] params = preKeyCmd.getParams();
							if (key == U_KEYWORD) {
								if (params.length == 0) {
									// EVERYTHING CHECKS OUT
									newImmediateCmd(preCmd.getInputString(),rest);
									IPeerDocument peer = getPeer();
									peer.retreatLine(ctx);
									handledSpecially = true;
								}
							} else if (key == UBT_KEYWORD || key == UBTB_KEYWORD ||
									   key == UBU_KEYWORD || key == UBUB_KEYWORD) {
								if (params.length == 1) {
									IResultInfo r;
									if (key == UBT_KEYWORD || key == UBTB_KEYWORD) {
										r = session.systemCmd2("(acl2s::print-ubt-superlen " + params[0].toString() + ")\n");
									} else {
										r = session.systemCmd2("(acl2s::print-ubu-superlen " + params[0].toString() + ")\n");
									}
									
									try {
										String output = r.getOutput();
										int lstart = output.indexOf("INDEX:");
										if (lstart < 0) throw new NumberFormatException();
										int numstart = lstart + "INDEX:".length();
										int numend = Math.max(output.indexOf('\n', numstart), numstart);
										output = output.substring(numstart, numend);
										int superLen = Integer.parseInt(output);
										
										int modlIdx = done.size() - 1;
										for (;;) {
											if (modlIdx < 0) break;
											DoneElement elt = done.get(modlIdx);
											if (elt == null) break;
											IEnvInfo env = elt.getEnv();
											if (env == null) break;
											if (env.getSuperDoneSize() <= superLen) {
												// EVERYTHING CHECKS OUT
												newImmediateCmd(preCmd.getInputString(),rest);
												IPeerDocument peer = getPeer();
												peer.retreatBackThrough(ctx, modlIdx);
												handledSpecially = true;
												break;
											}
											modlIdx--;
										}
									} catch (NumberFormatException e) {
										// do nothing
									}
								}
							}
						}
						
						if (!handledSpecially) {
							ResolvedInput cmd = preCmd.resolve(session);
							newImmediateCmd(preCmd.getInputString(),rest);
							if (getPeer() != null && cmd.couldNeedUndo() && InteractionPrefs.isRelevantCmdPrefWormhole(this)) {
								cmd = new WormholeWrappedInput(cmd);
							}
							session.submitCmdInput(cmd);
						}
					}
						break;
					case ISessionStatusListener.READY_MISC_SESSION:
					{
						//p = new StringParser(null, immediate);
						p.skipSpaceAndComments();
						final int start = p.getPos();
						LispObject.parse(p);
						final int end = p.getPos();
						String input = immediate.substring(start,end);
						newImmediateMisc(start,end);
						session.submitMiscInput(input);
					}
						break;
					default:
						// ignore
				}
				return true;  // just means don't insert the '\n'
			} catch (ParseException pe) {
				if (p.peek() == StringParser.EOF) return false; // just needs more input 
				ctx.setHighlightRange(dumpLength+1+p.getPos(),0,true);
				ctx.errorMessageBox("Parse Error", pe.getMessage() +
						"\n\nCursor has been positioned at spot of error.");
				return true;
			} catch (BadCmdException e) {
				ctx.setHighlightRange(dumpLength+1,0,true);
				ctx.errorMessageBox("Bad Command", e.getMessage() +
						"\n\nCursor has been positioned at violating command.");
				return true;
			} catch (SessionDeadException e) {
				// ignore
				return true;
			} catch (SessionException e) {
				// shouldn't happen
				Acl2sPlugin.logError("Unexpected session state.", e);
				return true;
			}
		}
		
		protected void newImmediateCmd(String input, String rest) {
			cmdPos = cmdHistory.size();
			cmdHistory.set(cmdPos-1,input);
			cmdHistory.add("");
			replaceImmediate(rest);
		}
		
		protected void newImmediateMisc(int start, int end) {
			String immediate = getImmediate();
			String input = immediate.substring(start,end);
			miscPos = miscHistory.size();
			miscHistory.set(miscPos-1,input);
			String rest = immediate.substring(end).trim();
			miscHistory.add(rest);
			replaceImmediate(miscHistory.get(miscPos));
		}
		
		/*protected void removeFromImmediate(int n) {
			replace2(dumpLength,Math.min(n,getLength()-dumpLength),"");
		}
		
		protected void stowImmediateCmd() {
			cmdHistory.set(cmdPos,getImmediate().trim());
		}
		
		protected void trimImmediateTail() {
			int newLen = getLength();
			while (newLen > 0 && Character.isSpaceChar(getChar2(newLen-1))) {
				newLen--;
			}
			replace2(newLen,getLength()-newLen,"");
		}*/
	
		
		public void replaceImmediate(String s) {
			String sep;
			if (s.indexOf('\n') >= 0 || s.indexOf('\r') >= 0) {
				sep = "\n";
			} else {
				sep = " ";
			}
			replace2(dumpLength,getLength()-dumpLength,sep + s);
		}
	
	
		public void cmdPrevious() {
			switch (session.getStatus()) {
			case ISessionStatusListener.READY_CMD_SESSION:
				if (cmdPos == 0) return;
				cmdHistory.set(cmdPos,getImmediate());
				cmdPos--;
				replaceImmediate(cmdHistory.get(cmdPos));
				resetUndoStuff();
				break;
			case ISessionStatusListener.READY_MISC_SESSION:
				if (miscPos == 0) return;
				miscHistory.set(miscPos,getImmediate());
				miscPos--;
				replaceImmediate(miscHistory.get(miscPos));
				resetUndoStuff();
				break;
			}
		}
	
		public void cmdNext() {
			switch (session.getStatus()) {
			case ISessionStatusListener.READY_CMD_SESSION:
				if (cmdPos == cmdHistory.size()-1) return;
				cmdHistory.set(cmdPos,getImmediate());
				cmdPos++;
				replaceImmediate(cmdHistory.get(cmdPos));
				resetUndoStuff();
				break;
			case ISessionStatusListener.READY_MISC_SESSION:
				if (miscPos == miscHistory.size()-1) return;
				miscHistory.set(miscPos,getImmediate());
				miscPos++;
				replaceImmediate(miscHistory.get(miscPos));
				resetUndoStuff();
				break;
			}
		}
		
		public void cmdLast() {
			switch (session.getStatus()) {
			case ISessionStatusListener.READY_CMD_SESSION:
				if (cmdPos == cmdHistory.size()-1) return;
				cmdHistory.set(cmdPos,getImmediate());
				cmdPos = cmdHistory.size() - 1;
				replaceImmediate(cmdHistory.get(cmdPos));
				resetUndoStuff();
				break;
			case ISessionStatusListener.READY_MISC_SESSION:
				if (miscPos == miscHistory.size()-1) return;
				miscHistory.set(miscPos,getImmediate());
				miscPos = miscHistory.size() - 1;
				replaceImmediate(miscHistory.get(miscPos));
				resetUndoStuff();
				break;
			}
		}
		
		public int getNextInputIdx(int start) {
			return getAdjacentIdx(start,true,inputIdxs);
		}
		
		public int getPrevInputIdx(int start) {
			return getAdjacentIdx(start,false,inputIdxs);
		}
		
		public int getNextCheckpointIdx(int start) {
			return getAdjacentIdx(start,true,checkpointIdxs);
		}
		
		public int getPrevCheckpointIdx(int start) {
			return getAdjacentIdx(start,false,checkpointIdxs);
		}
		
		private int getPseudoIndexIdx(int i, ArrayList<Integer> src) {
			int sz = src.size();
			if (i < sz - 1) {
				return src.get(i).intValue();
			} else if (i == sz - 1) {
				return dumpLength + 1;
			} else {
				return getLength();
			}
		}
		
		private int getAdjacentIdx(int start, boolean direction, ArrayList<Integer> src) {
			int max = src.size();
			if (max == 0) return 0;
			int inc = 0x10000000;
			int i = 0;
			while (inc > 0) {  // binary search, undershoot
				if (i+inc <= max && getPseudoIndexIdx(i+inc,src) < start) {
					i += inc;
				}
				inc >>= 1;
			}
			if (direction && i < max) {
				i++;
				if (getPseudoIndexIdx(i,src) == start && i < max) {
					i++;
				}
			}
			return getPseudoIndexIdx(i,src);
		}
		
		public int getModelIdxOfOffset(int offset) {
			for (int i = inputIdxs.size() - 1; i > 0; i--) {
				if (offset >= inputIdxs.get(i).intValue()) return i;
			}
			return 0;
		}
	
		public int getOffsetOfModelIdx(int idx) {
			return inputIdxs.get(idx).intValue();
		}
	
		public static final String PROMPT = "__a2s_session_prompt";
		public static final String CMDTYPE = "__a2s_session_cmdtype";
		public static final String INPUT = "__a2s_session_input";
		public static final String OUTPUT = "__a2s_session_output";
		public static final String OUTPUTERR = "__a2s_session_outputerr";
		
		public static String[] getContentTypes() {
			return new String[] { PROMPT, CMDTYPE, INPUT, OUTPUT, OUTPUTERR, Partitioner.DEFAULT };
		}
		
		public String[] getLegalContentTypes() {
			return getContentTypes();
		}
	
		// must be static or else tries to serialize the document
		static class Partitioner extends AbstractDocumentPartitioner implements Serializable {
			private static final long serialVersionUID = 2L;
	
			transient String appendType = null;
			transient SessionDocument doc = null;
	
			public Partitioner() {
				super();
				addRegion(0,1,DEFAULT);
			}
			
			public String[] getLegalContentTypes() {
				return getContentTypes();
			}
	
			public void connect(IDocument document) {
				super.connect(document);
				doc = (SessionDocument) document;
			}
			
			public IRegion documentChanged2(DocumentEvent event) {
				int offset = event.getOffset();
				if (appendType != null) {
					int idx = getLastDumpRegionIdx();
					int len = event.getText().length();
					MyTypedRegion r = idx >= 0 ? regions.get(idx) : new MyTypedRegion(0,0,DEFAULT);
					if (r.getType().equals(appendType)) {
						//System.err.println("Replacing a " + appendType);
						replaceRegion(idx,new MyTypedRegion(r.getOffset(),r.getLength()+len,appendType),true);
						offset = r.getOffset();
					} else {
						//System.err.println("Inserting a " + appendType);
						insertRegion(idx+1,new MyTypedRegion(offset,len,appendType),true);
					}
					appendType = null;
				}
				MyTypedRegion r = new MyTypedRegion(doc.newDumpLength,doc.getLength()-doc.newDumpLength,DEFAULT);
				replaceRegion(getImmediateRegionIdx(),r,true);
				
				return new Region(offset,doc.getLength()-offset);
			}
			
			int getLastDumpRegionIdx() {
				return regions.size() - 2;
			}
			
			int getImmediateRegionIdx() {
				return regions.size() - 1;
			}
			
			void preAppend(String typ) {
				if (appendType != null) {
					throw new IllegalStateException();
				}
				appendType = typ;
			}
	
			public void changeLastType(String fromTyp, String toTyp) {
				int idx = getLastDumpRegionIdx();
				if (idx < 0) return;
				MyTypedRegion r = regions.get(idx);
				if (r.getType().equals(fromTyp)) {
					replaceRegion(idx,new MyTypedRegion(r.getOffset(),r.getLength(),toTyp),false);
					doc.setDocumentPartitioner(Partitioner.this);
				}
			}
		}
	
		
		
		static final class CurElement implements Serializable {
			private static final long serialVersionUID = 5L;
	
			transient SessionDocument doc = null;
			void connect(SessionDocument d) { doc = d; }
			
			IEnvInfo env;
			IInputInfo input;
			final StringBuilder output = new StringBuilder();
			StringBuilder proofTree = new StringBuilder();
			StringBuilder nextProofTree = new StringBuilder();
			IStatusInfo status;
			ArrayList<Integer> chkptOffsets = new ArrayList<Integer>();
			ArrayList<String>  chkptNames   = new ArrayList<String>();
			
			boolean hideOutput;
			int outputPos;
			boolean inProofTree;
			
			public void init(IEnvInfo env) {
				this.env = env;
				input = null;
				output.setLength(0);
				outputPos = 0;
				status = null;
				if (env.getPrompt() != null)
					doc.append(env.getPrompt(), PROMPT);
				doc.inputIdxs.add(Integer.valueOf(doc.dumpLength));
				doc.checkpointIdxs.add(Integer.valueOf(doc.dumpLength));
				chkptOffsets.clear();
				chkptNames.clear();
				inProofTree = false;
				proofTree.setLength(0);
				nextProofTree.setLength(0);
			}
	
			public void nextInput(IInputInfo i) {
				if (input != null) throw new IllegalStateException();
				input = i;
				if (i.getInputTypeString() != null) 
					doc.append(i.getInputTypeString() + " ", CMDTYPE);
				if (i.getInputString() != null) {
					if (i.getInputString().indexOf('\n') > 0) {
						// prefix a newline so that indention looks right
						doc.append("\n" + i.getInputString() + "\n", INPUT);
					} else {
						doc.append(i.getInputString() + "\n", INPUT);
					}
				}
				if (i.getMetaOutput() != null) {
					doc.append(i.getMetaOutput() + "\n", OUTPUT);
				}
				hideOutput = input.hideOutput();
				
				startProofTree();
				endProofTree(); // notify listeners of clear output
			}
			
			public void appendOutput(String s) {
				if (input == null) throw new IllegalStateException();
				if (inProofTree) {
					nextProofTree.append(s);
				} else {
					output.append(s);
				}
			}
	
			//harshrc:: Heres where Peter sets the checkpoint offsets and 
			//remembers the goal names.
			public void layDownCheckpoint(String goalStr) {
				if (input == null) throw new IllegalStateException();
				chkptOffsets.add(Integer.valueOf(output.length()));
				chkptNames.add(goalStr);
				flushOutput();
				doc.checkpointIdxs.add(Integer.valueOf(doc.dumpLength));
				output.append("^^^ Checkpoint " + goalStr + " ^^^\n");
			}
	
			public void flushOutput() {
				if (!hideOutput && output.length() > outputPos) {
					doc.append(output.substring(outputPos), OUTPUT);
					outputPos = output.length();
				}
			}
	
			public void startProofTree() {
				inProofTree = true;
				nextProofTree.setLength(0);
			}
	
			public void endProofTree() {
				inProofTree = false;
				
				StringBuilder tmp = proofTree;
				tmp.setLength(0); // recycle
				proofTree = nextProofTree;
				nextProofTree = tmp;
				
				int idx = doc.countCompletedCmds();
				for (IProofTreeListener l : doc.listeners) {
					l.newProofTree(doc,idx);
				}
			}
			
			
			public DoneElement finish(IStatusInfo s) {
				flushOutput();
				/*if (proofTree.length() > 0) {
					doc.append(">>> Final proof tree output:\n", OUTPUT);
					doc.append(proofTree.toString(), OUTPUT);
					doc.append("<<< (end of proof tree output)\n", OUTPUT);
				}*/
				if (!s.wasSuccess()) {
					doc.partitioner.changeLastType(OUTPUT,OUTPUTERR);
				}
				status = s;
				return new DoneElement(this);
			}
			
			public DoneElement forceFinish() {
				flushOutput();
				return new DoneElement(this);
			}
			
			public IEnvInfo getEnv() { return env; }
			public IInputInfo getInput() { return input; }
			public String getOutput() { return output.toString(); }
			public IStatusInfo getStatus() { return status; }
		}
		
		static final class DoneElement implements Serializable {
			private static final long serialVersionUID = 5L;
			
			final IEnvInfo env;
			final IInputInfo input;
			final String output;
			final IStatusInfo status;
			final int[] chkptOffsets;
			final String[] chkptNames;
			final String finalProofTree;
	
			public DoneElement(CurElement that) {
				this.env = that.env;
				this.input = that.input;
				this.output = that.output.toString();
				this.status = that.status;
				int sz = that.chkptOffsets.size();
				assert sz == that.chkptNames.size();
				this.chkptOffsets = new int[sz];
				this.chkptNames = new String[sz];
				for (int i = 0; i < sz; i++) {
					this.chkptOffsets[i] = that.chkptOffsets.get(i).intValue();
					this.chkptNames[i] = that.chkptNames.get(i);
				}
				finalProofTree = that.proofTree.toString();
			}
	
			public IEnvInfo getEnv() { return env; }
			public IInputInfo getInput() { return input; }
			public String getOutput() { return output; }
			public IStatusInfo getStatus() { return status; }
			public String getFinalProofTree() { return finalProofTree; }
		}
	
		public void dispose() {
			session.killSession();
			session.removeSessionStatusListener(this);
			tokens.disconnect();
		}
	
		public void interrupt() throws SessionException {
			synchronized (session) {
				switch (session.getStatus()) {
				case READY_MISC_SESSION:
				case BUSY_SESSION:
					session.interruptSession();
					// fall through
				case READY_CMD_SESSION:
					session.scheduleAbort();
					break;
				}
			}
		}
	
		
		public void reparse() {
			tokens.reparse();
		}
	
		public void cleanCmdHist() {
			cmdHistory.clear();
			cmdHistory.add("");
			cmdPos = 0;
			miscHistory.clear();
			miscHistory.add("");
			miscPos = 0;
		}
	
		
		// PROOF TREE LISTENERS
		
		protected ArrayList<IProofTreeListener> listeners = new ArrayList<IProofTreeListener>();
		
		public void addProofTreeListener(IProofTreeListener l) {
			listeners.add(l);
		}
	
		public void removeProofTreeListener(IProofTreeListener l) {
			listeners.remove(l);
		}
	
	}