1.1 --- a/src/Pure/PIDE/document.ML	Sun Aug 14 08:45:38 2011 -0700
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 15 14:54:36 2011 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4  abstype state = State of
     1.5   {versions: version Inttab.table,  (*version_id -> document content*)
     1.6    commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
     1.7 -  execs: (bool * Toplevel.state) lazy Inttab.table,  (*exec_id -> execution process*)
     1.8 +  execs: Toplevel.state lazy Inttab.table,  (*exec_id -> execution process*)
     1.9    execution: unit future list}  (*global execution process*)
    1.10  with
    1.11  
    1.12 @@ -170,7 +170,7 @@
    1.13  val init_state =
    1.14    make_state (Inttab.make [(no_id, empty_version)],
    1.15      Inttab.make [(no_id, Future.value Toplevel.empty)],
    1.16 -    Inttab.make [(no_id, Lazy.value (true, Toplevel.toplevel))],
    1.17 +    Inttab.make [(no_id, Lazy.value Toplevel.toplevel)],
    1.18      []);
    1.19  
    1.20  
    1.21 @@ -229,7 +229,7 @@
    1.22      val last = get_last (node_of (the_version state version_id) name);
    1.23      val st =
    1.24        (case Lazy.peek (the_exec state last) of
    1.25 -        SOME result => #2 (Exn.release result)
    1.26 +        SOME result => Exn.release result
    1.27        | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos));
    1.28    in Toplevel.end_theory pos st end;
    1.29  
    1.30 @@ -300,12 +300,12 @@
    1.31      val _ = List.app (Toplevel.error_msg tr) errs;
    1.32    in
    1.33      (case result of
    1.34 -      NONE => (Toplevel.status tr Markup.failed; (false, st))
    1.35 +      NONE => (Toplevel.status tr Markup.failed; st)
    1.36      | SOME st' =>
    1.37         (Toplevel.status tr Markup.finished;
    1.38          proof_status tr st';
    1.39          if do_print then async_state tr st' else ();
    1.40 -        (true, st')))
    1.41 +        st'))
    1.42    end;
    1.43  
    1.44  end;
    1.45 @@ -332,7 +332,7 @@
    1.46      val exec' =
    1.47        Lazy.lazy (fn () =>
    1.48          let
    1.49 -          val st = #2 (Lazy.force exec);
    1.50 +          val st = Lazy.force exec;
    1.51            val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
    1.52          in run_command node_info exec_tr st end);
    1.53      val state' = define_exec exec_id' exec' state;