--- a/src/Pure/Isar/isar_document.ML Tue Jan 13 14:31:02 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML Tue Jan 13 17:34:12 2009 +0100
@@ -24,6 +24,11 @@
type command_id = string;
type state_id = string;
+val no_id = "";
+
+fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
+fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);
+
(** execution states **)
@@ -44,7 +49,7 @@
(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 =>
@@ -78,23 +83,78 @@
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);
+
+
+fun fold_entries 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 make_document dir name commands = Document {dir = dir, name = name, commands = commands};
+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
+ entries |>
+ (case next of
+ NONE => put_entry (id2, make_entry (SOME id) NONE state2)
+ | 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)
+ end);
+
+fun delete_after_entry (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 =>
+ 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))
+ 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);
@@ -126,7 +186,7 @@
(case Symtab.lookup (get_states ()) id of
NONE => err_undef "state" id
| SOME (State {status as Finished state, ...}) => state
- | _ => sys_error ("Unfinished state " ^ id));
+ | _ => error ("Unfinished state " ^ id));
fun define_command id tr =
@@ -149,23 +209,27 @@
| SOME doc => doc);
+(* document editing *)
+
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 id)];
+ val _ = define_document id (make_document dir name id entries);
in () end;
fun edit_document (id: document_id) (new_id: document_id) edits =
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' =
+ 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';
in () end;
-fun end_document (id: document_id) = sys_error "FIXME";
+fun end_document (id: document_id) = error "FIXME";
@@ -196,3 +260,4 @@
end;
end;
+