src/Pure/PIDE/command.ML
changeset 56944 578dc6b4be89
parent 56937 d11d11da0d90
child 57839 d5b0fa6f1f7a
equal deleted inserted replaced
56943:a3abb5222fce 56944:578dc6b4be89
   196 
   196 
   197 fun reset_state tr st0 = Toplevel.setmp_thread_position tr (fn () =>
   197 fun reset_state tr st0 = Toplevel.setmp_thread_position tr (fn () =>
   198   let
   198   let
   199     val name = Toplevel.name_of tr;
   199     val name = Toplevel.name_of tr;
   200     val res =
   200     val res =
   201       if Keyword.is_theory name andalso not (Keyword.is_theory_begin name) then
   201       if Keyword.is_theory_body name then Toplevel.reset_theory st0
   202         Toplevel.reset_theory st0
   202       else if Keyword.is_proof name then Toplevel.reset_proof st0
   203       else if Keyword.is_proof name then
       
   204         Toplevel.reset_proof st0
       
   205       else NONE;
   203       else NONE;
   206   in
   204   in
   207     (case res of
   205     (case res of
   208       NONE => st0
   206       NONE => st0
   209     | SOME st => (warning (Toplevel.type_error tr st0 ^ " -- resetting state"); st))
   207     | SOME st => (warning (Toplevel.type_error tr st0 ^ " -- resetting state"); st))