package acl2s.plugin.editors.lisp;
	
	import java.io.ByteArrayInputStream;
	import java.io.File;
	import java.io.InputStream;
	import java.util.ArrayList;
	import java.util.HashSet;
	import java.util.LinkedList;
	import java.util.TreeSet;
	
	import org.eclipse.core.runtime.CoreException;
	import org.eclipse.jface.text.BadLocationException;
	import org.eclipse.jface.text.DocumentEvent;
	import org.eclipse.jface.text.DocumentPartitioningChangedEvent;
	import org.eclipse.jface.text.IRegion;
	import org.eclipse.jface.text.Region;
	import org.eclipse.ui.IEditorInput;
	import org.eclipse.ui.IFileEditorInput;
	import org.peterd.util.io.MiscIO;
	
	import acl2s.lib.certify.Certifier;
	import acl2s.lib.parse.EmptyParse;
	import acl2s.lib.parse.IParseContext;
	import acl2s.lib.parse.ParseException;
	import acl2s.lib.parse.PositionedParseException;
	import acl2s.lib.parse.StringParser;
	import acl2s.lib.parse.SubstringParser;
	import acl2s.lib.parse.obj.LispObject;
	import acl2s.lib.session.IEnvInfo;
	import acl2s.lib.session.IStatusInfo;
	import acl2s.lib.session.SessionDeadException;
	import acl2s.lib.session.SessionException;
	import acl2s.lib.session.SessionMode;
	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.parse.DocumentParser;
	import acl2s.plugin.parse.LispToken;
	import acl2s.plugin.parse.LispTokens;
	import acl2s.plugin.prefs.InteractionPrefs;
	import acl2s.uilib.cmd.BadCmdException;
	import acl2s.uilib.cmd.ResolvableUserInput;
	import acl2s.uilib.cmd.ResolvedInput;
	import acl2s.uilib.session.IInputInfo;
	import acl2s.uilib.session.ISessionModel;
	import acl2s.uilib.session.ISessionStatusListener;
	import acl2s.uilib.session.RedoInput;
	import acl2s.uilib.session.StartupInputAndEnv;
	import acl2s.uilib.session.UndoInput;
	
	public class LispDocument extends A2sDocument implements IPeerDocument {
		public static String ID = LispDocument.class.getCanonicalName();
		
		protected final Partitioner ldp = new Partitioner();
		protected ISessionDocument ses = null;
		
		// ====== DATA / ACCESS / STORAGE =======
		private class DoneInfo {
			int modelIdx;
			ResolvedInput input;
	
			protected DoneInfo(int modelIdx, ResolvedInput input) {
				this.modelIdx = modelIdx;
				this.input = input;
			}
			
			public int getInputType() {
				if (input == null) {
					return ResolvedInput.UNKNOWN;
				} else {
					return input.getType();
				}
			}
		}
		
		private class AboveInfo {
			Region region;
			ResolvableUserInput resolvable;
	
			protected AboveInfo(Region region, ResolvableUserInput resolvable) {
				this.region = region;
				this.resolvable = resolvable;
			}
		}
		
		protected final ArrayList<AboveInfo> aboveInfo = new ArrayList<AboveInfo>();
		protected final ArrayList<DoneInfo> doneInfo = new ArrayList<DoneInfo>();
		
	/*	protected BeginBookCmdInput beginBookInput = null;
		protected int beginBookIdx = -1;*/
		protected SessionMode acl2Mode = SessionMode.compatible;
		protected LineMode lineMode = LineMode.getDefault();
			
		// just a view
		protected transient int lineIdx = 0;
		protected transient int todoIdx = 0;
	
		protected void updateIdxs() {
			lineIdx = getPreviousEnd(doneInfo.size());
			todoIdx = getPreviousEnd(aboveInfo.size());
		}
	
		protected void checkIdxs() {
			if (lineIdx != getPreviousEnd(doneInfo.size())) {
				throw new IllegalStateException();
			}
			if (todoIdx != getPreviousEnd(aboveInfo.size())) {
				throw new IllegalStateException();
			}
		}
		
		private int getPreviousEnd(int i) {
			assert i <= aboveInfo.size();
			if (i > 0) {
				return regionEnd(aboveInfo.get(i-1).region);
			} else {
				return 0;
			}
		}
		
		public static int regionEnd(Region r) {
			return r.getOffset() + r.getLength();
		}
	
		public MyTypedRegion getTodoRegion() {
			return new MyTypedRegion(lineIdx,todoIdx-lineIdx,TODO);
		}
		
		public MyTypedRegion getBelowRegion() {
			return new MyTypedRegion(todoIdx,getLength()-todoIdx,DEFAULT);
		}
		
		public int readOnlyPoint() { return todoIdx; }
		
		@Override
		protected boolean allowReplace(final int pos, final int length, final String text) {
			if (pos < todoIdx) {
				String pref = InteractionPrefs.getAboveEditPref(Acl2sPlugin.inDisplayThread() ? Acl2sPlugin.getShell() : null, this);
				if (pref == InteractionPrefs.ABOVE_EDIT_UBT) {
					display.asyncExec(new Runnable() {
						public void run() {
							int oldTodoIdx;
							do {
								oldTodoIdx = todoIdx;
								retreatLine2(null);
							} while (oldTodoIdx > todoIdx && pos < todoIdx);
							LispDocument.this.replace2(pos, length, text);
						}
					});
				}
				return false;
			} else {
				return true;
			}
		}
	
		public void replace(int pos, int length, String text) throws BadLocationException {
			if (text != null && text.indexOf('\t') >= 0) {
				text = text.replace("\t","    ");
				// shouldn't happen ordinarily with sourceviewer autoedits
				// not a general solution because caret doesn't cooperate
			}
			super.replace(pos, length, text);
		}
	
		public SessionMode getAcl2Mode() { return acl2Mode; }
	
		public void setAcl2Mode(SessionMode mode) {
			if (ses != null && ses.getManager().getStatus() != ISessionStatusListener.NO_SESSION) {
				throw new IllegalStateException();
			}
			if (!mode.equals(acl2Mode)) {
				acl2Mode = mode;
				ensureDirty();
			}
			updateDescriptions();
		}
		
		public LineMode getLineMode() { return lineMode; }
	
		public void setLineMode(LineMode mode) {
			if (ses != null && ses.getManager().getStatus() != ISessionStatusListener.NO_SESSION) {
				throw new IllegalStateException();
			}
			if (!mode.equals(lineMode)) {
				lineMode = mode;
				ensureDirty();
				if (!lineMode.isAdvancable()) {
					resetLineAndTodo();
				}
			}
			updateDescriptions();
		}
		
		protected String doGetDescription() {
			String desc;
			if (ses != null) {
				desc = "" + acl2Mode.getName() + " Mode";
				if (!lineMode.equals(LineMode.getDefault())) {
					desc += " (" + lineMode.getName() + ")";
				}
				if (!acl2Mode.getUsable()) {
					desc += " (not installed!)";
				}
			} else {
				desc = "(no associated session)";
			}
			if (acl2Mode.getBookDevAllowed() && hasBookCode()) {
				desc += " + book code";
			}
			return desc;
		}
		
		public boolean hasBookCode() {
			return tokens.pastBeginBookForm() > 0;
		}
		
		public String getPreamble() {
			int pastIdx = tokens.pastBeginBookForm();
			if (pastIdx > 0) {
				return get2(0,pastIdx);
			} else {
				return null;
			}
		}
		
		public boolean hasCompletedTangent() {
			int i = 0;
			for (;;) {
				if (i >= doneInfo.size()) {
					return false;
				}
				if (doneInfo.get(i).getInputType() == ResolvedInput.BEGIN_BOOK) {
					break;
				}
				i++;
			}
			i++;
			if (i >= doneInfo.size()) {
				return false;
			}
			if (doneInfo.get(i).getInputType() != ResolvedInput.IN_PACKAGE) {
				return false;
			}
			for (;;) {
				i++;
				if (i >= doneInfo.size()) {
					return false;
				}
				if (doneInfo.get(i).input == null ||
					!doneInfo.get(i).input.isEmbeddedEvent()) {
					return true;
				}
			}
		}
		
		// CREATION/SETUP 
		
		public LispDocument(MyDocumentProvider dp) {
			super(dp);
			setDocumentPartitioner(ldp);
			ldp.connect(this);
			tokens = new LispTokens();
			tokens.connect(this);
		}
		
		public ISessionDocument getSession() { return ses; }
		
		public void dispose() {
			tokens.disconnect();
		}
	
		public void setA2s(ISessionDocument a) {
			if (ses != a) {
				ses = a;
				if (ses != null) {
					ses.killSession(null);
				}
				doneInfo.clear();
				updateIdxs();
			}
			/*
			int max = ses.getModel().countCompletedCmds();
			for (int i = 0; i < doneInfo.size(); i++) {
				int idx = doneInfo.get(i).modelIdx;
				if (idx < 0 || idx >= max) {
					Acl2sPlugin.logWarning("Session model index out of bounds.  Moving completed line appropriately.",null);
					removeBadModelIdxsFrom(i);
					ensureDirty();
					break;
				}
				IInputInfo in = ses.getModel().getInput(doneInfo.get(i).modelIdx);
				boolean formMatch = aboveInfo.get(i).resolvable.getInputString().equals(in.getInputString()); 
				if (formMatch && in instanceof ResolvedInput) {
					doneInfo.get(i).input = (ResolvedInput) in;
				} else if (formMatch && in instanceof RedoInput) {
					doneInfo.get(i).input = (ResolvedInput) (((RedoInput)in).getOriginalInput());
				} else {
					Acl2sPlugin.logWarning("Session history doesn't match indices stored for .lisp file.  Moving completed line appropriately.",null);
					removeBadModelIdxsFrom(i);
					ensureDirty();
					break;
				}
			}*/
			partitioningChangedAll();
			updateDescriptions();
		}
	
		/*
		private void removeBadModelIdxsFrom(int i) {
			for (int j = doneInfo.size() - 1; j >= i; j--) {
				doneInfo.remove(i);
			}
			int oldLineIdx = lineIdx;
			updateIdxs();
			partitioningChanged(lineIdx,oldLineIdx - lineIdx);
		}
		*/
		
		
		//  LOAD & SAVE
		
		static class Annotation implements Comparable<Annotation> {
			int idx;
			int prio;
			String str;
			
			public Annotation(int idx, String str, int prio) {
				this.idx = idx;
				this.str = str;
				this.prio = prio;
			}
			
			public int compareTo(Annotation that) {
				if (this.idx == that.idx) {
					return this.prio - that.prio;
				} else {
					return this.idx - that.idx;
				}
			}
		}
		
		public final static String TODO_STRING = "#|ACL2s-ToDo-Line|#\n";
		public final static String SMODE_PREFIX = ";$ACL2s-SMode$;";
		public final static String LMODE_PREFIX = ";$ACL2s-LMode$;";
	
		public final static String PREAMBLE_START = "#|$ACL2s-Preamble$;\n";
		public final static int PREAMBLE_START_LEN = PREAMBLE_START.length();
		public final static String PREAMBLE_END = ";$ACL2s-Preamble$|#\n";
		public final static int PREAMBLE_END_LEN = PREAMBLE_END.length();
	
		public final static String OLD_LINE_STRING = ";$ACL2-A2S-LINE$;";
		public final static String OLD_TODO_STRING = "#|THE-LINE-INPROGRESS|#\n";
		public final static String OLD_SMODE_PREFIX = ";$ACL2-A2S-MODE$;";
		public final static String OLD_LMODE_PREFIX = ";$ACL2-A2S-LMODE$;";
		
		public final static String OLD_PREAMBLE_START = "#|$ACL2-A2S-PREAMBLE$;\n";
		public final static int OLD_PREAMBLE_START_LEN = OLD_PREAMBLE_START.length();
		public final static String OLD_PREAMBLE_END = ";$ACL2-A2S-PREAMBLE$|#\n";
		public final static int OLD_PREAMBLE_END_LEN = OLD_PREAMBLE_END.length();
	
		public InputStream getDumpStream() {
			StringBuilder dump = new StringBuilder();
	
			int pastIdx = 0;
			if (acl2Mode.getBookDevAllowed()) {
				pastIdx = tokens.pastBeginBookForm();
			}
			if (pastIdx > 0) {
				dump.append(PREAMBLE_START);
			}
	
			// mode output
			if (acl2Mode != SessionMode.compatible) {
				String[] modeInit = acl2Mode.getInitStrings();
				if (modeInit != null) {
					for (int i = 0; i < modeInit.length; i++) {
						dump.append(modeInit[i]);
					}
				}
				dump.append(SMODE_PREFIX);
				dump.append(acl2Mode.getName());
				dump.append('\n');
			}
			
			if (lineMode != LineMode.enforced) {
				dump.append(LMODE_PREFIX);
				dump.append(lineMode.getName());
				dump.append('\n');
			}
			
			TreeSet<Annotation> annotations = new TreeSet<Annotation>();
	
			
			if (lineMode.savePositions() && todoIdx > 0) {
				annotations.add(new Annotation(todoIdx,TODO_STRING,1));
			}
	
			if (pastIdx > 0) {
				annotations.add(new Annotation(pastIdx,PREAMBLE_END,2));
			}
	
	
			int pos = 0;
			for (Annotation a : annotations) { // in order
				assert pos <= a.idx;
				dump.append(get2(pos,a.idx-pos));
				dump.append(a.str);
				pos = a.idx;
			}
			dump.append(get2(pos,getLength()-pos));
			
			return new ByteArrayInputStream(dump.toString().getBytes());
		}
	
		public void set(String init) {
			aboveInfo.clear();
			doneInfo.clear();
			setDocumentPartitioner(null);
			ldp.disconnect();
			acl2Mode = SessionMode.compatible;
	
			StringBuilder content = new StringBuilder(init);
			
			int idx = 0;  // translate all tabs to 8 spaces
			for (; idx < content.length();) {
				idx = content.indexOf("\t", idx+1);
				if (idx < 0) break;
				content.replace(idx,idx+1,"        ");
			}
			idx = 0;     // remove all carriage returns
			for (; idx < content.length();) {
				idx = content.indexOf("\r", idx+1);
				if (idx < 0) break;
				content.replace(idx,idx+1,"");
			}
			
			
			// get rid of preamble markings; they're really for .lisp compatibility
			idx = content.indexOf(PREAMBLE_START);
			if (idx >= 0) {
				content.replace(idx, idx + PREAMBLE_START_LEN, "");
			} else {
				idx = content.indexOf(OLD_PREAMBLE_START);
				if (idx >= 0) {
					content.replace(idx, idx + OLD_PREAMBLE_START_LEN, "");
				}
			}
			idx = content.indexOf(PREAMBLE_END);
			if (idx >= 0) {
				content.replace(idx, idx + PREAMBLE_END_LEN, "");
			} else {
				idx = content.indexOf(OLD_PREAMBLE_END);
				if (idx >= 0) {
					content.replace(idx, idx + OLD_PREAMBLE_END_LEN, "");
				}
			}
	
			// read and get rid of code before any session mode spec
			idx = content.indexOf(SMODE_PREFIX); 
			if (idx < 0) idx = content.indexOf(OLD_SMODE_PREFIX);
	
			if (idx >= 0) {
				int after = content.indexOf(";", idx+1) + 1;
				int eol = after;
				while (eol < content.length()) {
					char ch = content.charAt(eol);
					if (ch == '\r' || ch == '\n') break;
					eol++;
				}
				String modeString = content.substring(after,eol);
				acl2Mode = Acl2sPlugin.getBaseConfig().lookupMode(modeString);
				if (acl2Mode == null) {
					acl2Mode = SessionMode.getUninstalledMode(modeString, new String[] { content.substring(0, idx) });
					Acl2sPlugin.maybeWarnUninstalledMode(modeString);
					// old approach:
					//Acl2sPlugin.logWarning("Unrecognized session mode (using default instead): " + modeString, null);
					//acl2Mode = Acl2sPlugin.getBaseConfig().getDefaultMode();
					//ensureDirty();
				}
				int pastModeDef = eol+1;
				if (pastModeDef < content.length() && content.charAt(eol) == '\r' &&
						content.charAt(pastModeDef) == '\n') {
					pastModeDef++;
				}
				content.delete(0,pastModeDef);
			}
	
			// read and get rid of any line mode spec
			idx = content.indexOf(LMODE_PREFIX);
			if (idx < 0) idx = content.indexOf(OLD_LMODE_PREFIX);
			
			if (idx >= 0) {
				int after = content.indexOf(";", idx+1) + 1;
				int eol = after;
				while (eol < content.length()) {
					char ch = content.charAt(eol);
					if (ch == '\r' || ch == '\n') break;
					eol++;
				}
				String modeString = content.substring(after,eol);
				lineMode = LineMode.lookup(modeString);
				if (lineMode == null) {
					Acl2sPlugin.logWarning("Unrecognized line mode (using default instead): " + modeString, null);
					lineMode = LineMode.getDefault();
					ensureDirty();
				}
				int pastModeDef = eol+1;
				if (pastModeDef < content.length() && content.charAt(eol) == '\r' &&
						content.charAt(pastModeDef) == '\n') {
					pastModeDef++;
				}
				content.delete(0,pastModeDef);
			}
			
			// { Get rid of & ignore any old "line" spec
			idx = content.indexOf(OLD_LINE_STRING); 
			if (idx >= 0) {
				int eol = idx;
				while (eol < content.length()) {
					char ch = content.charAt(eol);
					if (ch == '\r' || ch == '\n') break;
					eol++;
				}
				int after = eol+1;
				if (after < content.length() && content.charAt(eol) == '\r' &&
						content.charAt(after) == '\n') {
					after++;
				}
				content.delete(idx,after);
			}
			// }
			
			lineIdx = 0;
			
			// now find actual todo position
			todoIdx = content.indexOf(TODO_STRING);
			if (todoIdx < 0) todoIdx = content.indexOf(OLD_TODO_STRING);
			
			if (todoIdx < 0) {
				todoIdx = 0;
			} else {
				int after = content.indexOf("\n", todoIdx) + 1;  // to accommodate either old or new
				content.delete(todoIdx, after);
				
				
				SubstringParser p = new SubstringParser(null,content,0,todoIdx);
				try {
					while (!p.eof()) {
						int start = p.getPos();
						ResolvableUserInput in = ResolvableUserInput.parse(p, ID, this.getSession()); 
						/*if (in instanceof BeginBookCmdInput && beginBookInput == null) {
								beginBookInput = (BeginBookCmdInput) in;
								beginBookIdx = inputs.size() - 1;
							}*/
						int end = p.getPos();
						aboveInfo.add(new AboveInfo(new Region(start,end-start),in));
					}
				} catch (EmptyParse ep) {
					// ok
				} catch (ParseException pe) {
					lineIdx = 0;
					todoIdx = 0;
					aboveInfo.clear();
					doneInfo.clear();
					Acl2sPlugin.logWarning("Error restoring line position.",pe);
					ensureDirty();
				} catch (BadCmdException bce) {
					lineIdx = 0;
					todoIdx = 0;
					aboveInfo.clear();
					doneInfo.clear();
					Acl2sPlugin.logWarning("Error restoring line position.",bce);
					ensureDirty();
				}
	
			}
			super.set(content.toString());
			setDocumentPartitioner(ldp);
			ldp.connect(this);
			partitioningChangedAll();
			updateDescriptions();
		}
	
		public LispDocumentProvider getProvider() {
			return Acl2sPlugin.getLispDocumentProvider();
		}
		
		
		// LINE MANIPULATION
		
		protected void doResetLine() {
			if (doneInfo.size() == 0) return;
			int oldLineIdx = lineIdx;
			doneInfo.clear();
			updateIdxs();
			partitioningChanged(lineIdx,oldLineIdx - lineIdx);
			//if (lineMode.savePositions()) ensureDirty(); // not anymore!
		}
	
		protected void doResetTodo() {
			if (todoIdx == lineIdx) return;
			int oldTodoIdx = todoIdx;
			while (aboveInfo.size() > doneInfo.size()) {
				aboveInfo.remove(aboveInfo.size()-1);
			}
			updateIdxs();
			partitioningChanged(todoIdx,oldTodoIdx - todoIdx);
			if (lineMode.savePositions()) ensureDirty();
		}
		
		protected void doResetLineAndTodo() {
			if (aboveInfo.size() == 0) return;
			
			int oldTodoIdx = todoIdx;
			doneInfo.clear();
			aboveInfo.clear();
			updateIdxs();
			partitioningChanged(0,oldTodoIdx);
			if (oldTodoIdx != todoIdx) 
				if (lineMode.savePositions())
					ensureDirty();
		}
	
		public boolean inOrAboveLine(int offset) {
			return offset < todoIdx;
		}
	
		protected void doAdvanceLine(int modelIdx, ResolvedInput in) {
			if (doneInfo.size() >= aboveInfo.size()) throw new IllegalStateException();
			int oldLineIdx = lineIdx;
			doneInfo.add(new DoneInfo(modelIdx,in));
			updateIdxs();
			partitioningChanged(oldLineIdx,lineIdx-oldLineIdx);
		}
	
		protected void doRetreatLine() {
			if (doneInfo.size() == 0 || aboveInfo.size() > doneInfo.size()) throw new IllegalStateException();
			int oldLineIdx = lineIdx;
			doneInfo.remove(doneInfo.size()-1);
			aboveInfo.remove(doneInfo.size());
			updateIdxs();
			partitioningChanged(lineIdx,oldLineIdx-lineIdx);
			if (lineMode.savePositions()) ensureDirty();
		}
	
		protected void doRetreatTodo() {
			if (todoIdx == lineIdx) throw new IllegalStateException();
			int oldTodoIdx = todoIdx;
			aboveInfo.remove(aboveInfo.size()-1);
			updateIdxs();
			partitioningChanged(todoIdx,oldTodoIdx - todoIdx);
			if (lineMode.savePositions()) ensureDirty();
		}
		
		protected void addNextForm() throws BadCmdException, PositionedParseException, EmptyParse {
			String below = getBelowRegion().getFromDocument(this);
			StringParser p = new StringParser(null, below);
			int start = todoIdx + p.getPos();
			ResolvableUserInput in;
			try {
				in = ResolvableUserInput.parse(p,ID,this.getSession());
			} catch (EmptyParse e) {
				throw e;
			} catch (ParseException pe) {
				throw new PositionedParseException(pe,todoIdx + p.getPos());
			}
			int end = todoIdx + p.getPos();
			aboveInfo.add(new AboveInfo(new Region(start,end-start),in));
		}
		
		protected void doAdvanceTodo() throws PositionedParseException, BadCmdException, EmptyParse {
			int oldTodoIdx = todoIdx;
			addNextForm();
			updateIdxs();
			partitioningChanged(oldTodoIdx,todoIdx-oldTodoIdx);
			if (lineMode.savePositions()) ensureDirty();
			notifyLineAdvancement();
			resetUndoStuff();
		}
		
		public boolean isEmptyBelow() {
			String below = getBelowRegion().getFromDocument(this);
			StringParser p = new StringParser(null, below);
			try {
				p.skipSpaceAndComments();
			} catch (ParseException e) {
				return false;
			}
			return p.eof();
		}
		
		// ADVANCEMENT (for clearing undo history stuff)
		
		protected final HashSet<LineAdvancementListener> ladvListeners = new HashSet<LineAdvancementListener>();
		
		static interface LineAdvancementListener {
			public void lineAdvanced();
		}
		
		public void addLineAdvancementListener(LineAdvancementListener l) {
			ladvListeners.add(l);
		}
		
		public void removeLineAdvancementListener(LineAdvancementListener l) {
			ladvListeners.remove(l);
		}
		
		protected void notifyLineAdvancement() {
			for (LineAdvancementListener l : ladvListeners) {
				l.lineAdvanced();
			}
		}
	
		// PARTITIONER
		
		public final static String PREAMBLE = "__a2s_preamble";
		public final static String BOOK = "__a2s_book";
		public final static String TANGENT = "__a2s_tangent";
		public final static String TODO = "__a2s_line_todo";
		public final static String DEFAULT = Partitioner.DEFAULT;
		
		protected void partitioningChangedAll() {
			partitioningChanged(0,getLength());
		}
		
		protected void partitioningChanged(int start, int len) {
			ldp.computePartitions();
			DocumentPartitioningChangedEvent dpce;
			dpce = new DocumentPartitioningChangedEvent(this);
			dpce.setPartitionChange(DEFAULT_PARTITIONING, start, len);
			fireDocumentPartitioningChanged(dpce);
		}
		
		public static String[] getContentTypes() {
			return new String[] { PREAMBLE, BOOK, TANGENT, TODO, DEFAULT };
		}
		
		public String[] getLegalContentTypes() {
			return getContentTypes();
		}
	
		protected class Partitioner extends AbstractDocumentPartitioner {
			private static final long serialVersionUID = 1L;
	
			public String[] getLegalContentTypes() {
				return getContentTypes();
			}
	
			public IRegion documentChanged2(DocumentEvent event) {
				//computePartitions();
				
				updateLast();
				
				//return null;
				//return new Region(todoIdx,doc.getLength()-todoIdx);
				
				//int docLen = doc.getLength();
				int added = event.fText.length() - event.fLength;
				if (added < 0) added = 0;
				return null; //new Region(docLen-added,added);
			}
			
			private void updateLast() {
				updateIdxs();
				int docLen = LispDocument.this.getLength();
				int lastIdx = regions.size() - 1;
				if (lastIdx >= 0 && regions.get(lastIdx).getType() == DEFAULT) {
					MyTypedRegion r = new MyTypedRegion(todoIdx,docLen-todoIdx,DEFAULT);
					replaceRegion(lastIdx,r,true);
				} else {
					addRegion(todoIdx,docLen,DEFAULT);
				}
			}
			
			private void computePartitions() {
				clearRegions();
				
				int docLen = LispDocument.this.getLength();
				int idx = 0;
	
				//updateIdxs();  PREREQUISITE!
				checkIdxs();
				
				if (lineIdx > idx) {  // <=> modelIdxs.size() > 0
					int i = 0;
					int toIdx;
					if (i < doneInfo.size() && doneInfo.get(i).getInputType() != ResolvedInput.BEGIN_BOOK) { 
						do {
							toIdx = regionEnd(aboveInfo.get(i).region);
							i++;
						} while (i < doneInfo.size() && doneInfo.get(i).getInputType() != ResolvedInput.BEGIN_BOOK);
						addRegion(idx, toIdx, PREAMBLE);
						idx = toIdx;
					}
					if (i < doneInfo.size()) { // <=> lineIdx > idx
						toIdx = regionEnd(aboveInfo.get(i).region);
						i++;
						if (i < doneInfo.size() && (doneInfo.get(i).getInputType() == ResolvedInput.IN_PACKAGE)) {
							do {
								toIdx = regionEnd(aboveInfo.get(i).region);
								i++;
							} while (i < doneInfo.size() &&
									doneInfo.get(i).input != null &&
									doneInfo.get(i).input.isEmbeddedEvent());
						}
						addRegion(idx, toIdx, BOOK);
						idx = toIdx;
						if (lineIdx > idx) {
							addRegion(idx, lineIdx, TANGENT);
							idx = lineIdx;
						}
					}
				}
				if (todoIdx > idx) {
					addRegion(idx, todoIdx, TODO);
					idx = todoIdx;
				}
				if (docLen > idx) {
					addRegion(idx, docLen, DEFAULT);
					idx = docLen;
				}
			}
		}
	
		
		/*===================== to be called by A2s =================*/	
		protected IInputInfo curInput = null;
		protected final LinkedList<UndoInput> undoInput = new LinkedList<UndoInput>();
		//protected boolean deleteOnError = false;
		
		private UndoInput getUndo(ResolvedInput in, int superIdx) {
			return new UndoInput(in,superIdx,
					ses.getManager().getSecret(),
					in.getUndoMsg());
		}
		
		public IInputInfo nextInputOption() {
			if (!lineMode.isAdvancable()) return null;
			if (!undoInput.isEmpty()) {
				curInput = undoInput.removeFirst();
				return curInput;
			}
			// else no pending undo
			if (doneInfo.size() == aboveInfo.size()) {
				curInput = null;
				return curInput;
			}
			// else pending 'todo' form(s)
			ResolvableUserInput foo = aboveInfo.get(doneInfo.size()).resolvable;
			ResolvedInput bar = null;
			if (ses.getManager().isAlive()) {
				try {
					bar = foo.resolve(ses.getManager());
				} catch (SessionException e) {
					// shouldn't happen
					Acl2sPlugin.logError("Acl2 session problem for system command.", e);
					return null;
				}
			}
			if (!lineMode.cancelOnError()) doAdvanceLine(0,bar);
			curInput = bar;
			if (ses.getManager().isAlive() && bar != null) { // bar != null probably redundant
				if (!bar.couldNeedUndo() ||
						bar.getUndoMsg() != null) {
					return curInput;
				}
			}
			if (!lineMode.cancelOnError()) { return curInput; } // no REDOs
			// else REDO might be possible.  keep checking...
			ISessionModel model = ses.getModel();
			IEnvInfo env = model.getEnv(model.countCompletedCmds());
			if (env == null) return curInput;  // no session yet!
			if (env.getSuperUndoneSize() == 0) return curInput;
			LispObject parsed = bar == null ? null : bar.getParsed();
			int preDone = env.getSuperDoneSize();
			int i = model.countCompletedCmds() - 1;
			int balance = 0;
			IEnvInfo oldPostEnv = env;
			IEnvInfo oldPreEnv;
			for (;i > 0;) { // the i > 0 shouldn't be needed
				IInputInfo old = model.getInput(i);
				oldPreEnv = model.getEnv(i);
				if (old instanceof StartupInputAndEnv) {
					return curInput;
				} else if (old instanceof RedoInput) {
					balance++;
				} else if (old instanceof UndoInput && balance > 0) {
					balance--;
				} else if (old instanceof UndoInput) {
					if (oldPostEnv.getSuperDoneSize() != preDone) return curInput;
					
					UndoInput oldUndo = (UndoInput) old;
					IInputInfo orig = oldUndo.getOriginalInput();
					if (!(orig instanceof ResolvedInput)) return curInput;
					ResolvedInput orig2 = (ResolvedInput) orig;
					
	                if (parsed != null) { // if post-resolved parsing is available, use it
	                    LispObject oldParsed = orig2.getParsed();
	                	if (!(parsed.equals(oldParsed))) return curInput;
	                } else {
	                	if (!(orig2.abstractlyEquals(foo,env.getParseContext()))) return curInput;
	                }
			
					int hist = oldPreEnv.getSuperDoneSize();
					if (hist > env.getSuperDoneSize() + env.getSuperUndoneSize()) return curInput;
					// everything checks out!  make it a REDO
					curInput = new RedoInput(orig,oldPreEnv.getSuperDoneSize(),ses.getManager().getSecret());
					return curInput;
				} else if (old instanceof ResolvedInput) {
					ResolvedInput old2 = (ResolvedInput) old;
					if (old2.couldNeedUndo()) {
						// return curInput;
						// break here if we want something that *potentially* affects
						// history (but doesn't) to interfere with allowability of REDO  
					}
					if (old2.getUndoMsg() != null) {
						return curInput;
						// could be something fishy
					}
				}
				if (preDone > oldPostEnv.getSuperDoneSize() + oldPostEnv.getSuperUndoneSize()) {
					return curInput;
					// optimization to clip search when we know we've past
					// where a matching undo would have been
				}
				
				// rewind one top-level form
				do {
					i--;
				} while (i > 0 && model.getEnv(i).inWormhole());
				oldPostEnv = oldPreEnv;
			}
			return curInput;
		}
	
		public void commandCompleted(IInputInfo in, IStatusInfo status, int modelIdx) {
			if (!lineMode.cancelOnError()) return;
			if (in == curInput) {
				if (in instanceof ResolvedInput) {
					if (!status.wasSuccess()) {
						doResetTodo();
					} else {
						doAdvanceLine(modelIdx,(ResolvedInput) in);
					}
				} else if (in instanceof RedoInput) {
					if (!status.wasSuccess()) {
						Acl2sPlugin.logError("Error while redoing in ACL2:" + ses.getModel().getOutput(modelIdx), null);
						ses.getManager().killSession();
					}
					IInputInfo orig = ((RedoInput)in).getOriginalInput();
					if (!(orig instanceof ResolvedInput)) {
						throw new IllegalStateException();
					}
					doAdvanceLine(modelIdx,(ResolvedInput) orig);
				} else if (in instanceof UndoInput) {
					if (!status.wasSuccess()) {
						Acl2sPlugin.logError("Error while undoing in ACL2:" + ses.getModel().getOutput(modelIdx), null);
						ses.getManager().killSession();
					}
					// nothing else to do
				} else {
					// impossible
					throw new IllegalStateException();
				}
				curInput = null;
			} else if (in.getSource().equals(ID)) {
				if (status.extendedLogicalState()) {
					if (!status.wasSuccess()) { // weird.  we'll just fix it.
						int superHistIdx = ses.getModel().getEnv(modelIdx).getSuperDoneSize();
						String cmd = UndoInput.buildUndoString(superHistIdx, ses.getManager().getSecret());
						try {
							/* (void) */ ses.getManager().systemCmd2(cmd);
							ses.getManager().updateModelEnv();
						} catch (SessionException e) {
							Acl2sPlugin.logError("Session died unexpectedly.", e);
						}
					} else { // it seems we canceled this in the mean time
						// Undo to last superhistory index 
						int superIdx;
						int doneCount = doneInfo.size();
						if (doneCount == 0) {
							superIdx = StartupInputAndEnv.instance.getSuperDoneSize();
						} else {
							superIdx = ses.getModel().getStatus(doneInfo.get(doneCount - 1).modelIdx).getSuperDoneSize();
						}
						undoInput.addFirst(getUndo((ResolvedInput) in, superIdx));
					}
				}
			} else if (in instanceof ResolvedInput &&
					status.extendedLogicalState()) {
				// didn't come from line action
				// & ResolvedInput means it came from user
				// & we only care if it modified the world
				ResolvedInput c = (ResolvedInput) in;
	
				String pref = InteractionPrefs.getRelevantCmdPref(Acl2sPlugin.inDisplayThread() ? Acl2sPlugin.getShell() : null, ses);
				if (pref.equals(InteractionPrefs.RELEVANT_CMD_INSERT)) {
					int oldTodoIdx = todoIdx;
					String formString = c.getInputString();
					int formStart;
					if (todoIdx == 0) {
						formStart = todoIdx;
						formString = formString + "\n\n";
					} else {
						formStart = todoIdx + 2;
						formString = "\n\n" + formString;
					}
					replace2(todoIdx,0,formString);
					aboveInfo.add(new AboveInfo(new Region(formStart,c.getInputString().length()),c));
					doneInfo.add(new DoneInfo(modelIdx,c));
					updateIdxs();
					partitioningChanged(oldTodoIdx,todoIdx-oldTodoIdx);
					notifyLineAdvancement();
					resetUndoStuff();
				} else {
					// Undo to last superhistory index 
					int superIdx;
					int doneCount = doneInfo.size();
					if (doneCount == 0) {
						superIdx = StartupInputAndEnv.instance.getSuperDoneSize();
					} else {
						superIdx = ses.getModel().getStatus(doneInfo.get(doneCount - 1).modelIdx).getSuperDoneSize();
					}
					undoInput.addFirst(getUndo((ResolvedInput) in, superIdx));
				}
			}
		}
	
		public void resetLineAndTodo() {  // called by a2s on clean session
			curInput = null;
			doResetLineAndTodo();
		}
	
		public void resetLine() {  // called by a2s on restart/stop session
			curInput = null;
			doResetLine();
			undoInput.clear();
		}
	
	
		/*=================== to be called from editors (by ADs) ================*/	
		/*protected boolean checkA2s(A2sEditor ctx) {
			if (a2s == null) {
				ctx.infoMessageBox("Not supported", "Operation not supported because this lisp file has no associated session.  Go to menu `ACL2' | `Set session mode...' to change.");
				return false;
			} else {
				return true;
			}
		}*/
		
		// allow null ctx!
		public void cancelTodo(A2sEditor ctx) {
			if (ses != null && curInput instanceof ResolvedInput) {
				try {
					ses.interrupt();
				} catch (SessionException e) {
				}
				curInput = null;
			}
			int oldTodoIdx = todoIdx;
			doResetTodo();
			if (ctx instanceof LispEditor)
				ctx.revealRange(todoIdx,oldTodoIdx-todoIdx);
		}
	
		protected void advanceTodo2(A2sEditor ctx, boolean emptyOk) {
			try {
				doAdvanceTodo();
				if (ses != null) {
					ses.ping();
				}
			} catch (EmptyParse e) {
				if (!emptyOk) {
					ctx.infoMessageBox("Could not advance todo", "No more forms in Lisp file.");
				}
			} catch (PositionedParseException e) {
				ctx.setHighlightRange(e.getPos(),0,true);
				ctx.errorMessageBox("Parse Error", e.getMessage() + "\n\nCursor has been positioned at spot of error.");
			} catch (BadCmdException e) {
				String below = getBelowRegion().getFromDocument(this);
				StringParser p = new StringParser(null, below);
				try {
					p.skipSpaceAndComments();
				} catch (ParseException e1) {
				}
				ctx.setHighlightRange(todoIdx+p.getPos(),0,true);
				ctx.errorMessageBox("Bad Command", e.getMessage() + "\n\nCursor has been positioned at violating command.");
			}
		}
		
		public void advanceTodo(A2sEditor ctx) {
			if (!lineMode.isAdvancable()) {
				ctx.infoMessageBox("Not supported", "Operation not supported in this line mode.  Go to menu `ACL2' | `Set line mode...' to enable line tracking.");
				return;
			}
			int oldTodoIdx = todoIdx;
			advanceTodo2(ctx,false);
			if (ctx instanceof LispEditor)
				ctx.revealRange(oldTodoIdx,todoIdx-oldTodoIdx);
		}
	
		public void allTodo(A2sEditor ctx) {
			if (!lineMode.isAdvancable()) {
				ctx.infoMessageBox("Not supported", "Operation not supported in this line mode.  Go to menu `ACL2' | `Set line mode...' to enable line tracking.");
				return;
			}
			int savedTodoIdx;
			do {
				savedTodoIdx = todoIdx;
				advanceTodo2(ctx,true);
			} while (savedTodoIdx < todoIdx);
		}
		
		// allow null ctx!
		protected void retreatLine2(A2sEditor ctx) {
			if (doneInfo.size() < aboveInfo.size()) {
				if (doneInfo.size() < aboveInfo.size() - 1) {
					doRetreatTodo();
				} else {
					cancelTodo(ctx);
				}
			} else {
				int inputIdx = doneInfo.size() - 1;
				int modelIdx = doneInfo.get(inputIdx).modelIdx;
				ResolvedInput input = doneInfo.get(inputIdx).input;
				assert input != null;
				/*if (input == null) {
					ctx.errorMessageBox("Error moving line", "Could not retreat line because document is still initializing.");
					return;
				}*/
				doRetreatLine();
				if (ses != null && lineMode.cancelOnError() && input.couldNeedUndo()) {
					IEnvInfo env = ses.getModel().getEnv(modelIdx);
					UndoInput undo = getUndo(input,env.getSuperDoneSize());
					
					undoInput.addLast(undo);
					ses.ping();
				}
			}
		}
		
		public void retreatLine(A2sEditor ctx) {
			if (aboveInfo.size() == 0) return;
			
			int oldTodoIdx = todoIdx;
	
			retreatLine2(ctx);
			
			if (ctx instanceof LispEditor)
				ctx.revealRange(todoIdx,oldTodoIdx-todoIdx);
		}
		
		public void retreatBackThrough(A2sEditor ctx, int modelIdx) {
			int oldTodoIdx = todoIdx;
	
			for (;;) {
				int lastDone = doneInfo.size() - 1;
				if (lastDone < 0) break;
				if (doneInfo.get(lastDone).modelIdx < modelIdx) break;
				retreatLine2(ctx);
			}
			
			if (ctx instanceof LispEditor)
				ctx.revealRange(todoIdx,oldTodoIdx-todoIdx);
		}
	
		public void resetLineAndTodo(A2sEditor ctx) {
			if (aboveInfo.size() == 0) return;
			int oldTodoIdx;
			do {
				oldTodoIdx = todoIdx;
				retreatLine2(ctx);
			} while (aboveInfo.size() > 0);
			
			if (ctx instanceof LispEditor)
				ctx.revealRange(todoIdx,oldTodoIdx-todoIdx);
		}
	
		public void moveTodoPastPoint(int index, A2sEditor ctx) {
			if (index > todoIdx || (index == todoIdx && index == 0)) {
				// skip to beginning of whitespace if in it
				LispToken t = tokens.getToken(tokens.getTokenIdxContaining(index));
				if (index < t.offset || t.type == LispToken.EOF_TOK) {
					index = t.absoluteStart();
				}
				
				int oldTodoIdx;
				do {
					oldTodoIdx = todoIdx;
					advanceTodo2(ctx, false);
				} while (oldTodoIdx < todoIdx && index > todoIdx);
			} else {
				int oldTodoIdx;
				do {
					if (aboveInfo.size() == 0) return;
					oldTodoIdx = todoIdx;
					retreatLine2(ctx);
				} while (oldTodoIdx > todoIdx && index < todoIdx);
			}
		}
		
		public void moveTodoPastCursor(A2sEditor ctx) {
			if (!(ctx instanceof LispEditor)) {
				ctx.errorMessageBox("Not supported", "The invoked action is only supported in an ACL2/Lisp editor.");
				return;
			}
			int cursor = ctx.getDocCaret();
			if (lineMode.isAdvancable()) { // move line
				moveTodoPastPoint(cursor,ctx);
			} else { // submit form
				if (ses == null) {
					ctx.errorMessageBox("No associated session", "The invoked action is only supported with an " +
						"associated session that is running and ready for command input.");
				}
				if (ses.getManager().getStatus() != ISessionStatusListener.READY_CMD_SESSION) {
					ctx.errorMessageBox("Session not ready", "The invoked action is only supported with an " +
						"associated session that is running and ready for command input.");
					return;
				}
				int len = getLength();
				int backSearchFrom = len;
				if (cursor < backSearchFrom) {
					int tIdx = tokens.getTokenIdxContaining(cursor);
					backSearchFrom = tokens.getToken(tIdx).offset + 1;
				}
				
				if (backSearchFrom >= len) {
					ctx.errorMessageBox("No more input", "No more input forms after cursor.");
					return;
				}
				
				int start = tokens.formSearch(backSearchFrom, false);
				
				try {
					IParseContext pc;
					DocumentParser dp;
					ResolvableUserInput preCmd;
					ResolvedInput cmd;
	
					pc = ses.getManager().getCurrentEnv().getParseContext();
					dp = new DocumentParser(pc,this,start);
					try {
						preCmd = ResolvableUserInput.parse(dp,ID, this.getSession());
						cmd = preCmd.resolve(ses.getManager());
						cmd.throwIfBad();
					} catch (ParseException pe) {
						ctx.setDocCaret(dp.getPos());
						ctx.errorMessageBox("Parse Error", pe.getMessage() +
						"\n\nCursor has been positioned at spot of error.");
						return;
					} catch (BadCmdException e) {
						ctx.setDocCaret(start);
						ctx.errorMessageBox("Bad Command", e.getMessage() +
						"\n\nCursor has been positioned at violating command.");
						return;
					}
					
					ses.getManager().submitCmdInput(cmd);
					try {
						dp.skipSpaceAndComments();
					} catch (ParseException e) {
						// don't care anymore
					}
					ctx.setDocCaret(Math.min(dp.getPos(),getLength()));
				} catch (SessionDeadException e) {
					ctx.errorMessageBox("Session died",
							"Session died before requested input could be submitted.");
					return;
				} catch (SessionException e) {
					ctx.errorMessageBox("Unexpected session state",
							"Unexpected session state before submitting input:\n\n" +
							e.getMessage());
					return;
				}
			}
		}
		
		public String suckForm(A2sEditor ctx) {
			if (!lineMode.isAdvancable()) {
				ctx.infoMessageBox("Not supported", "Operation not supported in this line mode.  Go to menu `ACL2' | `Set line mode...' to enable line tracking.");
				return null;
			}
			try {
				String inputString;
				if (lineMode.cancelOnError()) {
					addNextForm();
					AboveInfo a = aboveInfo.remove(aboveInfo.size() - 1);
					replace2(a.region.getOffset(),a.region.getLength(),"");
					inputString = a.resolvable.getInputString();
				} else {
					doAdvanceTodo();
					doAdvanceLine(0,null);
					inputString = aboveInfo.get(aboveInfo.size() - 1).resolvable.getInputString();
				}
				return inputString;
			} catch (EmptyParse e) {
				ctx.infoMessageBox("Cannot read next form", "No more forms in Lisp file.");
				return null;
			} catch (PositionedParseException e) {
				ctx.errorMessageBox("Parse Error", e.getMessage());
				return null;
			} catch (BadCmdException e) {
				ctx.errorMessageBox("Bad Command", e.getMessage());
				return null;
			}
		}
	
		public void reparse() {
			tokens.reparse();
		}
	
		public void cleanOutputFiles(A2sEditor ctx) {
			// GCL == .o  SBCL == .fasl  OpenMCL == .dfsl  + .acl2 + .cert
			

			File f = getOSFile();

			if (!Certifier.legalLispFile(f)) return;  // quietly do nothing
			
			String base = MiscIO.removeFileExtension(f.getPath());
			new File(base + ".acl2").delete();
			new File(base + ".cert").delete();
			new File(base + ".o").delete();
			new File(base + ".fasl").delete();
			new File(base + ".dfsl").delete();
			
			IEditorInput input = getInput();
			if (input instanceof IFileEditorInput) {
				IFileEditorInput finput = (IFileEditorInput) input;
				try {
					finput.getFile().getParent().refreshLocal(1, null);
				} catch (CoreException e) {
					Acl2sPlugin.logError("Error refreshing directory after cleaning output files", e);
				}
			} // else, no need
		}
	}