src/Pure/PIDE/document.ML
changeset 40398 cdda2847a91e
parent 40391 b0dafbfc05b7
child 40449 9c390868d255
equal deleted inserted replaced
40397:4ad71312a192 40398:cdda2847a91e
   117 
   117 
   118 
   118 
   119 (** global state -- document structure and execution process **)
   119 (** global state -- document structure and execution process **)
   120 
   120 
   121 abstype state = State of
   121 abstype state = State of
   122  {versions: version Inttab.table,                     (*version_id -> document content*)
   122  {versions: version Inttab.table,  (*version_id -> document content*)
   123   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
   123   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
   124   execs: Toplevel.state option lazy Inttab.table,     (*exec_id -> execution process*)
   124   execs: (bool * Toplevel.state) lazy Inttab.table,  (*exec_id -> execution process*)
   125   execution: unit future list}                        (*global execution process*)
   125   execution: unit future list}  (*global execution process*)
   126 with
   126 with
   127 
   127 
   128 fun make_state (versions, commands, execs, execution) =
   128 fun make_state (versions, commands, execs, execution) =
   129   State {versions = versions, commands = commands, execs = execs, execution = execution};
   129   State {versions = versions, commands = commands, execs = execs, execution = execution};
   130 
   130 
   132   make_state (f (versions, commands, execs, execution));
   132   make_state (f (versions, commands, execs, execution));
   133 
   133 
   134 val init_state =
   134 val init_state =
   135   make_state (Inttab.make [(no_id, empty_version)],
   135   make_state (Inttab.make [(no_id, empty_version)],
   136     Inttab.make [(no_id, Future.value Toplevel.empty)],
   136     Inttab.make [(no_id, Future.value Toplevel.empty)],
   137     Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],
   137     Inttab.make [(no_id, Lazy.value (true, Toplevel.toplevel))],
   138     []);
   138     []);
   139 
   139 
   140 
   140 
   141 (* document versions *)
   141 (* document versions *)
   142 
   142 
   233         val int = is_some (Toplevel.init_of tr);
   233         val int = is_some (Toplevel.init_of tr);
   234         val start = start_timing ();
   234         val start = start_timing ();
   235         val (errs, result) = run int tr st;
   235         val (errs, result) = run int tr st;
   236         val _ = timing tr (end_timing start);
   236         val _ = timing tr (end_timing start);
   237         val _ = List.app (Toplevel.error_msg tr) errs;
   237         val _ = List.app (Toplevel.error_msg tr) errs;
   238         val _ =
   238         val res =
   239           (case result of
   239           (case result of
   240             NONE => Toplevel.status tr Markup.failed
   240             NONE => (Toplevel.status tr Markup.failed; (false, st))
   241           | SOME st' =>
   241           | SOME st' =>
   242              (Toplevel.status tr Markup.finished;
   242              (Toplevel.status tr Markup.finished;
   243               proof_status tr st';
   243               proof_status tr st';
   244               if int then () else async_state tr st'));
   244               if int then () else async_state tr st';
   245       in result end
   245               (true, st')));
       
   246       in res end
   246   | Exn.Exn exn =>
   247   | Exn.Exn exn =>
   247       if Exn.is_interrupt exn then reraise exn
   248       if Exn.is_interrupt exn then reraise exn
   248       else
   249       else
   249        (Toplevel.error_msg tr (ML_Compiler.exn_message exn);
   250        (Toplevel.error_msg tr (ML_Compiler.exn_message exn);
   250         Toplevel.status tr Markup.failed; NONE));
   251         Toplevel.status tr Markup.failed;
       
   252         (false, Toplevel.toplevel)));
   251 
   253 
   252 end;
   254 end;
   253 
   255 
   254 
   256 
   255 
   257 
   270     val exec = the_exec state exec_id;
   272     val exec = the_exec state exec_id;
   271     val exec_id' = new_id ();
   273     val exec_id' = new_id ();
   272     val future_tr = the_command state id;
   274     val future_tr = the_command state id;
   273     val exec' =
   275     val exec' =
   274       Lazy.lazy (fn () =>
   276       Lazy.lazy (fn () =>
   275         (case Lazy.force exec of
   277         let
   276           NONE => NONE
   278           val st = #2 (Lazy.force exec);
   277         | SOME st =>
   279           val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
   278             let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
   280         in run_command name exec_tr st end);
   279             in run_command name exec_tr st end));
       
   280     val state' = define_exec exec_id' exec' state;
   281     val state' = define_exec exec_id' exec' state;
   281   in (exec_id', (id, exec_id') :: updates, state') end;
   282   in (exec_id', (id, exec_id') :: updates, state') end;
   282 
   283 
   283 in
   284 in
   284 
   285