--- a/src/Pure/Isar/isar_document.ML Tue Jan 13 13:02:16 2009 -0800
+++ b/src/Pure/Isar/isar_document.ML Tue Jan 13 22:25:04 2009 +0100
@@ -11,19 +11,25 @@
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;
+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);
+
(** execution states **)
@@ -35,16 +41,16 @@
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
- NONE => (Toplevel.error_msg tr (SYS_ERROR "Cannot terminate here!", ""); NONE)
+ NONE => (Toplevel.error_msg tr (ERROR "Cannot terminate here!", ""); NONE)
| SOME (_, SOME err) => (Toplevel.error_msg tr err; NONE)
| SOME (state', NONE) => SOME state'))))
| Running future =>
@@ -53,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);
@@ -74,27 +81,87 @@
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};
+fun the_entry entries (id: command_id) =
+ (case Symtab.lookup entries id of
+ NONE => err_undef "document entry" id
+ | SOME (Entry entry) => entry);
+
+fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
+
+fun map_entry (id: command_id) f entries =
+ let
+ val {prev, next, state} = the_entry entries id;
+ val (prev', next', state') = f (prev, next, state);
+ in put_entry (id, make_entry prev' next' state') entries end;
+
(* document *)
datatype document = Document of
{dir: Path.T, (*master directory*)
name: string, (*theory name*)
- commands: entry Symtab.table}; (*unique command entries indexed by command_id*)
+ start: command_id, (*empty start command*)
+ entries: entry Symtab.table}; (*unique command entries indexed by command_id*)
+
+fun make_document dir name start entries =
+ Document {dir = dir, name = name, start = start, entries = entries};
+
+fun map_entries f (Document {dir, name, start, entries}) =
+ make_document dir name start (f 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 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);
-fun make_document dir name commands = Document {dir = dir, name = name, commands = commands};
+
+(* modify entries *)
+
+fun insert_entry (id: command_id, id2: command_id) = map_entries (fn entries =>
+ let val {prev, next, state} = the_entry entries id in
+ entries |>
+ (case next of
+ NONE => put_entry (id2, make_entry (SOME id) NONE NONE)
+ | SOME id3 =>
+ 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 (id: command_id) = map_entries (fn entries =>
+ let val {prev, next, state} = the_entry entries id in
+ entries |>
+ (case next of
+ NONE => error ("Missing next entry: " ^ quote id)
+ | SOME id2 =>
+ (case #next (the_entry entries id2) of
+ NONE => put_entry (id, make_entry prev NONE state)
+ | SOME id3 =>
+ put_entry (id, make_entry prev (SOME id3) state) #>
+ put_entry (id3, make_entry (SOME id) (#next (the_entry entries id3)) NONE)))
+ end);
(** global configuration **)
-fun err_dup kind id = sys_error ("Duplicate " ^ kind ^ ": " ^ quote id);
-fun err_undef kind id = sys_error ("Unknown " ^ kind ^ ": " ^ quote id);
-
local
val global_states = ref (Symtab.empty: state Symtab.table);
val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
@@ -125,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
- | _ => sys_error ("Unfinished state " ^ id));
+ | SOME (State state) => state);
fun define_command id tr =
@@ -136,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 =
@@ -146,27 +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);
+(* 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 commands = Symtab.make [(id, make_entry NONE NONE id)];
- val _ = define_document id (make_document dir name commands);
+ 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 {dir, name, commands} = the_document id;
- val commands' = sys_error "FIXME";
- val _ = define_document new_id (make_document dir name commands');
+ 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' =
+ 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) = sys_error "FIXME";
-
(** concrete syntax **)
@@ -185,14 +294,15 @@
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;
-end;