more context lines on failure

[digama0]

ML error messages tend to be closer to 20 lines:

 /home/mario/Documents/HOL/src/portableML/Portable.sml:15: error: Structure does not match signature.
    Signature: val export: string * 'a -> unit
    Structure: Not present
 Found near
   struct
    structure Process = OS.Process 
    structure FileSys = OS.FileSys 
    exception Div = General.Div 
    exception Mod = ... 
    fun ... 
    ... 
    ...
    end
 error in quse /home/mario/Documents/HOL/src/portableML/Portable.sml : Fail "Static Errors"
 error in load $(HOLDIR)/sigobj/Portable : Fail "Static Errors"
 error in load $(HOLDIR)/sigobj/Feedback : Fail "Static Errors"
 error in load /home/mario/Documents/HOL/src/bool/boolScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"

Getting just the last 10 lines of this error message is dropping everything important. (For a while I didn't even realize the error message is truncated and just thought ML had really bad error messages...)

Perhaps it would be better to just have no limit? Is this a performance optimization?

[mn200]

The number was chosen completely arbitrarily, knowing that if it was insufficient the user could always consult the full log (in .hollogs). You probably don't want the complete content of the log-file: if you've successfully processed hundreds of theorems before getting to the error, getting all of that output dumped seems excessive (particularly if running Holmake -k). Equally, I'm happy to try the larger number and to see how it feels in practice.

[digama0]

knowing that if it was insufficient the user could always consult the full log (in .hollogs).

Ah, that's good to know. It might be a good idea to have a message saying as much, i.e. "message truncated, see .hollogs/abcd.log for the full error report".