changeset 58928 | 23d0ffd48006 |
parent 57649 | a43898f76ae9 |
child 59086 | 94b2690ad494 |
--- a/src/Pure/PIDE/session.ML Fri Nov 07 16:22:25 2014 +0100 +++ b/src/Pure/PIDE/session.ML Fri Nov 07 16:36:55 2014 +0100 @@ -54,7 +54,6 @@ (Execution.shutdown (); Thy_Info.finish (); Present.finish (); - Outer_Syntax.check_syntax (); Future.shutdown (); Event_Timer.shutdown (); Future.shutdown ();