[isabelle] How to use Isabelle/Isar as a compiler?



Hi everyone,
Is there any way that we can use Isabelle/Isar as a compiler?
For example, how do we run a command like:
$ ./isabelle MyTheory.thy
And then isabelle will do as the Proof General processes the whole buffer,
and will return the first found error if it exists.

Thank you




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.