Runtime exceptions are printed in wrong environment

[haselwarter]

Problem

When a lexing / desugar / typing / runtime / nucleus exception is caught in toplevel.ml, it gets reraised as a toplevel exception. However, when this toplevel exception gets printed, the toplevel state is reset to what it was prior to the evaluation of the current file. For example, if a file extends the nucleus signature, and the exception requires printing of a term judgement, the new symbol is not available in the old signature. This leads to a Fatal error: exception Not_found together with the error message. Similar to #306 .

Example

rule A type
rule B type
rule s : B

let _ = s : A

Fails with

Processing file toplevel_error.m31
Rule A is postulated.
Rule B is postulated.
Rule s is postulated.

Looking up rule s

Toplevel.Error: 
state = initial_environment
File "toplevel_error.m31", line 5, characters 9-13:
Runtime error: unhandled operation ML.coerce 
Looking up rule s

Fatal error: exception Not_found
Raised at file "map.ml", line 135, characters 10-25
Called from file "src/nucleus/signature.ml" (inlined), line 7, characters 48-64
Called from file "src/nucleus/sanity.ml", line 52, characters 14-41
Called from file "src/nucleus/sanity.ml", line 85, characters 27-49
Called from file "src/nucleus/sanity.ml", line 104, characters 22-55
Called from file "src/runtime/runtime.ml", line 700, characters 17-78
Called from file "src/utils/print.ml", line 26, characters 6-19
Called from file "format.ml", line 1252, characters 4-20
Called from file "format.ml", line 1313, characters 16-34
Called from file "format.ml", line 1313, characters 16-34
Called from file "format.ml", line 1252, characters 4-20
Called from file "format.ml", line 1313, characters 16-34
Called from file "format.ml", line 1252, characters 4-20
Called from file "format.ml", line 1252, characters 4-20
Called from file "format.ml", line 1313, characters 16-34
Called from file "src/andromeda.ml", line 183, characters 12-77
Called from file "src/andromeda.ml", line 187, characters 14-63

Compilation exited abnormally with code 2 at Sat Apr 11 15:10:02

(some debugging annotations added)