# HG changeset patch # User wenzelm # Date 1281895987 -7200 # Node ID 6cfc6fce7bfb38899d83fb9eecad4b23c29f861a # Parent 7bdf6c79a2db206a40e497c86ee1d9d666f42b3a document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id; diff -r 7bdf6c79a2db -r 6cfc6fce7bfb src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Sun Aug 15 19:36:13 2010 +0200 +++ b/src/Pure/PIDE/document.ML Sun Aug 15 20:13:07 2010 +0200 @@ -159,10 +159,10 @@ (** global state -- document structure and execution process **) abstype state = State of - {versions: version Inttab.table, (*version_id -> document content*) - commands: Toplevel.transition Inttab.table, (*command_id -> transition function*) - execs: Toplevel.state option lazy Inttab.table, (*exec_id -> execution process*) - execution: unit future list} (*global execution process*) + {versions: version Inttab.table, (*version_id -> document content*) + commands: Toplevel.transition future Inttab.table, (*command_id -> transition (future parsing)*) + execs: Toplevel.state option lazy Inttab.table, (*exec_id -> execution process*) + execution: unit future list} (*global execution process*) with fun make_state (versions, commands, execs, execution) = @@ -173,7 +173,7 @@ val init_state = make_state (Inttab.make [(no_id, empty_version)], - Inttab.make [(no_id, Toplevel.empty)], + Inttab.make [(no_id, Future.value Toplevel.empty)], Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))], []); @@ -198,11 +198,11 @@ map_state (fn (versions, commands, execs, execution) => let val id_string = print_id id; - val tr = + val tr = Future.fork_pri 2 (fn () => Position.setmp_thread_data (Position.id_only id_string) - (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) (); + (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ()); val commands' = - Inttab.update_new (id, Toplevel.put_id id_string tr) commands + Inttab.update_new (id, tr) commands handle Inttab.DUP dup => err_dup "command" dup; in (versions, commands', execs, execution) end); @@ -211,6 +211,9 @@ NONE => err_undef "command" id | SOME tr => tr); +fun join_commands (State {commands, ...}) = + Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands (); + (* command executions *) @@ -244,12 +247,14 @@ let val exec = the_exec state exec_id; val exec_id' = new_id (); - val tr = Toplevel.put_id (print_id exec_id') (the_command state id); + val tr = the_command state id; val exec' = Lazy.lazy (fn () => (case Lazy.force exec of NONE => NONE - | SOME st => Toplevel.run_command name tr st)); + | SOME st => + let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join tr) + in Toplevel.run_command name exec_tr st end)); val state' = define_exec exec_id' exec' state; in (exec_id', (id, exec_id') :: updates, state') end; @@ -277,6 +282,8 @@ val (rev_updates, new_version', state') = fold update_node (node_names_of new_version) ([], new_version, state); val state'' = define_version new_id new_version' state'; + + val _ = join_commands state''; (* FIXME async!? *) in (rev rev_updates, state'') end; end;