# HG changeset patch
# User wenzelm
# Date 1231881649 -3600
# Node ID c9bb4e06d1730f66ec414af7a91947b60f8509df
# Parent  d98fe0c504a87e87ab5451a5b2278d4b2b0babe5
misc internal rearrangements;
fold_entries: really start from start, or optional position;
added find_first_entries, find_first_entries;
insert_entry: always invalidate next state;
added refresh_states (partial version);

diff -r d98fe0c504a8 -r c9bb4e06d173 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Tue Jan 13 17:34:12 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML	Tue Jan 13 22:20:49 2009 +0100
@@ -11,20 +11,21 @@
   type document_id = string
   val define_command: command_id -> Toplevel.transition -> unit
   val begin_document: document_id -> Path.T -> unit
+  val end_document: document_id -> unit
   val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
-  val end_document: document_id -> unit
 end;
 
 structure IsarDocument: ISAR_DOCUMENT =
 struct
 
+
 (* unique identifiers *)
 
 type document_id = string;
 type command_id = string;
 type state_id = string;
 
-val no_id = "";
+fun new_id () = "isabelle:" ^ serial_string ();
 
 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
 fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);
@@ -40,12 +41,12 @@
   Failed |
   Finished of Toplevel.state;
 
-fun status_markup Unprocessed = Markup.unprocessed
-  | status_markup (Running future) = Markup.running (Task_Queue.str_of_task (Future.task_of future))
-  | status_markup Failed = Markup.failed
-  | status_markup (Finished _) = Markup.finished;
+fun markup_status Unprocessed = Markup.unprocessed
+  | markup_status (Running future) = Markup.running (Task_Queue.str_of_task (Future.task_of future))
+  | markup_status Failed = Markup.failed
+  | markup_status (Finished _) = Markup.finished;
 
-fun status_update tr state status =
+fun update_status retry tr state status =
   (case status of
     Unprocessed => SOME (Running (Future.fork_pri 1 (fn () =>
       (case Toplevel.transition true tr state of
@@ -58,6 +59,7 @@
       | SOME (Exn.Result NONE) => SOME Failed
       | SOME (Exn.Result (SOME state')) => SOME (Finished state')
       | SOME (Exn.Exn exn) => (Toplevel.error_msg tr (exn, ""); SOME Failed))
+  | Failed => if retry then SOME Unprocessed else NONE
   | _ => NONE);
 
 
@@ -79,7 +81,7 @@
 datatype entry = Entry of
  {prev: command_id option,
   next: command_id option,
-  state: state_id};
+  state: state_id option};
 
 fun make_entry prev next state = Entry {prev = prev, next = next, state = state};
 
@@ -112,31 +114,38 @@
   make_document dir name start (f entries);
 
 
-fun fold_entries f (Document {start, entries, ...}) =
+(* iterating entries *)
+
+fun fold_entries opt_id f (Document {start, entries, ...}) =
+  let
+    fun apply NONE x = x
+      | apply (SOME id) x = apply (#next (the_entry entries id)) (f id x);
+  in if is_some opt_id then apply opt_id else apply (SOME start) end;
+
+fun get_first_entries opt_id f (Document {start, entries, ...}) =
   let
-    fun descend NONE x = x
-      | descend (SOME id) x = descend_next id (f id x)
-    and descend_next id = descend (#next (the_entry entries id));
-  in descend_next start end;
+    fun get NONE = NONE
+      | get (SOME id) = (case f id of NONE => get (#next (the_entry entries id)) | some => some);
+  in if is_some opt_id then get opt_id else get (SOME start) end;
 
+fun find_first_entries opt_id P =
+  get_first_entries opt_id (fn x => if P x then SOME x else NONE);
+
+
+(* modify entries *)
 
 fun insert_entry (id: command_id, id2: command_id) = map_entries (fn entries =>
-  let
-    val {prev, next, state} = the_entry entries id;
-    val state2 = no_id;
-  in
+  let val {prev, next, state} = the_entry entries id in
     entries |>
       (case next of
-        NONE => put_entry (id2, make_entry (SOME id) NONE state2)
+        NONE => put_entry (id2, make_entry (SOME id) NONE NONE)
       | SOME id3 =>
-          let val {next = next3, state = state3, ...} = the_entry entries id3 in
-            put_entry (id, make_entry prev (SOME id2) state) #>
-            put_entry (id2, make_entry (SOME id) (SOME id3) state2) #>
-            put_entry (id3, make_entry (SOME id2) next3 state3)
-          end)
+          put_entry (id, make_entry prev (SOME id2) state) #>
+          put_entry (id2, make_entry (SOME id) (SOME id3) NONE) #>
+          put_entry (id3, make_entry (SOME id2) (#next (the_entry entries id3)) NONE))
   end);
 
-fun delete_after_entry (id: command_id) = map_entries (fn entries =>
+fun delete_after (id: command_id) = map_entries (fn entries =>
   let val {prev, next, state} = the_entry entries id in
     entries |>
       (case next of
@@ -145,10 +154,8 @@
           (case #next (the_entry entries id2) of
             NONE => put_entry (id, make_entry prev NONE state)
           | SOME id3 =>
-              let val {next = next3, state = state3, ...} = the_entry entries id3 in
-                put_entry (id, make_entry prev (SOME id3) state) #>
-                put_entry (id3, make_entry (SOME id) next3 state3)
-              end))
+              put_entry (id, make_entry prev (SOME id3) state) #>
+              put_entry (id3, make_entry (SOME id) (#next (the_entry entries id3)) NONE)))
   end);
 
 
@@ -185,8 +192,7 @@
 fun the_state (id: state_id) =
   (case Symtab.lookup (get_states ()) id of
     NONE => err_undef "state" id
-  | SOME (State {status as Finished state, ...}) => state
-  | _ => error ("Unfinished state " ^ id));
+  | SOME (State state) => state);
 
 
 fun define_command id tr =
@@ -196,7 +202,7 @@
 fun the_command (id: command_id) =
   (case Symtab.lookup (get_commands ()) id of
     NONE => err_undef "command" id
-  | SOME cmd => cmd);
+  | SOME tr => tr);
 
 
 fun define_document (id: document_id) document =
@@ -206,31 +212,70 @@
 fun the_document (id: document_id) =
   (case Symtab.lookup (get_documents ()) id of
     NONE => err_undef "document" id
-  | SOME doc => doc);
+  | SOME (Document doc) => doc);
 
 
-(* document editing *)
+(* begin/end document *)
 
 fun begin_document (id: document_id) path =
   let
     val (dir, name) = ThyLoad.split_thy_path path;
     val _ = define_command id Toplevel.empty;
     val _ = define_state id (make_state NONE id (Finished Toplevel.toplevel));
-    val entries = Symtab.make [(id, make_entry NONE NONE id)];
+    val entries = Symtab.make [(id, make_entry NONE NONE (SOME id))];
     val _ = define_document id (make_document dir name id entries);
   in () end;
 
-fun edit_document (id: document_id) (new_id: document_id) edits =
+fun end_document (id: document_id) = error "FIXME";
+
+
+(* document editing *)
+
+fun refresh_states old_document new_document =
   let
+    val Document {entries = old_entries, ...} = old_document;
+    val Document {entries = new_entries, ...} = new_document;
+
+    fun is_changed id =
+      (case try (the_entry new_entries) id of
+        SOME {state = SOME _, ...} => false
+      | _ => true);
+
+    fun cancel_state id () =
+      (case the_entry old_entries id of
+        {state = SOME state_id, ...} =>
+          (case the_state state_id of
+            {status = Running future, ...} => Future.cancel future
+          | _ => ())
+      | _ => ());
+
+    fun new_state id (prev_state_id, new_states) =
+      let
+        val state_id = new_id ();
+        val state = make_state prev_state_id id Unprocessed;
+        val _ = define_state state_id state;
+      in (SOME state_id, (state_id, state) :: new_states) end;
+  in
+    (case find_first_entries NONE is_changed old_document of
+      NONE => new_document
+    | SOME id =>
+        let
+          val _ = fold_entries (SOME id) cancel_state old_document ();
+          val (_, new_states) = fold_entries (SOME id) new_state new_document (NONE, []);
+          (* FIXME update states *)
+        in new_document end)
+  end;
+
+fun edit_document (id: document_id) (id': document_id) edits =
+  let
+    val document = Document (the_document id);
     val document' =
-      fold (fn (id, SOME id2) => insert_entry (id, id2) | (id, NONE) => delete_after_entry id)
-        edits (the_document id);
-    (* FIXME update states *)
-    val _ = define_document new_id document';
+      document
+      |> fold (fn (id, SOME id2) => insert_entry (id, id2) | (id, NONE) => delete_after id) edits
+      |> refresh_states document;
+    val _ = define_document id' document';
   in () end;
 
-fun end_document (id: document_id) = error "FIXME";
-
 
 
 (** concrete syntax **)
@@ -249,14 +294,14 @@
       Toplevel.imperative (fn () => begin_document id (Path.explode path))));
 
 val _ =
+  OuterSyntax.internal_command "Isar.end_document"
+    (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
+
+val _ =
   OuterSyntax.internal_command "Isar.edit_document"
     (P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE)
       >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => end_document id new_id edits)));
 
-val _ =
-  OuterSyntax.internal_command "Isar.end_document"
-    (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
-
 end;
 
 end;