added TOPLEVEL_ERROR (simplified version from output.ML);
authorwenzelm
Sun Jul 29 16:00:04 2007 +0200 (2007-07-29)
changeset 24055f7483532537b
parent 24054 0eacec17e8e7
child 24056 e134e757fc64
added TOPLEVEL_ERROR (simplified version from output.ML);
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Jul 29 16:00:03 2007 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Jul 29 16:00:04 2007 +0200
     1.3 @@ -38,6 +38,7 @@
     1.4    val skip_proofs: bool ref
     1.5    exception TERMINATE
     1.6    exception RESTART
     1.7 +  exception TOPLEVEL_ERROR
     1.8    val exn_message: exn -> string
     1.9    val program: (unit -> 'a) -> 'a
    1.10    type transition
    1.11 @@ -237,6 +238,7 @@
    1.12  exception RESTART;
    1.13  exception EXCURSION_FAIL of exn * string;
    1.14  exception FAILURE of state * exn;
    1.15 +exception TOPLEVEL_ERROR;
    1.16  
    1.17  
    1.18  (* print exceptions *)
    1.19 @@ -254,7 +256,7 @@
    1.20  fun exn_msg _ TERMINATE = "Exit."
    1.21    | exn_msg _ RESTART = "Restart."
    1.22    | exn_msg _ Interrupt = "Interrupt."
    1.23 -  | exn_msg _ Output.TOPLEVEL_ERROR = "Error."
    1.24 +  | exn_msg _ TOPLEVEL_ERROR = "Error."
    1.25    | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
    1.26    | exn_msg _ (ERROR msg) = msg
    1.27    | exn_msg detailed (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg detailed) exns)
    1.28 @@ -303,16 +305,20 @@
    1.29    let val y = ref x
    1.30    in raise_interrupt (fn () => y := f x) (); ! y end;
    1.31  
    1.32 +fun toplevel_error f x = f x
    1.33 +  handle exn => (Output.error_msg (exn_message exn); raise TOPLEVEL_ERROR);
    1.34 +
    1.35  in
    1.36  
    1.37  fun controlled_execution f =
    1.38    f
    1.39    |> debugging
    1.40 -  |> interruptible
    1.41 -  |> setmp Output.do_toplevel_errors false;
    1.42 +  |> interruptible;
    1.43  
    1.44  fun program f =
    1.45 -  Output.ML_errors (fn () => debugging f () handle exn => error (exn_message exn)) ();
    1.46 + (f
    1.47 +  |> debugging
    1.48 +  |> toplevel_error) ();
    1.49  
    1.50  end;
    1.51