--- 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;