disable export_theory in interactive mode

[digama0]

Also a possibility: using Globals.interactive as the default value of the flag. I decided not to because I am not sure if users like to run export_theory manually in REPL sessions (they shouldn't). Edit: implemented

This flag is needed to prevent hol4-vscode from generating actual theory outputs when the server reads and runs the file in fast-cheat mode. (Yes, I tried rebinding export_theory. It's not reliable because the massive block of opens at the top of most script files has a tendency to re-rebind it.)

[mn200]

If we have to have a guard on this at all, then I'd prefer to let it just be Globals.interactive (and then Theory.sig can stay as it is).

While working in the "before-times" (before we have a nice syntax #1364), I'd still prefer to have you rebind the SML value, along with enforcing the requirement that all open declarations occur at the head of the file. (Meaning the rebind can reliably be applied after doing all those opens.)

[digama0]

Currently the HOL parser doesn't even parse open declarations, which makes this annoying to do correctly. Plus mid-file opens are a thing. The syntax of #1364 is precisely what we need in order to do this properly, until then I'm still having to deal with a significant fraction of breakages when using hol4-vscode normally.

[mn200]

Mid-file opens should not be a thing. I'd happily grasp that (and other) nettle first just so that eventually layering over a nicer syntax can be done as a separate concern.

For the purposes of keeping this particular commit small, please just guard exporting with Globals.interactive.

[digama0]

I think mid-file open should be a thing, where I mean specifically open and not the load side effect. open is a normal operation in SML and it is weird to restrict its use to the top of the file; it is used in let blocks too. It is the open effect and not the load effect that is problematic in this particular case, while #1364 is aimed at restricting the load effect to the top of the file.

[mn200]

Of course, open should be freely usable in non-Script files. In script files, it is equally reasonable to restrict top-level occurrences to the top of the files. (People shouldn't be writing much code with nested open in script-files, but it's reasonable to keep it legal.)

open's shotgun destruction of the namespace is a very bad thing to have happen in the middle of a script.

[mn200]

It looks like some test-cases will need to be adjusted.