Subscripts in locked region are revealed the moment you finish a lemma

[David Aspinall]

As long as you work within the lemma it is fine.

lemma

    assumes asm: "P\<isub>i \<and> Q\<isub>i" shows "Q\<isub>i \<and> P\<isub>i"

proof -

    from asm obtain "P\<isub>i" and "Q\<isub>i"

        by blast

    then show "Q\<isub>i \<and> P\<isub>i"

        by simp

qed

[David Aspinall]

This is caused by overlapping text property invisible: Unicode Tokens uses font-lock to set the invisible property for the smaller regions for the subscript markup, whereas the proof region which allows control of proof visibility overlaps this region and uses a variable named after the proof.

The wider scope of the non-invisible region overrides the contained invisible regions.

The cleanest way to fix this is probably to rework the proof visibility control to make pg-script-portions' refer directly to spans rather than invisibility tokens. Then add/remove the overriding property in pg-make-element-invisible' and 'pg-make-element-visible'.

Would be nice to use some nice higher-level folding mechanism to use instead of the visibility properties.

[David Aspinall]

Fixed as suggested by avoiding buffer-invisibility-spec for script region visibility control, in favour of explicitly adding and removing invisible properties on spans. See #317.