src/Pure/PIDE/document.ML
changeset 40390 5bc4336d9768
parent 39391 f1d6ede54862
child 40391 b0dafbfc05b7
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Nov 06 15:34:11 2010 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Nov 06 16:03:49 2010 +0100
     1.3 @@ -210,6 +210,15 @@
     1.4              (fn () => Toplevel.print_state false st) ()))
     1.5    else ();
     1.6  
     1.7 +fun run int tr st =
     1.8 +  (case Toplevel.transition int tr st of
     1.9 +    SOME (st', NONE) => ([], SOME st')
    1.10 +  | SOME (_, SOME exn_info) =>
    1.11 +      (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
    1.12 +        [] => Exn.interrupt ()
    1.13 +      | errs => (errs, NONE))
    1.14 +  | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
    1.15 +
    1.16  in
    1.17  
    1.18  fun run_command thy_name tr st =
    1.19 @@ -220,14 +229,7 @@
    1.20      Exn.Result () =>
    1.21        let
    1.22          val int = is_some (Toplevel.init_of tr);
    1.23 -        val (errs, result) =
    1.24 -          (case Toplevel.transition int tr st of
    1.25 -            SOME (st', NONE) => ([], SOME st')
    1.26 -          | SOME (_, SOME exn_info) =>
    1.27 -              (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
    1.28 -                [] => Exn.interrupt ()
    1.29 -              | errs => (errs, NONE))
    1.30 -          | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
    1.31 +        val (errs, result) = run int tr st;
    1.32          val _ = List.app (Toplevel.error_msg tr) errs;
    1.33          val _ =
    1.34            (case result of