thank you for your answer.
You wrote:
> I am very interessed in structure transformations in structured documents
>(this is the subject of my thesis) and every experience in this domain is
>interresting for me.
>
The documents we use (proof presentations in fact) have a very restricted
structure in that every line is linked to one or more other lines according to a
logical calculi ("Line A follows from line B and line C by rule X").
The proofs we get from theorem prover systems are usually unreadable in an
aesthetic sense. So we try to restructure these outputs by creating subproofs,
moving lines to other positions etc. But we always have to ensure that the
transformed proof is still correct.
Our approach to this by now is functional: the user has to call certain
transformation functions (of which we hope that they preserve correctness) to
achive his goal. This functions operate on the internal presentation of the
proof.
Now we would like to use a more "declarative" way:
One defines the structure of correct proofs and its the job of the restructuring
tool (perhaps Thot) to check for correctness (now in a structural sense).
Then transforming the proof would be possible by simply copying, cutting and
pasting lines or whole subproofs ("paragraphs") in an editor window.
> Concerning the import of formats in Thot, there is no generic tool similar to
>transformation schema. A way to write such converters in thot is the use of
>the API to build the structure tree in memory and then saving this document in
>a piv file.
>
Now that's a bit rude:
First I define a structure schema for my type of documents, but then I have to
build an internal representation "by hand" (or reenter the whole document) ?!
What about the possibility to write an interface to the lexx/yacc tools?
Regards,
Thomas