Opened 14 years ago
Closed 14 years ago
#310 closed defect (fixed)
Subscripts in locked region are revealed the moment you finish a lemma
Reported by: | David Aspinall | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-4.0 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
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
Change History (2)
comment:1 Changed 14 years ago by
Status: | new → accepted |
---|
comment:2 Changed 14 years ago by
Resolution: | → fixed |
---|---|
Status: | accepted → closed |
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.
Note: See
TracTickets for help on using
tickets.
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.