Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
always report updates -- required has "handshake";
authorwenzelm
Wed, 06 Jan 2010 23:18:12 +0100
changeset 34285 218fa4267718
parent 34284 33ad3571ad83
child 34286 951aa92d06bb
always report updates -- required has "handshake";
src/Pure/Isar/isar_document.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle