# HG changeset patch # User wenzelm # Date 1216200024 -7200 # Node ID a811269b577ccd9e2814083783bc9e506b29b0cf # Parent 0dcdf992711464d2b0d67fa6b4637e989f15a1c2 export type id with no_id and create_command; basic support for editor model: insert_command, remove_command; refined command status; misc tuning; diff -r 0dcdf9927114 -r a811269b577c src/Pure/Isar/isar.ML --- a/src/Pure/Isar/isar.ML Tue Jul 15 23:36:26 2008 +0200 +++ b/src/Pure/Isar/isar.ML Wed Jul 16 11:20:24 2008 +0200 @@ -7,12 +7,15 @@ signature ISAR = sig + type id = string + val no_id: id + val create_command: Toplevel.transition -> id val init_point: unit -> unit val state: unit -> Toplevel.state - val exn: unit -> (exn * string) option val context: unit -> Proof.context val goal: unit -> thm val print: unit -> unit + val exn: unit -> (exn * string) option val >> : Toplevel.transition -> bool val >>> : Toplevel.transition list -> unit val linear_undo: int -> unit @@ -23,6 +26,8 @@ val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit val loop: unit -> unit val main: unit -> unit + val insert_command: id -> id -> unit + val remove_command: id -> unit end; structure Isar: ISAR = @@ -61,11 +66,21 @@ val is_proper = fn Theory => true | Proof => true | _ => false; -(* datatype command *) +(* command status *) datatype status = - Initial | - Result of Toplevel.state * (exn * string) option; + Unprocessed | + Running | + Failed of exn * string | + Finished of Toplevel.state; + +fun status_markup Unprocessed = Markup.unprocessed + | status_markup Running = Markup.running + | status_markup (Failed _) = Markup.failed + | status_markup (Finished _) = Markup.finished; + + +(* datatype command *) datatype command = Command of {category: category, @@ -76,7 +91,7 @@ Command {category = category, transition = transition, status = status}; val empty_command = - make_command (Empty, Toplevel.empty, Result (Toplevel.toplevel, NONE)); + make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel); fun map_command f (Command {category, transition, status}) = make_command (f (category, transition, status)); @@ -84,67 +99,85 @@ fun map_status f = map_command (fn (category, transition, status) => (category, transition, f status)); -fun status_markup Initial = Markup.unprocessed - | status_markup (Result (_, NONE)) = Markup.finished - | status_markup (Result (_, SOME _)) = Markup.failed; - (* global collection of identified commands *) fun err_dup id = sys_error ("Duplicate command " ^ quote id); fun err_undef id = sys_error ("Unknown command " ^ quote id); -local - -val empty_commands = Graph.empty: command Graph.T; -val global_commands = ref empty_commands; - -in +local val global_commands = ref (Graph.empty: command Graph.T) in fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f) - handle Graph.DUP id => err_dup id | Graph.UNDEF id => err_undef id; + handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad; + +fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands); -fun init_commands () = change_commands (K empty_commands); +end; + + +fun init_commands () = change_commands (K Graph.empty); fun the_command id = let val Command cmd = if id = no_id then empty_command - else (Graph.get_node (! global_commands) id handle Graph.UNDEF _ => err_undef id) + else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad) in cmd end; fun prev_command id = if id = no_id then NONE else - (case Graph.imm_preds (! global_commands) id handle Graph.UNDEF _ => err_undef id of + (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of [] => NONE | [prev] => SOME prev | _ => sys_error ("Non-linear command dependency " ^ quote id)); -end; +fun next_commands id = + if id = no_id then [] + else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad; + +fun descendant_commands ids = + Graph.all_succs (get_commands ()) (filter_out (fn id => id = no_id) ids) + handle Graph.UNDEF bad => err_undef bad; + + +(* maintain status *) + +fun report_status markup id = Toplevel.status (#transition (the_command id)) markup; + +fun update_status status id = change_commands (Graph.map_node id (map_status (fn old_status => + let + val markup = status_markup status; + val _ = if markup <> status_markup old_status then report_status markup id else (); + in status end))); -fun the_result id = - (case the_command id of - {status = Result res, ...} => res - | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition)); +(* create and dispose commands *) -val the_state = #1 o the_result; -val command_status = Toplevel.status o #transition o the_command; +fun create_command raw_tr = + let + val (id, tr) = identify raw_tr; + val cmd = make_command (category_of tr, tr, Unprocessed); + val _ = change_commands (Graph.new_node (id, cmd)); + in id end; + +fun dispose_command id = + let + val desc = descendant_commands [id]; + val _ = List.app (report_status Markup.disposed) desc; + val _ = change_commands (Graph.del_nodes desc); + in () end; -fun new_command prev (id, cmd) = - change_commands (Graph.new_node (id, cmd) #> prev <> no_id ? Graph.add_edge (prev, id)); +(* final state *) -fun dispose_command id = - (command_status id Markup.disposed; change_commands (Graph.del_nodes [id])); - -fun update_command_status id status = - (change_commands (Graph.map_node id (map_status (K status))); - command_status id (status_markup status)); +fun the_state id = + (case the_command id of + {status = Finished state, ...} => state + | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition)); -(** TTY interaction **) +(** TTY model -- single-threaded **) (* global point *) @@ -155,14 +188,14 @@ end; + fun set_point id = change_point (K id); fun init_point () = set_point no_id; -fun point_result () = NAMED_CRITICAL "Isar" (fn () => - let val id = point () in (id, the_result id) end); +fun point_state () = NAMED_CRITICAL "Isar" (fn () => + let val id = point () in (id, the_state id) end); -fun state () = #1 (#2 (point_result ())); -fun exn () = #2 (#2 (point_result ())); +fun state () = #2 (point_state ()); fun context () = Toplevel.context_of (state ()) @@ -175,25 +208,36 @@ fun print () = Toplevel.print_state false (state ()); -(* interactive state transformations --- NOT THREAD-SAFE! *) +(* global failure status *) + +local val global_exn = ref (NONE: (exn * string) option) in + +fun set_exn err = global_exn := err; +fun exn () = ! global_exn; + +end; + + +(* interactive state transformations *) nonfix >> >>>; fun >> raw_tr = let - val (id, tr) = identify raw_tr; - val (prev, (prev_state, _)) = point_result (); - val category = category_of tr; - val _ = new_command prev (id, make_command (category, tr, Initial)); + val id = create_command raw_tr; + val {category, transition = tr, ...} = the_command id; + val (prev, prev_state) = point_state (); + val _ = if prev <> no_id then change_commands (Graph.add_edge (prev, id)) else (); in (case Toplevel.transition true tr prev_state of NONE => (dispose_command id; false) - | SOME (result as (_, err)) => - (update_command_status id (Result result); - Option.map (Toplevel.error_msg tr) err; - if is_some err orelse category = Control then dispose_command id - else set_point id; - true)) + | SOME (_, SOME err) => + (Toplevel.error_msg tr err; set_exn (SOME err); dispose_command id; true) + | SOME (state, NONE) => + (set_exn NONE; + if category = Control then dispose_command id + else (update_status (Finished state) id; set_point id); + true)) end; fun >>> [] = () @@ -281,5 +325,36 @@ fun main () = toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()}; + + +(** editor model **) + +(* run commands *) (* FIXME *) + +fun run_commands ids = + let + val _ = List.app (update_status Unprocessed) ids; + in () end; + + +(* modify document *) + +fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () => + let + val nexts = next_commands prev; + val _ = change_commands + (fold (fn next => Graph.del_edge (prev, next) #> Graph.add_edge (id, next)) nexts #> + Graph.add_edge (prev, id)); + in descendant_commands [id] end) |> run_commands; + +fun remove_command id = NAMED_CRITICAL "Isar" (fn () => + let + val prev_edge = + (case prev_command id of NONE => K I + | SOME prev => fn next => Graph.add_edge (prev, next)); + val nexts = next_commands id; + val _ = change_commands (fold (fn next => Graph.del_edge (id, next) #> prev_edge next) nexts); + in descendant_commands nexts end) |> run_commands; + end;