# HG changeset patch
# User wenzelm
# Date 1262816292 -3600
# Node ID 218fa42677184fa6892199734e82dde97156c9c6
# Parent  33ad3571ad8355ef9a29e0a5bfb7db08204ecd53
always report updates -- required has "handshake";

diff -r 33ad3571ad83 -r 218fa4267718 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Wed Jan 06 22:21:25 2010 +0100
+++ b/src/Pure/Isar/isar_document.ML	Wed Jan 06 23:18:12 2010 +0100
@@ -232,11 +232,10 @@
       in put_state state_id' state' end;
   in (state_id', ((id, state_id'), make_state') :: updates) end;
 
-fun report_updates [] = ()
-  | report_updates updates =
-      implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
-      |> Markup.markup Markup.assign
-      |> Output.status;
+fun report_updates updates =
+  implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
+  |> Markup.markup Markup.assign
+  |> Output.status;
 
 in