/*
 * generated by Xtext
 */
package mm.ecxt.scoping;

import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.EReference;
import org.eclipse.xtext.nodemodel.util.NodeModelUtils;
import org.eclipse.xtext.resource.IEObjectDescription;
import org.eclipse.xtext.scoping.IScope;
import org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider;
import org.eclipse.xtext.scoping.impl.FilteringScope;

import com.google.common.base.Predicate;

import mm.ecxt.mmLanguage.AxiomStatement;
import mm.ecxt.mmLanguage.Block;
import mm.ecxt.mmLanguage.ConstDecl;
import mm.ecxt.mmLanguage.MMDatabase;
import mm.ecxt.mmLanguage.ProofStatement;
import mm.ecxt.mmLanguage.VarDecl;

/**
 * This class contains custom scoping description.
 * 
 * See
 * https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#scoping
 * on how and when to use it.
 */
public class MMLanguageScopeProvider extends AbstractDeclarativeScopeProvider {

	private static boolean isValidReference(EObject source, EObject target) {
		boolean targetNotVisibleAfterBlock = !(target instanceof ConstDecl || target instanceof AxiomStatement
				|| target instanceof ProofStatement);
		if (targetNotVisibleAfterBlock) {
			EObject targetBlock = target instanceof VarDecl ? target.eContainer().eContainer() : target.eContainer();
			assert targetBlock instanceof Block || targetBlock instanceof MMDatabase;
			if (!contains(targetBlock, source)) {
				return false;
			}
		}
		return startOffsetOf(target) < startOffsetOf(source);
	}

	private static boolean contains(EObject container, EObject obj) {
		return obj != null && (obj.equals(container) || contains(container, obj.eContainer()));
	}

	private static int startOffsetOf(EObject x) {
		return NodeModelUtils.getNode(x).getTotalOffset();
	}

	@Override
	public IScope getScope(final EObject context, EReference reference) {
		Predicate<IEObjectDescription> filter = new Predicate<IEObjectDescription>() {
			@Override
			public boolean apply(IEObjectDescription input) {
				return isValidReference(context, input.getEObjectOrProxy());
			}
		};
		return new FilteringScope(super.getScope(context, reference), filter);
	}

}

@@ -494,41 +494,8 @@
 nt;%0A
-import mm.ecxt.mmLanguage.Block;%0A
 impo
@@ -980,16 +980,134 @@
 rget) %7B%0A
+%09%09if (target.eContainer() == null) %7B%0A%09%09%09// TODO: Implement references to $%5B ... $%5D included file%0A%09%09%09return false;%0A%09%09%7D%0A
 %09%09boolea
@@ -1110,27 +1110,24 @@
 olean target
-Not
 VisibleAfter
@@ -1138,10 +1138,8 @@
 k = 
-!(
 targ
@@ -1241,17 +1241,16 @@
 ment
-)
 ;%0A%09%09if (
 targ
@@ -1249,17 +1249,15 @@
 if (
+!
 target
-Not
 Visi
@@ -1273,16 +1273,82 @@
 lock) %7B%0A
+%09%09%09// First we make sure that the source is in the target's block%0A
 %09%09%09EObje
@@ -1455,15 +1455,14 @@
 %0A%09%09%09
-assert 
+if (!(
 targ
@@ -1484,51 +1484,110 @@
 eof 
-Block %7C%7C targetBlock instanceof MMDatabase;
+MMDatabase)) %7B%0A%09%09%09%09// this should not occur, but for robustness we'll stop here%0A%09%09%09%09return false;%0A%09%09%09%7D
 %0A%09%09%09

Fix NullPointerException if multiple .mm files open