# HG changeset patch
# User wenzelm
# Date 1216588018 -7200
# Node ID 34e7236443f3672d35a5fa4454ee4964a9a3e7aa
# Parent  a5019f9ae06812fa0a51e4f952d7f68f81847362
tty loop: do not report status;

diff -r a5019f9ae068 -r 34e7236443f3 src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Sun Jul 20 23:06:55 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Sun Jul 20 23:06:58 2008 +0200
@@ -156,11 +156,12 @@
 
 fun report_status markup id = Toplevel.status (#transition (the_command id)) markup;
 
-fun update_status status id = change_commands (Graph.map_node id (map_status (fn old_status =>
-  let
-    val markup = status_markup status;
-    val _ = if markup <> status_markup old_status then report_status markup id else ();
-  in status end)));
+fun update_status status id = change_commands (Graph.map_node id (map_status (K status)));
+
+fun report_update_status status id =
+  change_commands (Graph.map_node id (map_status (fn old_status =>
+    let val markup = status_markup status
+    in if markup <> status_markup old_status then report_status markup id else (); status end)));
 
 
 (* create and dispose commands *)
@@ -348,10 +349,10 @@
   | SOME state =>
       (case run true (#transition (the_command id)) state of
         NONE => ()
-      | SOME status => update_status status id));
+      | SOME status => report_update_status status id));
       
 fun rerun_commands ids =
-  (List.app (update_status Unprocessed) ids; List.app try_run ids);
+  (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
 
 
 (* modify document *)