[Texmacs-dev] Syntax translation

[sgulati]

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