(** global state -- document structure and execution process **)

 (** global state -- document structure and execution process **)

 abstype state = State of

 abstype state = State of

  {versions: version Inttab.table,  (*version_id -> document content*)

  {versions: version Inttab.table,  (*version_id -> document content*)

   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)

   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)

   execution: unit future list}  (*global execution process*)

   execution: unit future list}  (*global execution process*)

 with

 with

 fun make_state (versions, commands, execs, execution) =

 fun make_state (versions, commands, execs, execution) =

   State {versions = versions, commands = commands, execs = execs, execution = execution};

   State {versions = versions, commands = commands, execs = execs, execution = execution};

   make_state (f (versions, commands, execs, execution));

   make_state (f (versions, commands, execs, execution));

 val init_state =

 val init_state =

   make_state (Inttab.make [(no_id, empty_version)],

   make_state (Inttab.make [(no_id, empty_version)],

     Inttab.make [(no_id, Future.value Toplevel.empty)],

     Inttab.make [(no_id, Future.value Toplevel.empty)],

     []);

     []);

 (* document versions *)

 (* document versions *)

 fun get_theory state version_id pos name =

 fun get_theory state version_id pos name =

   let

   let

     val last = get_last (node_of (the_version state version_id) name);

     val last = get_last (node_of (the_version state version_id) name);

     val st =

     val st =

       (case Lazy.peek (the_exec state last) of

       (case Lazy.peek (the_exec state last) of

       | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos));

       | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos));

   in Toplevel.end_theory pos st end;

   in Toplevel.end_theory pos st end;

 (* document execution *)

 (* document execution *)

       else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;

       else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;

     val _ = timing tr (Timing.result start);

     val _ = timing tr (Timing.result start);

     val _ = List.app (Toplevel.error_msg tr) errs;

     val _ = List.app (Toplevel.error_msg tr) errs;

   in

   in

     (case result of

     (case result of

     | SOME st' =>

     | SOME st' =>

        (Toplevel.status tr Markup.finished;

        (Toplevel.status tr Markup.finished;

         proof_status tr st';

         proof_status tr st';

         if do_print then async_state tr st' else ();

         if do_print then async_state tr st' else ();

   end;

   end;

 end;

 end;

     val exec_id' = new_id ();

     val exec_id' = new_id ();

     val future_tr = the_command state id;

     val future_tr = the_command state id;

     val exec' =

     val exec' =

       Lazy.lazy (fn () =>

       Lazy.lazy (fn () =>

         let

         let

           val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);

           val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);

         in run_command node_info exec_tr st end);

         in run_command node_info exec_tr st end);

     val state' = define_exec exec_id' exec' state;

     val state' = define_exec exec_id' exec' state;

   in (exec_id', (id, exec_id') :: updates, state') end;

   in (exec_id', (id, exec_id') :: updates, state') end;