What is the meaning of this pseudo-code function? While reading the paper Holistic twig joins: optimal XML pattern matching I came across the pseudo code for liststack algorithm. (available through google scholar)

A function in the algorithm confused me, since I can understand what it is supposed to do, but can't deconstruct the notation:

$\qquad \mathtt{Function}\ \mathtt{end}(q\mathtt) \\
 \qquad\qquad \mathtt{return}\ \forall q_i \in \mathtt{subtreeNodes}(q) : \mathtt{isLeaf}(q_i) \implies \mathtt{eof}(T_{q_i})$

This function is supposed to return a single boolean result. It is supposed to be true when all lists associated to leaf nodes of a query pattern node are at their end. So true means there are no more nodes in the query pattern to process.

But what is the meaning of the set builder(ish?) notation here? Is it 

$\qquad$ "for all subtree nodes of $q$ for which $\mathtt{isLeaf}(q_i)$ is true $\mathtt{eof}(T_{q_i})$ is also true"

(which means that the list is at the end position)? 

Or is it 

$\qquad$ "for all subtree nodes of $q$, $\mathtt{isLeaf}(q_i)$ implies $\mathtt{eof}(T_{q_i})$ is true"? 

Is double arrow representing implies with its truth table? 

As you can see, I'm having a bit difficulty in associating the colon and its precedence.
"Implies" in the English language indicates that there is room for subjectivity. But this is not standard English you're looking at. When you read A⟹B as "A implies B" in Discrete Mathematics, it is just another way to say, "If A is true, then B is true." Formally, this is called material implication.

So the two ways you thought to read it are the same - as far as Comp.Sci. goes. Left to right and minimal imagination it reads (out loud), 
"Return the truth of this assertion: For all q-sub-i that are members of subtreeNodes of q, isLeaf of q-sub-i implies eof of T-sub-sub-i."