# HG changeset patch # User wenzelm # Date 1365014330 -7200 # Node ID 92fda7beace45be0e693108e88241a87298a5b66 # Parent 4c7fdc00bd5929648969f0ae1945b22fc702a308 recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9); diff -r 4c7fdc00bd59 -r 92fda7beace4 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Wed Apr 03 16:45:14 2013 +0200 +++ b/src/Pure/PIDE/command.ML Wed Apr 03 20:38:50 2013 +0200 @@ -63,8 +63,9 @@ fun run int tr st = if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then - (Goal.fork_name "Toplevel.diag" ~1 (fn () => Toplevel.command_exception int tr st); - ([], SOME st)) + Toplevel.setmp_thread_position tr (fn () => + (Goal.fork_name "Toplevel.diag" ~1 (fn () => Toplevel.command_exception int tr st); + ([], SOME st))) () else Toplevel.command_errors int tr st; fun check_cmts tr cmts st =