document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
authorwenzelm
Sun Aug 15 20:13:07 2010 +0200 (2010-08-15 ago)
changeset 384216cfc6fce7bfb
parent 38420 7bdf6c79a2db
child 38422 f96394dba335
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Aug 15 19:36:13 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Aug 15 20:13:07 2010 +0200
     1.3 @@ -159,10 +159,10 @@
     1.4  (** global state -- document structure and execution process **)
     1.5  
     1.6  abstype state = State of
     1.7 - {versions: version Inttab.table,                   (*version_id -> document content*)
     1.8 -  commands: Toplevel.transition Inttab.table,       (*command_id -> transition function*)
     1.9 -  execs: Toplevel.state option lazy Inttab.table,   (*exec_id -> execution process*)
    1.10 -  execution: unit future list}                      (*global execution process*)
    1.11 + {versions: version Inttab.table,                     (*version_id -> document content*)
    1.12 +  commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
    1.13 +  execs: Toplevel.state option lazy Inttab.table,     (*exec_id -> execution process*)
    1.14 +  execution: unit future list}                        (*global execution process*)
    1.15  with
    1.16  
    1.17  fun make_state (versions, commands, execs, execution) =
    1.18 @@ -173,7 +173,7 @@
    1.19  
    1.20  val init_state =
    1.21    make_state (Inttab.make [(no_id, empty_version)],
    1.22 -    Inttab.make [(no_id, Toplevel.empty)],
    1.23 +    Inttab.make [(no_id, Future.value Toplevel.empty)],
    1.24      Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],
    1.25      []);
    1.26  
    1.27 @@ -198,11 +198,11 @@
    1.28    map_state (fn (versions, commands, execs, execution) =>
    1.29      let
    1.30        val id_string = print_id id;
    1.31 -      val tr =
    1.32 +      val tr = Future.fork_pri 2 (fn () =>
    1.33          Position.setmp_thread_data (Position.id_only id_string)
    1.34 -          (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ();
    1.35 +          (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
    1.36        val commands' =
    1.37 -        Inttab.update_new (id, Toplevel.put_id id_string tr) commands
    1.38 +        Inttab.update_new (id, tr) commands
    1.39            handle Inttab.DUP dup => err_dup "command" dup;
    1.40      in (versions, commands', execs, execution) end);
    1.41  
    1.42 @@ -211,6 +211,9 @@
    1.43      NONE => err_undef "command" id
    1.44    | SOME tr => tr);
    1.45  
    1.46 +fun join_commands (State {commands, ...}) =
    1.47 +  Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands ();
    1.48 +
    1.49  
    1.50  (* command executions *)
    1.51  
    1.52 @@ -244,12 +247,14 @@
    1.53    let
    1.54      val exec = the_exec state exec_id;
    1.55      val exec_id' = new_id ();
    1.56 -    val tr = Toplevel.put_id (print_id exec_id') (the_command state id);
    1.57 +    val tr = the_command state id;
    1.58      val exec' =
    1.59        Lazy.lazy (fn () =>
    1.60          (case Lazy.force exec of
    1.61            NONE => NONE
    1.62 -        | SOME st => Toplevel.run_command name tr st));
    1.63 +        | SOME st =>
    1.64 +            let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join tr)
    1.65 +            in Toplevel.run_command name exec_tr st end));
    1.66      val state' = define_exec exec_id' exec' state;
    1.67    in (exec_id', (id, exec_id') :: updates, state') end;
    1.68  
    1.69 @@ -277,6 +282,8 @@
    1.70      val (rev_updates, new_version', state') =
    1.71        fold update_node (node_names_of new_version) ([], new_version, state);
    1.72      val state'' = define_version new_id new_version' state';
    1.73 +
    1.74 +    val _ = join_commands state'';  (* FIXME async!? *)
    1.75    in (rev rev_updates, state'') end;
    1.76  
    1.77  end;