Hi,
I wanted to make a framework for syntax translation between texmacs
and PVS. Currently I have been able to successfully send commands to
PVS and receive the corresponding outputs from the same. These outputs
are then received by texmacs via an input pipe and displayed
correspondingly. However due to difference in the syntax of these
commands I would first need to convert the texmacs commands to PVS
-compatible form before executing them in PVS and then the
correspoding ouputs will have to be converted back to texmacs. Please
tell me how I should go ahead making such a translation, as in a
translation table or some other type of translator. Also how I should
call and use such a translation table or module from a plug-in scheme
file.
I saw one such TeXmacs file /TeXmacs/progs/utils/plugins/plugin-convert.scm
which seemed to carry out some kind of translation. The commands will
be in math mode when sent to PVS for building a theory or doing
proofs. My \spec command in texmacs is used to write these
specifications.
best regards,
sumeer
_______________________________________________
Texmacs-dev mailing list
[email protected]
http://lists.gnu.org/mailman/listinfo/texmacs-dev
