Embellished operators

Hi all,

I'm thinking again about the rules for embellished operators and it 
seems to me that some elements are particular. For example if we ask how 
to determine the stretching of something like:

<math>
<mover>
<mo>&#x2192;</mo>
<mtext>over</mtext>
</mover>
</math>

The obvious answer is that the arrow should stretch to cover the over 
script. OK. However one can also say that the <mover> is an embellished 
element as a whole. Since is has no siblings, the arrow should have its 
default size.

To give slightly less trivial examples, what should be the size of the 
arrows (100px or 200px?) in these examples:

<math>
<mover>
<mspace width="100px"/>
<munder>
<mo>&#x2192;</mo>
<mspace width="200px"/>
</munder>
</mover>
</math>

and

<math>
<mover>
<mspace width="200px"/>
<munder>
<mo>&#x2192;</mo>
<mspace width="100px"/>
</munder>
</mover>
</math>

An example with vertical stretching rules:

<math>
<mrow>
<mspace height="50px" depth="50px"/>
<mrow>
<mo>|</mo>
<mspace height="100px" depth="100px"/>
</mrow>
</mrow>
</math>

(I wonder if an attribute like embellishedop = "false" could help to 
prevent this kind of ambiguity?)

I noticed this because implementing the complete embellished op rules 
caused a regression in Mozilla with MathML code generated by MathJax:
https://bugzilla.mozilla.org/show_bug.cgi?id=687807