smarter recovery from toplevel type error;

--- a/src/Pure/Isar/toplevel.ML	Sun May 11 20:23:08 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon May 12 12:01:02 2014 +0200
@@ -34,6 +34,7 @@
   val empty: transition
   val name_of: transition -> string
   val pos_of: transition -> Position.T
+  val type_error: transition -> state -> string
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
   val interactive: bool -> transition -> transition
@@ -87,6 +88,8 @@
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command_errors: bool -> transition -> state -> Runtime.error list * state option
   val command_exception: bool -> transition -> state -> state
+  val reset_theory: state -> state option
+  val reset_proof: state -> state option
   type result
   val join_results: result -> (transition * state) list
   val element_result: transition Thy_Syntax.element -> state -> result * state
@@ -335,7 +338,7 @@
 fun at_command tr = command_msg "At " tr;
 
 fun type_error tr state =
-  ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
+  command_msg "Illegal application of " tr ^ " " ^ str_of_state state;
 
 
 (* modify transitions *)
@@ -599,7 +602,7 @@
         Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
       val _ = Timing.protocol_message timing_props timing_result;
     in
-      (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_err)
+      (result, Option.map (fn UNDEF => ERROR (type_error tr state) | exn => exn) opt_err)
     end);
 
 in
@@ -640,6 +643,27 @@
 fun command tr = command_exception (! interact) tr;
 
 
+(* reset state *)
+
+local
+
+fun reset_state check trans st =
+  if check st then NONE
+  else #2 (command_errors false (trans empty) st);
+
+in
+
+val reset_theory = reset_state is_theory forget_proof;
+
+val reset_proof =
+  reset_state is_proof
+    (transaction (fn _ =>
+      (fn Theory (gthy, _) => Skipped_Proof (0, (gthy, gthy))
+        | _ => raise UNDEF)));
+
+end;
+
+
 (* scheduled proof result *)
 
 datatype result =

--- a/src/Pure/PIDE/command.ML	Sun May 11 20:23:08 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Mon May 12 12:01:02 2014 +0200
@@ -194,6 +194,21 @@
 
 local
 
+fun reset_state tr st0 = Toplevel.setmp_thread_position tr (fn () =>
+  let
+    val name = Toplevel.name_of tr;
+    val res =
+      if Keyword.is_theory name andalso not (Keyword.is_theory_begin name) then
+        Toplevel.reset_theory st0
+      else if Keyword.is_proof name then
+        Toplevel.reset_proof st0
+      else NONE;
+  in
+    (case res of
+      NONE => st0
+    | SOME st => (warning (Toplevel.type_error tr st0 ^ " -- resetting state"); st))
+  end) ();
+
 fun run int tr st =
   if Goal.future_enabled 1 andalso Keyword.is_diag (Toplevel.name_of tr) then
     (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
@@ -220,14 +235,16 @@
     SOME prf => status tr (Proof.status_markup prf)
   | NONE => ());
 
-fun eval_state span tr ({malformed, state = st, ...}: eval_state) =
+fun eval_state span tr ({malformed, state, ...}: eval_state) =
   if malformed then
     {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
   else
     let
-      val malformed' = Toplevel.is_malformed tr;
+      val _ = Multithreading.interrupted ();
 
-      val _ = Multithreading.interrupted ();
+      val malformed' = Toplevel.is_malformed tr;
+      val st = reset_state tr state;
+
       val _ = status tr Markup.running;
       val (errs1, result) = run true tr st;
       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');