src/Pure/PIDE/document.ML
changeset 40398 cdda2847a91e
parent 40391 b0dafbfc05b7
child 40449 9c390868d255
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Nov 06 20:18:06 2010 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Nov 06 20:59:59 2010 +0100
     1.3 @@ -119,10 +119,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 + {versions: version Inttab.table,  (*version_id -> document content*)
     1.9    commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
    1.10 -  execs: Toplevel.state option lazy Inttab.table,     (*exec_id -> execution process*)
    1.11 -  execution: unit future list}                        (*global execution process*)
    1.12 +  execs: (bool * Toplevel.state) lazy Inttab.table,  (*exec_id -> execution process*)
    1.13 +  execution: unit future list}  (*global execution process*)
    1.14  with
    1.15  
    1.16  fun make_state (versions, commands, execs, execution) =
    1.17 @@ -134,7 +134,7 @@
    1.18  val init_state =
    1.19    make_state (Inttab.make [(no_id, empty_version)],
    1.20      Inttab.make [(no_id, Future.value Toplevel.empty)],
    1.21 -    Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],
    1.22 +    Inttab.make [(no_id, Lazy.value (true, Toplevel.toplevel))],
    1.23      []);
    1.24  
    1.25  
    1.26 @@ -235,19 +235,21 @@
    1.27          val (errs, result) = run int tr st;
    1.28          val _ = timing tr (end_timing start);
    1.29          val _ = List.app (Toplevel.error_msg tr) errs;
    1.30 -        val _ =
    1.31 +        val res =
    1.32            (case result of
    1.33 -            NONE => Toplevel.status tr Markup.failed
    1.34 +            NONE => (Toplevel.status tr Markup.failed; (false, st))
    1.35            | SOME st' =>
    1.36               (Toplevel.status tr Markup.finished;
    1.37                proof_status tr st';
    1.38 -              if int then () else async_state tr st'));
    1.39 -      in result end
    1.40 +              if int then () else async_state tr st';
    1.41 +              (true, st')));
    1.42 +      in res end
    1.43    | Exn.Exn exn =>
    1.44        if Exn.is_interrupt exn then reraise exn
    1.45        else
    1.46         (Toplevel.error_msg tr (ML_Compiler.exn_message exn);
    1.47 -        Toplevel.status tr Markup.failed; NONE));
    1.48 +        Toplevel.status tr Markup.failed;
    1.49 +        (false, Toplevel.toplevel)));
    1.50  
    1.51  end;
    1.52  
    1.53 @@ -272,11 +274,10 @@
    1.54      val future_tr = the_command state id;
    1.55      val exec' =
    1.56        Lazy.lazy (fn () =>
    1.57 -        (case Lazy.force exec of
    1.58 -          NONE => NONE
    1.59 -        | SOME st =>
    1.60 -            let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
    1.61 -            in run_command name exec_tr st end));
    1.62 +        let
    1.63 +          val st = #2 (Lazy.force exec);
    1.64 +          val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
    1.65 +        in 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