| changeset 55386 | 0c15ac6edcf7 |
| parent 53192 | 04df1d236e1c |
| 55385:169e12bbf9a3 | 55386:0c15ac6edcf7 |
|---|---|
55 Thy_Info.finish (); |
55 Thy_Info.finish (); |
56 Present.finish (); |
56 Present.finish (); |
57 Outer_Syntax.check_syntax (); |
57 Outer_Syntax.check_syntax (); |
58 Future.shutdown (); |
58 Future.shutdown (); |
59 Event_Timer.shutdown (); |
59 Event_Timer.shutdown (); |
60 Future.shutdown (); |
|
60 session_finished := true); |
61 session_finished := true); |
61 |
62 |
62 |
63 |
63 (** protocol handlers **) |
64 (** protocol handlers **) |
64 |
65 |