src/Pure/PIDE/command.ML

   let
     val name = Toplevel.name_of tr;
     val res =
       if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
       else if Keyword.is_proof keywords name then Toplevel.reset_proof st0
+      else if Keyword.is_theory_end keywords name then
+        (case Toplevel.reset_notepad st0 of
+          NONE => Toplevel.reset_theory st0
+        | some => some)
       else NONE;
   in
     (case res of
       NONE => st0
     | SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st))