1.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 31 23:28:21 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 31 23:46:49 2010 +0200
     1.3 @@ -192,6 +192,59 @@
     1.4  
     1.5  
     1.6  
     1.7 +(* toplevel transactions *)
     1.8 +
     1.9 +local
    1.10 +
    1.11 +fun proof_status tr st =
    1.12 +  (case try Toplevel.proof_of st of
    1.13 +    SOME prf => Toplevel.status tr (Proof.status_markup prf)
    1.14 +  | NONE => ());
    1.15 +
    1.16 +fun async_state tr st =
    1.17 +  if Toplevel.print_of tr then
    1.18 +    ignore
    1.19 +      (Future.fork
    1.20 +        (fn () =>
    1.21 +          Toplevel.setmp_thread_position tr
    1.22 +            (fn () => Future.status (fn () => Toplevel.print_state false st)) ()))
    1.23 +  else ();
    1.24 +
    1.25 +in
    1.26 +
    1.27 +fun run_command thy_name tr st =
    1.28 +  (case
    1.29 +      (case Toplevel.init_of tr of
    1.30 +        SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
    1.31 +      | NONE => Exn.Result ()) of
    1.32 +    Exn.Result () =>
    1.33 +      let
    1.34 +        val int = is_some (Toplevel.init_of tr);
    1.35 +        val (errs, result) =
    1.36 +          (case Toplevel.transition int tr st of
    1.37 +            SOME (st', NONE) => ([], SOME st')
    1.38 +          | SOME (_, SOME exn_info) =>
    1.39 +              (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
    1.40 +                [] => raise Exn.Interrupt
    1.41 +              | errs => (errs, NONE))
    1.42 +          | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
    1.43 +        val _ = List.app (Toplevel.error_msg tr) errs;
    1.44 +        val _ =
    1.45 +          (case result of
    1.46 +            NONE => Toplevel.status tr Markup.failed
    1.47 +          | SOME st' =>
    1.48 +             (Toplevel.status tr Markup.finished;
    1.49 +              proof_status tr st';
    1.50 +              if int then () else async_state tr st'));
    1.51 +      in result end
    1.52 +  | Exn.Exn exn =>
    1.53 +     (Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE))
    1.54 +
    1.55 +end;
    1.56 +
    1.57 +
    1.58 +
    1.59 +
    1.60  (** editing **)
    1.61  
    1.62  (* edit *)
    1.63 @@ -214,7 +267,7 @@
    1.64            NONE => NONE
    1.65          | SOME st =>
    1.66              let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
    1.67 -            in Toplevel.run_command name exec_tr st end));
    1.68 +            in run_command name exec_tr st end));
    1.69      val state' = define_exec exec_id' exec' state;
    1.70    in (exec_id', (id, exec_id') :: updates, state') end;
    1.71