mailing-list for TeXmacs Users

[Lionel Elie Mamane <address@hidden>]

On Mon, Oct 30, 2006 at 09:38:44AM +0100, Joris van der Hoeven wrote:
> On Mon, Oct 30, 2006 at 07:39:40AM +0100, Lionel Elie Mamane wrote:

>>> 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.

> But in that case a similar argument holds for the colour of the
> prompt, even though this information seems a bit more versatile.

I see the two as a different kind of information, but there are
arguments both way.

If you see the colour of the prompt as "this command has been executed
sometime in the past and has succeeded", then yes, the colour should
survive a save/exit/load cycle. The main advantage to this is: One can
open the document and immediately see what Coq commands have been
evaluated and found to pass correctly (without error) before. One sees
which part of the document is still not Coq-correct and which part is.

But I mean the colour of the prompt to say something else, that is
"the state Coq is right now is before / after that command". That is,
something that is part of the "interface to Coq" part of tmEgg and not
the "integrate Coq code in a document" part. Then, even if one has Coq
installed, when opening the document, Coq is in state "not started"
and all prompts should be in the colour for "Coq state is _before_
this command". The same if one doesn't have Coq: Coq is in the state
"not started".


What I don't like about the first solution (colour survives save /
exit / open) is that what the colour on start says is "these commands
were checked with some version of Coq on some computer in the
past". They wouldn't necessarily pass without error with the version
of Coq installed on *this* computer when you open the document. I
think it would be more confusing than anything else that one:

 - opens the document

 - see some commands have already been checked

 - ask for evaluation (check) of the command after that

 - an error happens in a "already checked" command (because wrong
   version of Coq, ...)



But if my beta-testers scream bloody murder at my choices, I'll change
it to the other way :)


-- 
Lionel