--- a/NEWS Fri Sep 10 14:37:57 2010 +0200
+++ b/NEWS Fri Sep 10 15:17:44 2010 +0200
@@ -254,6 +254,14 @@
theory loader state as before. Potential INCOMPATIBILITY, subtle
change in semantics.
+* Parallel and asynchronous execution requires special care concerning
+interrupts. Structure Exn provides some convenience functions that
+avoid working directly with raw Interrupt. User code must not absorb
+interrupts -- intermediate handling (for cleanup etc.) needs to be
+followed by re-raising of the original exception. Another common
+source of mistakes are "handle _" patterns, which make the meaning of
+the program subject to physical effects of the environment.
+
*** System ***
--- a/src/HOL/Import/proof_kernel.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Sep 10 15:17:44 2010 +0200
@@ -1299,10 +1299,13 @@
end
| NONE => (thy,NONE)
end
- end (* FIXME avoid handle _ *)
+ end
handle e =>
- (if_debug (fn () => writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
- (thy,NONE))
+ if Exn.is_interrupt e then reraise e
+ else
+ (if_debug (fn () =>
+ writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
+ (thy,NONE))
fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
let
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Sep 10 15:17:44 2010 +0200
@@ -73,12 +73,12 @@
fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
- handle (exn as Exn.Interrupt) => reraise exn
- | exn => (log_exn log tag id exn; ())
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; ())
fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
- handle (exn as Exn.Interrupt) => reraise exn
- | exn => (log_exn log tag id exn; d)
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; d)
fun register (init, run, done) thy =
let val id = length (Actions.get thy) + 1
--- a/src/HOL/Tools/meson.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Sep 10 15:17:44 2010 +0200
@@ -576,8 +576,7 @@
(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
The resulting clauses are HOL disjunctions.*)
-fun make_clauses_unsorted ths = fold_rev add_clauses ths []
-handle exn => error (ML_Compiler.exn_message exn) (*###*)
+fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
val make_clauses = sort_clauses o make_clauses_unsorted;
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
--- a/src/Pure/Concurrent/future.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/Concurrent/future.ML Fri Sep 10 15:17:44 2010 +0200
@@ -110,7 +110,7 @@
val _ = Single_Assignment.assign result res
handle exn as Fail _ =>
(case Single_Assignment.peek result of
- SOME (Exn.Exn Exn.Interrupt) => raise Exn.Interrupt
+ SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
| _ => reraise exn);
val ok =
(case the (Single_Assignment.peek result) of
@@ -184,7 +184,7 @@
Exn.capture (fn () =>
Multithreading.with_attributes Multithreading.private_interrupts
(fn _ => Position.setmp_thread_data pos e ())) ()
- else Exn.Exn Exn.Interrupt;
+ else Exn.interrupt_exn;
in assign_result group result res end;
in (result, job) end;
@@ -359,10 +359,12 @@
val _ = broadcast scheduler_event;
in continue end
- handle Exn.Interrupt =>
- (Multithreading.tracing 1 (fn () => "Interrupt");
- List.app cancel_later (Task_Queue.cancel_all (! queue));
- broadcast_work (); true);
+ handle exn =>
+ if Exn.is_interrupt exn then
+ (Multithreading.tracing 1 (fn () => "Interrupt");
+ List.app cancel_later (Task_Queue.cancel_all (! queue));
+ broadcast_work (); true)
+ else reraise exn;
fun scheduler_loop () =
while
@@ -415,11 +417,12 @@
fun get_result x =
(case peek x of
NONE => Exn.Exn (Fail "Unfinished future")
- | SOME (exn as Exn.Exn Exn.Interrupt) =>
- (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
- [] => exn
- | exns => Exn.Exn (Exn.EXCEPTIONS exns))
- | SOME res => res);
+ | SOME res =>
+ if Exn.is_interrupt_exn res then
+ (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
+ [] => res
+ | exns => Exn.Exn (Exn.EXCEPTIONS exns))
+ else res);
fun join_next deps = (*requires SYNCHRONIZED*)
if null deps then NONE
@@ -486,7 +489,11 @@
fun promise_group group : 'a future =
let
val result = Single_Assignment.var "promise" : 'a result;
- fun abort () = assign_result group result (Exn.Exn Exn.Interrupt) handle Fail _ => true;
+ fun abort () = assign_result group result Exn.interrupt_exn
+ handle Fail _ => true
+ | exn =>
+ if Exn.is_interrupt exn then raise Fail "Concurrent attempt to fulfill promise"
+ else reraise exn;
val task = SYNCHRONIZED "enqueue_passive" (fn () =>
Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
in Future {promised = true, task = task, group = group, result = result} end;
@@ -494,11 +501,20 @@
fun promise () = promise_group (worker_subgroup ());
fun fulfill_result (Future {promised, task, group, result}) res =
- let
- val _ = promised orelse raise Fail "Not a promised future";
- fun job ok = assign_result group result (if ok then res else Exn.Exn Exn.Interrupt);
- val _ = execute (task, group, [job]);
- in () end;
+ if not promised then raise Fail "Not a promised future"
+ else
+ let
+ fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn);
+ val _ =
+ Multithreading.with_attributes Multithreading.no_interrupts (fn _ =>
+ let
+ val still_passive =
+ SYNCHRONIZED "fulfill_result" (fn () =>
+ Unsynchronized.change_result queue
+ (Task_Queue.dequeue_passive (Thread.self ()) task));
+ in if still_passive then execute (task, group, [job]) else () end);
+ val _ = Single_Assignment.await result;
+ in () end;
fun fulfill x res = fulfill_result x (Exn.Result res);
--- a/src/Pure/Concurrent/lazy.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/Concurrent/lazy.ML Fri Sep 10 15:17:44 2010 +0200
@@ -60,9 +60,9 @@
(*semantic race: some other threads might see the same
Interrupt, until there is a fresh start*)
val _ =
- (case res of
- Exn.Exn Exn.Interrupt => Synchronized.change var (fn _ => Expr e)
- | _ => ());
+ if Exn.is_interrupt_exn res then
+ Synchronized.change var (fn _ => Expr e)
+ else ();
in res end
| NONE => restore_interrupts (fn () => Future.join_result x) ())
end) ());
--- a/src/Pure/Concurrent/lazy_sequential.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML Fri Sep 10 15:17:44 2010 +0200
@@ -34,10 +34,7 @@
(case ! r of
Expr e => Exn.capture e ()
| Result res => res);
- val _ =
- (case result of
- Exn.Exn Exn.Interrupt => ()
- | _ => r := Result result);
+ val _ = if Exn.is_interrupt_exn result then () else r := Result result;
in result end;
fun force r = Exn.release (force_result r);
--- a/src/Pure/Concurrent/simple_thread.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML Fri Sep 10 15:17:44 2010 +0200
@@ -19,7 +19,9 @@
if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;
fun fork interrupts body =
- Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
+ Thread.fork (fn () =>
+ exception_trace (fn () =>
+ body () handle exn => if Exn.is_interrupt exn then () else reraise exn),
attributes interrupts);
fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
--- a/src/Pure/Concurrent/task_queue.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Fri Sep 10 15:17:44 2010 +0200
@@ -27,6 +27,7 @@
val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
val extend: task -> (bool -> bool) -> queue -> queue option
+ val dequeue_passive: Thread.thread -> task -> queue -> bool * queue
val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
val depend: task -> task list -> queue -> queue
val dequeue_towards: Thread.thread -> task list -> queue ->
@@ -80,9 +81,8 @@
fun cancel_group (Group {status, ...}) exn =
Synchronized.change status
(fn exns =>
- (case exn of
- Exn.Interrupt => if null exns then [exn] else exns
- | _ => exn :: exns));
+ if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
+ else exns);
fun is_canceled (Group {parent, status, ...}) =
not (null (Synchronized.value status)) orelse
@@ -217,12 +217,19 @@
(* dequeue *)
+fun dequeue_passive thread task (queue as Queue {groups, jobs}) =
+ (case try (get_job jobs) task of
+ SOME (Passive _) =>
+ let val jobs' = set_job task (Running thread) jobs
+ in (true, make_queue groups jobs') end
+ | _ => (false, queue));
+
fun dequeue thread (queue as Queue {groups, jobs}) =
(case Task_Graph.get_first (uncurry ready_job) jobs of
- NONE => (NONE, queue)
- | SOME (result as (task, _, _)) =>
+ SOME (result as (task, _, _)) =>
let val jobs' = set_job task (Running thread) jobs
- in (SOME result, make_queue groups jobs') end);
+ in (SOME result, make_queue groups jobs') end
+ | NONE => (NONE, queue));
(* dequeue_towards -- adhoc dependencies *)
--- a/src/Pure/General/basics.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/General/basics.ML Fri Sep 10 15:17:44 2010 +0200
@@ -94,7 +94,7 @@
(* partiality *)
fun try f x = SOME (f x)
- handle (exn as Exn.Interrupt) => reraise exn | _ => NONE;
+ handle exn => if Exn.is_interrupt exn then reraise exn else NONE;
fun can f x = is_some (try f x);
--- a/src/Pure/General/exn.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/General/exn.ML Fri Sep 10 15:17:44 2010 +0200
@@ -12,6 +12,10 @@
val capture: ('a -> 'b) -> 'a -> 'b result
val release: 'a result -> 'a
exception Interrupt
+ val interrupt: unit -> 'a
+ val is_interrupt: exn -> bool
+ val interrupt_exn: 'a result
+ val is_interrupt_exn: 'a result -> bool
exception EXCEPTIONS of exn list
val flatten: exn -> exn list
val flatten_list: exn list -> exn list
@@ -40,14 +44,28 @@
| release (Exn e) = reraise e;
-(* interrupt and nested exceptions *)
+(* interrupts *)
exception Interrupt = Interrupt;
+
+fun interrupt () = raise Interrupt;
+
+fun is_interrupt Interrupt = true
+ | is_interrupt (IO.Io {cause = Interrupt, ...}) = true
+ | is_interrupt _ = false;
+
+val interrupt_exn = Exn Interrupt;
+
+fun is_interrupt_exn (Exn exn) = is_interrupt exn
+ | is_interrupt_exn _ = false;
+
+
+(* nested exceptions *)
+
exception EXCEPTIONS of exn list;
-fun flatten Interrupt = []
- | flatten (EXCEPTIONS exns) = flatten_list exns
- | flatten exn = [exn]
+fun flatten (EXCEPTIONS exns) = flatten_list exns
+ | flatten exn = if is_interrupt exn then [] else [exn]
and flatten_list exns = List.concat (map flatten exns);
fun release_all results =
--- a/src/Pure/Isar/proof.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/Isar/proof.ML Fri Sep 10 15:17:44 2010 +0200
@@ -990,8 +990,9 @@
(case test_proof goal_state of
Exn.Result (SOME _) => goal_state
| Exn.Result NONE => error (fail_msg (context_of goal_state))
- | Exn.Exn Exn.Interrupt => raise Exn.Interrupt
- | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
+ | Exn.Exn exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
end;
in
--- a/src/Pure/Isar/runtime.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/Isar/runtime.ML Fri Sep 10 15:17:44 2010 +0200
@@ -54,30 +54,38 @@
val detailed = ! Output.debugging;
- fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
- | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
- | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
- map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
- | exn_msgs _ TERMINATE = ["Exit"]
- | exn_msgs _ Exn.Interrupt = []
- | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
- | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
- | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
- | exn_msgs _ (ERROR msg) = [msg]
- | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
- | exn_msgs _ (exn as THEORY (msg, thys)) =
- [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
- | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
- (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
- | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
- (if detailed then
- if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
- else []))]
- | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
- (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
- | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
- (if detailed then if_context ctxt Display.string_of_thm thms else []))]
- | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
+ fun exn_msgs context exn =
+ if Exn.is_interrupt exn then []
+ else
+ (case exn of
+ Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
+ | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
+ | EXCURSION_FAIL (exn, loc) =>
+ map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs context exn)
+ | TERMINATE => ["Exit"]
+ | TimeLimit.TimeOut => ["Timeout"]
+ | TOPLEVEL_ERROR => ["Error"]
+ | SYS_ERROR msg => ["## SYSTEM ERROR ##\n" ^ msg]
+ | ERROR msg => [msg]
+ | Fail msg => [raised exn "Fail" [msg]]
+ | THEORY (msg, thys) =>
+ [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
+ | Syntax.AST (msg, asts) =>
+ [raised exn "AST" (msg ::
+ (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
+ | TYPE (msg, Ts, ts) =>
+ [raised exn "TYPE" (msg ::
+ (if detailed then
+ if_context context Syntax.string_of_typ Ts @
+ if_context context Syntax.string_of_term ts
+ else []))]
+ | TERM (msg, ts) =>
+ [raised exn "TERM" (msg ::
+ (if detailed then if_context context Syntax.string_of_term ts else []))]
+ | THM (msg, i, thms) =>
+ [raised exn ("THM " ^ string_of_int i) (msg ::
+ (if detailed then if_context context Display.string_of_thm thms else []))]
+ | _ => [raised exn (General.exnMessage exn) []]);
in exn_msgs NONE e end;
fun exn_message exn_position exn =
@@ -102,9 +110,14 @@
|> debugging
|> Future.interruptible_task;
-fun toplevel_error output_exn f x =
- let val ctxt = Option.map Context.proof_of (Context.thread_data ())
- in f x handle exn => (output_exn (exn_context ctxt exn); raise TOPLEVEL_ERROR) end;
+fun toplevel_error output_exn f x = f x
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else
+ let
+ val ctxt = Option.map Context.proof_of (Context.thread_data ());
+ val _ = output_exn (exn_context ctxt exn);
+ in raise TOPLEVEL_ERROR end;
end;
--- a/src/Pure/Isar/toplevel.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Fri Sep 10 15:17:44 2010 +0200
@@ -30,7 +30,6 @@
val timing: bool Unsynchronized.ref
val profiling: int Unsynchronized.ref
val skip_proofs: bool Unsynchronized.ref
- exception TOPLEVEL_ERROR
val program: (unit -> 'a) -> 'a
val thread: bool -> (unit -> unit) -> Thread.thread
type transition
@@ -222,8 +221,6 @@
val profiling = Unsynchronized.ref 0;
val skip_proofs = Unsynchronized.ref false;
-exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
-
fun program body =
(body
|> Runtime.controlled_execution
@@ -231,7 +228,7 @@
fun thread interrupts body =
Thread.fork
- (((fn () => body () handle Exn.Interrupt => ())
+ (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
|> Runtime.debugging
|> Runtime.toplevel_error
(fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Fri Sep 10 15:17:44 2010 +0200
@@ -37,8 +37,10 @@
(while not (List.null (! in_buffer)) do
PolyML.compiler (get, parameters) ())
handle exn =>
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); reraise exn);
+ if Exn.is_interrupt exn then reraise exn
+ else
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ error (output ()); reraise exn);
in if verbose then print (output ()) else () end;
fun use_file context verbose name =
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Fri Sep 10 15:17:44 2010 +0200
@@ -41,8 +41,10 @@
(while not (List.null (! in_buffer)) do
PolyML.compiler (get, parameters) ())
handle exn =>
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); reraise exn);
+ if Exn.is_interrupt exn then reraise exn
+ else
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ error (output ()); reraise exn);
in if verbose then print (output ()) else () end;
fun use_file context verbose name =
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Fri Sep 10 15:17:44 2010 +0200
@@ -148,7 +148,7 @@
(OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
val result = Exn.capture (restore_attributes f) x;
- val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false);
+ val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
val _ = Thread.interrupt watchdog handle Thread _ => ();
in if was_timeout then raise TimeOut else Exn.release result end) ();
@@ -209,7 +209,7 @@
let val res =
sync_wait (SOME orig_atts)
(SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
- in case res of Exn.Exn Exn.Interrupt => kill 10 | _ => () end;
+ in if Exn.is_interrupt_exn res then kill 10 else () end;
(*cleanup*)
val output = read_file output_name handle IO.Io _ => "";
@@ -217,7 +217,7 @@
val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
val _ = Thread.interrupt system_thread handle Thread _ => ();
- val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
+ val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
in (output, rc) end);
--- a/src/Pure/ML-Systems/smlnj.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Fri Sep 10 15:17:44 2010 +0200
@@ -142,7 +142,7 @@
fun interruptible (f: 'a -> 'b) x =
let
- val result = ref (Exn.Exn Interrupt: 'b Exn.result);
+ val result = ref (Exn.interrupt_exn: 'b Exn.result);
val old_handler = Signals.inqHandler Signals.sigINT;
in
SMLofNJ.Cont.callcc (fn cont =>
@@ -159,16 +159,6 @@
end;
-(* basis library fixes *)
-
-structure TextIO =
-struct
- open TextIO;
- fun inputLine is = TextIO.inputLine is
- handle IO.Io _ => raise Interrupt;
-end;
-
-
(** OS related **)
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Sep 10 15:17:44 2010 +0200
@@ -25,6 +25,10 @@
loc_props
end |> Position.of_properties;
+fun offset_position_of loc =
+ let val pos = position_of loc
+ in if is_some (Position.offset_of pos) then pos else Position.none end;
+
fun exn_position exn =
(case PolyML.exceptionLocation exn of
NONE => Position.none
@@ -44,12 +48,12 @@
| _ => Position.report_text);
fun report_decl markup loc decl =
- report_text Markup.ML_ref (position_of loc)
+ report_text Markup.ML_ref (offset_position_of loc)
(Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
fun report loc (PolyML.PTtype types) =
PolyML.NameSpace.displayTypeExpression (types, depth, space)
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> report_text Markup.ML_typing (position_of loc)
+ |> report_text Markup.ML_typing (offset_position_of loc)
| report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
| report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
| report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
@@ -67,7 +71,7 @@
fun eval verbose pos toks =
let
val _ = Secure.secure_mltext ();
- val {name_space = space, print, error = err, ...} = ML_Env.local_context;
+ val space = ML_Env.name_space;
(* input *)
@@ -99,15 +103,29 @@
SOME c));
- (* output *)
+ (* output channels *)
+
+ val writeln_buffer = Unsynchronized.ref Buffer.empty;
+ fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
+ fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
+
+ val warnings = Unsynchronized.ref ([]: string list);
+ fun warn msg = Unsynchronized.change warnings (cons msg);
+ fun output_warnings () = List.app warning (rev (! warnings));
- val output_buffer = Unsynchronized.ref Buffer.empty;
- fun output () = Buffer.content (! output_buffer);
- fun put s = Unsynchronized.change output_buffer (Buffer.add s);
+ val error_buffer = Unsynchronized.ref Buffer.empty;
+ fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
+ fun flush_error () = writeln (Buffer.content (! error_buffer));
+ fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
- fun put_message {message, hard, location, context = _} =
- (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");
- put (Pretty.string_of (Pretty.from_ML (pretty_ml message)) ^ "\n"));
+ fun message {message = msg, hard, location = loc, context = _} =
+ let
+ val txt =
+ Markup.markup Markup.location
+ ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
+ Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
+ Markup.markup (Position.report_markup (offset_position_of loc)) "";
+ in if hard then err txt else warn txt end;
(* results *)
@@ -118,7 +136,7 @@
let
fun display disp x =
if depth > 0 then
- (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
+ (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
else ();
fun apply_fix (a, b) =
@@ -142,25 +160,27 @@
List.app apply_val values
end;
+ exception STATIC_ERRORS of unit;
+
fun result_fun (phase1, phase2) () =
((case phase1 of
NONE => ()
| SOME parse_tree => report_parse_tree depth space parse_tree);
(case phase2 of
- NONE => err "Static Errors"
+ NONE => raise STATIC_ERRORS ()
| SOME code =>
apply_result
((code
|> Runtime.debugging
- |> Runtime.toplevel_error (Output.error_msg o exn_message)) ())));
+ |> Runtime.toplevel_error (err o exn_message)) ())));
(* compiler invocation *)
val parameters =
- [PolyML.Compiler.CPOutStream put,
+ [PolyML.Compiler.CPOutStream write,
PolyML.Compiler.CPNameSpace space,
- PolyML.Compiler.CPErrorMessageProc put_message,
+ PolyML.Compiler.CPErrorMessageProc message,
PolyML.Compiler.CPLineNo (fn () => ! line),
PolyML.Compiler.CPLineOffset get_offset,
PolyML.Compiler.CPFileName location_props,
@@ -170,9 +190,21 @@
(while not (List.null (! input_buffer)) do
PolyML.compiler (get, parameters) ())
handle exn =>
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- err (output ()); reraise exn);
- in if verbose then print (output ()) else () end;
+ if Exn.is_interrupt exn then reraise exn
+ else
+ let
+ val exn_msg =
+ (case exn of
+ STATIC_ERRORS () => ""
+ | Runtime.TOPLEVEL_ERROR => ""
+ | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
+ val _ = output_warnings ();
+ val _ = output_writeln ();
+ in raise_error exn_msg end;
+ in
+ if verbose then (output_warnings (); flush_error (); output_writeln ())
+ else ()
+ end;
end;
--- a/src/Pure/PIDE/document.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/PIDE/document.ML Fri Sep 10 15:17:44 2010 +0200
@@ -225,7 +225,7 @@
SOME (st', NONE) => ([], SOME st')
| SOME (_, SOME exn_info) =>
(case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
- [] => raise Exn.Interrupt
+ [] => Exn.interrupt ()
| errs => (errs, NONE))
| NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
val _ = List.app (Toplevel.error_msg tr) errs;
@@ -238,7 +238,10 @@
if int then () else async_state tr st'));
in result end
| Exn.Exn exn =>
- (Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE))
+ if Exn.is_interrupt exn then reraise exn
+ else
+ (Toplevel.error_msg tr (ML_Compiler.exn_message exn);
+ Toplevel.status tr Markup.failed; NONE));
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Sep 10 15:17:44 2010 +0200
@@ -983,17 +983,18 @@
end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *)
and handler (e,srco) =
- case (e,srco) of
- (XML_PARSE,SOME src) =>
- panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
- | (Exn.Interrupt,SOME src) =>
- (Output.error_msg "Interrupt during PGIP processing"; loop true src)
- | (Toplevel.UNDEF,SOME src) =>
- (Output.error_msg "No working context defined"; loop true src)
- | (e,SOME src) =>
- (Output.error_msg (ML_Compiler.exn_message e); loop true src)
- | (PGIP_QUIT,_) => ()
- | (_,NONE) => ()
+ if Exn.is_interrupt e andalso is_some srco then
+ (Output.error_msg "Interrupt during PGIP processing"; loop true (the srco))
+ else
+ case (e,srco) of
+ (XML_PARSE,SOME src) =>
+ panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
+ | (Toplevel.UNDEF,SOME src) =>
+ (Output.error_msg "No working context defined"; loop true src)
+ | (e,SOME src) =>
+ (Output.error_msg (ML_Compiler.exn_message e); loop true src)
+ | (PGIP_QUIT,_) => ()
+ | (_,NONE) => ()
in
(* TODO: add socket interface *)
--- a/src/Pure/System/isabelle_process.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Fri Sep 10 15:17:44 2010 +0200
@@ -117,7 +117,7 @@
end;
-(* protocol loop *)
+(* protocol loop -- uninterruptible *)
val crashes = Unsynchronized.ref ([]: exn list);
--- a/src/Pure/System/isar.ML Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Pure/System/isar.ML Fri Sep 10 15:17:44 2010 +0200
@@ -111,7 +111,7 @@
| op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
-(* toplevel loop *)
+(* toplevel loop -- uninterruptible *)
val crashes = Unsynchronized.ref ([]: exn list);
--- a/src/Tools/jEdit/README Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Tools/jEdit/README Fri Sep 10 15:17:44 2010 +0200
@@ -26,9 +26,6 @@
previous commands (proof end on proof head), or markup produced by
loading external files.
- * Some performance bottlenecks for massive amount of markup,
- e.g. when processing large ML sections.
-
* General lack of various conveniences known from Proof General.
Despite these shortcomings, Isabelle/jEdit already demonstrates that
--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Fri Sep 10 15:17:44 2010 +0200
@@ -8,6 +8,8 @@
.error { background-color: #FFC1C1; }
.debug { background-color: #FFE4E1; }
+.location { display: none; }
+
.hilite { background-color: #FFFACD; }
.keyword { font-weight: bold; color: #009966; }
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Fri Sep 10 15:17:44 2010 +0200
@@ -11,7 +11,6 @@
import java.awt.Color
-import org.gjt.sp.jedit.GUIUtilities
import org.gjt.sp.jedit.syntax.Token
@@ -31,8 +30,8 @@
{
def >= (that: Icon): Boolean = this.priority >= that.priority
}
- val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
- val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
+ val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png"))
+ val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png"))
/* command status */
@@ -100,7 +99,7 @@
val tooltip: Markup_Tree.Select[String] =
{
case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
- Pretty.string_of(List(Pretty.block(body)), margin = 40)
+ Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), margin = 40)
case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
--- a/src/Tools/jEdit/src/jedit/plugin.scala Fri Sep 10 14:37:57 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Fri Sep 10 15:17:44 2010 +0200
@@ -15,12 +15,15 @@
import scala.collection.mutable
-import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
+import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
+ Buffer, EditPane, ServiceManager, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.util.Log
+
object Isabelle
{
@@ -106,6 +109,17 @@
}
+ /* icons */
+
+ def load_icon(name: String): javax.swing.Icon =
+ {
+ val icon = GUIUtilities.loadIcon(name)
+ if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
+ Log.log(Log.ERROR, icon, "Bad icon: " + name);
+ icon
+ }
+
+
/* settings */
def default_logic(): String =