- From: Lionel Elie Mamane <address@hidden>
- To: Joris van der Hoeven <address@hidden>
- Cc: address@hidden
- Subject: Re: [TeXmacs] Forcing refresh of rendering of a document fragment
- Date: Mon, 30 Oct 2006 07:39:40 +0100
On Sun, Oct 29, 2006 at 09:30:47PM +0100, Joris van der Hoeven wrote:
>
On Tue, Oct 24, 2006 at 02:40:35PM +0200, Lionel Elie Mamane wrote:
>
> 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?
>
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.
If it were exported, I'd use it indeed.
>
> 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. 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, (...). 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.
Yes, yes. That's why I leave the content of the output nodes in the
document: someone without Coq can follow the operations without
redoing them.
--
Lionel
Archive powered by MHonArc 2.6.19.