mailing-list for TeXmacs Users

[Joris van der Hoeven <address@hidden>]

On Tue, Oct 24, 2006 at 02:40:35PM +0200, Lionel Elie Mamane wrote:
> Short version: How does one force refreshing the rendering of a
> document fragment from Scheme code, short of doing an edit action at
> that point or near?

You can assign the tree with itself, although this is not perfect
(since the history will keep track of that). In the C++ code,
we also have a routine

        void edit_typeset_rep::typeset_invalidate (path p)

We might want to export this to the Scheme level.

> the end result I'm aiming at is rather simple: before a certain point
> in the document, all prompts are one colour and after that point all
> prompts are another colour. If you see a better way to do it, I'm open
> to suggestions. That point is transient, depending on the state of the
> Coq process and should _not_ be saved with the document. It is
> currently in a Scheme variable (as a position).

Yes, extern seems a reasonable thing to use, especially if you
don't want to keep anything like the colour in the document.
Notice however that this is not necessarily what you want
in all circumstances: don't forget the case that someone without Coq
wants to open a Coq document in the same state that you left it,
without wanting to (re)do any computations.

Best wishes, Joris