tlaplus / CommunityModules

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
MIT License
273 stars 36 forks source link

WIP: IOExec enhancements #7

Closed lvanengelen closed 4 years ago

lvanengelen commented 4 years ago

The current IOExec has some problems handling quotes and spaces. This PR improves the situation by making IOExec just a small wrapper around Java's ProcessBuilder.

To keep the convenience of passing a string with %s placeholders, we introduce a new operator IOExecTemplate which takes a template string for the command. This template string is then split into words on which %s expansion takes place. This allows for spaces in the expanded strings. Note that for the sake of simplicity we don't handle:

lemmy commented 4 years ago

Thanks for the contribution!

https://github.com/tlaplus/CommunityModules/commit/46543b43135251bdcba25ab6529aadb9cdd1a144 https://github.com/tlaplus/CommunityModules/commit/666938954c1cbeb67f895eb6758b0d4313713ef4 https://github.com/tlaplus/CommunityModules/commit/1b3b43e0ce5ddafab0c8932d727ce223ce3f91e7

lvanengelen commented 4 years ago

Cool! However could you take a look at the error handling for me? I question if I did the calls to EvalException correctly: whether I use the correct error constant and such.