equal
deleted
inserted
replaced
61 |
61 |
62 local |
62 local |
63 |
63 |
64 fun run int tr st = |
64 fun run int tr st = |
65 if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then |
65 if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then |
66 (Goal.fork_name "Toplevel.diag" ~1 (fn () => Toplevel.command_exception int tr st); |
66 Toplevel.setmp_thread_position tr (fn () => |
67 ([], SOME st)) |
67 (Goal.fork_name "Toplevel.diag" ~1 (fn () => Toplevel.command_exception int tr st); |
|
68 ([], SOME st))) () |
68 else Toplevel.command_errors int tr st; |
69 else Toplevel.command_errors int tr st; |
69 |
70 |
70 fun check_cmts tr cmts st = |
71 fun check_cmts tr cmts st = |
71 Toplevel.setmp_thread_position tr |
72 Toplevel.setmp_thread_position tr |
72 (fn () => cmts |
73 (fn () => cmts |