# HG changeset patch
# User wenzelm
# Date 1215704582 -7200
# Node ID 02b2c9eab4e2f43903d14ef1a220389ffbb3f27a
# Parent  69618a03b6f7e9e92923f3930d3822581109c0e2
tty interaction: do not move point after error;

diff -r 69618a03b6f7 -r 02b2c9eab4e2 src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Thu Jul 10 17:26:27 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Thu Jul 10 17:43:02 2008 +0200
@@ -161,9 +161,6 @@
 
 (* interactive state transformations --- NOT THREAD-SAFE! *)
 
-fun result_error _ NONE = ()
-  | result_error tr (SOME err) = Toplevel.error_msg tr err;
-
 nonfix >> >>>;
 
 fun >> raw_tr =
@@ -175,10 +172,10 @@
   in
     (case Toplevel.transition true tr prev_state of
       NONE => (dispose_command id; false)
-    | SOME result =>
-        (change_command_status id (K (Result result));  (* FIXME outdate all_succs (!?) *)
-          result_error tr (#2 result);
-          if category = Control then dispose_command id
+    | SOME (result as (_, err)) =>
+        (change_command_status id (K (Result result));
+          Option.map (Toplevel.error_msg tr) err;
+          if is_some err orelse category = Control then dispose_command id
           else set_point id;
           true))
   end;