Re: [tlaplus] Using pcal.trans to write to different file

Hi Andrew,

It would take about 10 minutes to add an option to write the output to specname.new, plus about 15 minutes to find where options are handled and where the output file is written. As Hillel points out, if you want the output to be written to new .tla file, the module name should be changed. It would take 10 minutes to program that so it works 99.9% of the time. Making it work right all the time would be somewhat more difficult. You're welcome to submit an implementation of such a feature.

Leslie

On Wednesday, July 3, 2019 at 11:35:10 AM UTC-7, Hillel Wayne wrote:

I don't believe there is. Anything that did this would also have to change the module name to match the new file.

H

On Wed, Jul 3, 2019, 12:41 PM Andrew Helwer <andrew.helwer atxx domain name gmail.com> wrote:
Quick question - when I use "java pcal.trans specname.tla", it modifies the specname.tla file and writes the original contents to specname.old; is there a way to leave specname.tla untouched and specify an output file containing the translated PlusCal?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe atxx googlegroups.com.
To post to this group, send email to tlaplus atxx googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1828bef7-a959-4521-b6ee-f3ad90fdaa31%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.