Closed fehrenbach closed 9 years ago
Your analysis is correct. I think the reason for this feature was command lines like this:
pts boring-library.pts --literate cool-stuff.lpts
This command processes boring-library.pts as a non-literate file, and then processes cool-stuff.lpts as a literate file with all the bindings from boring-library.pts in scope.
With the new support for modules, we don't need this anymore: One should use an import in cool-stuff.lpts, and literate vs. non-literate will be figured out from the file extensions. So we could remove this feature, cleaning up the whole option handling story while we're at it.
After looking at docs, the fix might be as simple as:
diff --git a/src-lib/PTS/Options.hs b/src-lib/PTS/Options.hs
index 334c37b..97aac11 100755
--- a/src-lib/PTS/Options.hs
+++ b/src-lib/PTS/Options.hs
@@ -117,5 +117,5 @@ handleShowInsts = ShowInsts
-- order requirements
-argOrder = ReturnInOrder FilePath
+argOrder = Permute
-- flag processing
I suspect one might drop quite some code as a result (processFlagsGlobal
vs processFlagsLocal
looks related).
But I'm out of time for today, so I couldn't get to the bottom of this pit and didn't test this yet.
Yes this fix would probably work, but when touching this, one should also simplify the option handling.
Yes this fix would probably work, but when touching this, one should also simplify the option handling.
I see — Local
options don't make any more sense.
pts foo.pts --debug=typing
does not do what I would expect it to, namely it does not print typing debug information. Butpts --debug=typing foo.pts
does.I gather, from glancing at the option handling code and experimenting, that command line options apply only to files to their right. This is somewhat unconventional. In case we really need this it should be mentioned somewhere and we should warn users when options do not apply to any file, as in the first invokation above.