# HG changeset patch
# User wenzelm
# Date 1232016922 -3600
# Node ID 5dfe03f423c418e65cc51725238f995a638c7158
# Parent  8fc3aeece219be5bfe75d3a33c8c5bb21e6acec3
edit_document: proper edits/edit markup, including the document id;
tuned;

diff -r 8fc3aeece219 -r 5dfe03f423c4 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Thu Jan 15 11:53:49 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML	Thu Jan 15 11:55:22 2009 +0100
@@ -45,6 +45,14 @@
 
 fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
 
+fun put_entry_state (id: command_id) state entries =
+  let val {next, ...} = the_entry entries id
+  in put_entry (id, make_entry next state) entries end;
+
+fun reset_state id = put_entry_state id NONE;
+fun set_state (id, state_id) = put_entry_state id (SOME state_id);
+
+
 
 (* document *)
 
@@ -95,9 +103,7 @@
         entries |>
           (case #next (the_entry entries id2) of
             NONE => put_entry (id, make_entry NONE state)
-          | SOME id3 =>
-              put_entry (id, make_entry (SOME id3) state) #>
-              put_entry (id3, make_entry (#next (the_entry entries id3)) NONE)))
+          | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_state id3))
   end);
 
 
@@ -197,30 +203,33 @@
         val state' = update_state (the_command id) (the_state state_id);
         val _ = define_state state_id' state';
       in (state_id', (id, state_id') :: updates) end;
-
-    fun update_state (id, state_id) entries =
-      let val _ = Output.status (Markup.markup (Markup.command_state id state_id) "")
-      in put_entry (id, make_entry (#next (the_entry entries id)) (SOME state_id)) entries end;
   in
     (case find_entries is_changed old_document of
-      NONE => new_document
+      NONE => ([], new_document)
     | SOME (prev, id) =>
         let
           val _ = fold_entries (SOME id) cancel_state old_document ();
           val prev_state_id = the (#state (the_entry new_entries (the prev)));
           val (_, updates) = fold_entries (SOME id) new_state new_document (prev_state_id, []);
-          val new_document' = new_document |> map_entries (fold update_state updates);
-        in new_document' end)
+          val new_document' = new_document |> map_entries (fold set_state updates);
+        in (updates, new_document') end)
   end;
 
+fun report_updates _ [] = ()
+  | report_updates (document_id: document_id) updates =
+      implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
+      |> Markup.markup (Markup.edits document_id)
+      |> Output.status;
+
 fun edit_document (id: document_id) (id': document_id) edits =
   let
     val document = Document (the_document id);
-    val document' =
+    val (updates, document') =
       document
       |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits
       |> update_states document;
     val _ = define_document id' document';
+    val _ = report_updates id' updates;
   in () end;