texmacs-dev
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Texmacs-dev] Re: [TeXmacs] tmEgg and TeXmacs [was: Reporting bugs in Te


From: Henri Lesourd
Subject: [Texmacs-dev] Re: [TeXmacs] tmEgg and TeXmacs [was: Reporting bugs in TeXmacs]
Date: Tue, 08 Aug 2006 12:44:55 +0200
User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.2) Gecko/20030208 Netscape/7.02

Lionel Elie Mamane wrote:

I'd like my code to get notified (and be able to do stuff) when text
in an <input> of a Coq session is modified / deleted, as well as when
a whole <input> or a whole Coq <session> is deleted (or cut) or
pasted. Is there any way to do this in TeXmacs currently, or would it
be rather straightforward to add

This is definitely a feature for which I see a need,
for reasons rather similar to your concerns.

As far as I know, this is thus a natural extension
of TeXmacs programming, but before, we must stabilize
simpler features which have been implemented over the
last year, and which in particular, are not described
in the documentation. I would say that after this,
features like notification are next on the list.

As for me, what I do currently to solve these kinds
of problems is retaining a copy of the relevant chunks
of the document at one point in time, and when I need
it, comparing them to the current version. For implementing
this, you only need tree traversals of the markup,
and to be able to know when the comparison should
be done. This latter one is the critical point, which
depends on your application : as for me, what I do is
that I check changes when an "action" occurs, namely,
when the users hits Ctrl-Return inside a session (or
inside a chunk of markup, its the same), I look at
the changes, and then I build a function call using
the content of the current markup chunk that I just
checked ; the problem with this is that for example
in a session, because I hook (i.e., I replace) the
action which previously implemented the sending of
the current line to the plugin, I must also reimplement
the low-level machinery for adding a new line if the
user is doing a submit when located on the last line,
or either just put the cursor to the next line and
update the output just above with the result computed
by my plugin. Given what you say, what you want
to do would imply to do what I describe here,
plus possibly a more complex update of the
session as a whole (e.g., changing, or even
removing or inserting several different lines
in the session for one particular event).


I hope this was understandable.

Me too ;-P ...


Best, Henri





reply via email to

[Prev in Thread] Current Thread [Next in Thread]