changeset 62505 | 9e2a65912111 |
parent 61077 | 06cca32aa519 |
child 62826 | eb94e570c1a4 |
--- a/src/Pure/PIDE/document.ML Thu Mar 03 14:03:06 2016 +0100 +++ b/src/Pure/PIDE/document.ML Thu Mar 03 15:23:02 2016 +0100 @@ -486,7 +486,7 @@ else NONE | NONE => NONE)) node () else ()) - handle exn => (Output.system_message (Runtime.exn_message exn); reraise exn); + handle exn => (Output.system_message (Runtime.exn_message exn); Exn.reraise exn); val future = (singleton o Future.forks) {name = "theory:" ^ name,