# HG changeset patch # User huffman # Date 1231884504 28800 # Node ID be8a15ffc511b16595dd5c4b3cdf88474a1ae466 # Parent 4a2482e16934894216be37f95b4896e7ccfaf5f2# Parent b834f95c2532d0c11170ff386bd63cdbdfc6d19d merged diff -r 4a2482e16934 -r be8a15ffc511 src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Tue Jan 13 13:48:21 2009 -0800 +++ b/src/Pure/Isar/isar_document.ML Tue Jan 13 14:08:24 2009 -0800 @@ -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;