merged
authorwenzelm
Fri Sep 10 15:17:44 2010 +0200 (2010-09-10)
changeset 39277f263522ab226
parent 39276 2ad95934521f
parent 39245 cc155a9bf3a2
child 39278 cc7abfe6d5e7
merged
NEWS
src/HOL/Tools/meson.ML
     1.1 --- a/NEWS	Fri Sep 10 14:37:57 2010 +0200
     1.2 +++ b/NEWS	Fri Sep 10 15:17:44 2010 +0200
     1.3 @@ -254,6 +254,14 @@
     1.4  theory loader state as before.  Potential INCOMPATIBILITY, subtle
     1.5  change in semantics.
     1.6  
     1.7 +* Parallel and asynchronous execution requires special care concerning
     1.8 +interrupts.  Structure Exn provides some convenience functions that
     1.9 +avoid working directly with raw Interrupt.  User code must not absorb
    1.10 +interrupts -- intermediate handling (for cleanup etc.) needs to be
    1.11 +followed by re-raising of the original exception.  Another common
    1.12 +source of mistakes are "handle _" patterns, which make the meaning of
    1.13 +the program subject to physical effects of the environment.
    1.14 +
    1.15  
    1.16  *** System ***
    1.17  
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Sep 10 14:37:57 2010 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Sep 10 15:17:44 2010 +0200
     2.3 @@ -1299,10 +1299,13 @@
     2.4                      end
     2.5                    | NONE => (thy,NONE)
     2.6              end
     2.7 -    end  (* FIXME avoid handle _ *)
     2.8 +    end
     2.9      handle e =>
    2.10 -      (if_debug (fn () => writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
    2.11 -        (thy,NONE))
    2.12 +      if Exn.is_interrupt e then reraise e
    2.13 +      else
    2.14 +        (if_debug (fn () =>
    2.15 +            writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
    2.16 +          (thy,NONE))
    2.17  
    2.18  fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
    2.19    let
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Sep 10 14:37:57 2010 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Sep 10 15:17:44 2010 +0200
     3.3 @@ -73,12 +73,12 @@
     3.4  fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
     3.5  
     3.6  fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
     3.7 -  handle (exn as Exn.Interrupt) => reraise exn
     3.8 -       | exn => (log_exn log tag id exn; ())
     3.9 +  handle exn =>
    3.10 +    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; ())
    3.11  
    3.12  fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
    3.13 -  handle (exn as Exn.Interrupt) => reraise exn
    3.14 -       | exn => (log_exn log tag id exn; d)
    3.15 +  handle exn =>
    3.16 +    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; d)
    3.17  
    3.18  fun register (init, run, done) thy =
    3.19    let val id = length (Actions.get thy) + 1
     4.1 --- a/src/HOL/Tools/meson.ML	Fri Sep 10 14:37:57 2010 +0200
     4.2 +++ b/src/HOL/Tools/meson.ML	Fri Sep 10 15:17:44 2010 +0200
     4.3 @@ -576,8 +576,7 @@
     4.4  
     4.5  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
     4.6    The resulting clauses are HOL disjunctions.*)
     4.7 -fun make_clauses_unsorted ths = fold_rev add_clauses ths []
     4.8 -handle exn => error (ML_Compiler.exn_message exn) (*###*)
     4.9 +fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
    4.10  val make_clauses = sort_clauses o make_clauses_unsorted;
    4.11  
    4.12  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
     5.1 --- a/src/Pure/Concurrent/future.ML	Fri Sep 10 14:37:57 2010 +0200
     5.2 +++ b/src/Pure/Concurrent/future.ML	Fri Sep 10 15:17:44 2010 +0200
     5.3 @@ -110,7 +110,7 @@
     5.4      val _ = Single_Assignment.assign result res
     5.5        handle exn as Fail _ =>
     5.6          (case Single_Assignment.peek result of
     5.7 -          SOME (Exn.Exn Exn.Interrupt) => raise Exn.Interrupt
     5.8 +          SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
     5.9          | _ => reraise exn);
    5.10      val ok =
    5.11        (case the (Single_Assignment.peek result) of
    5.12 @@ -184,7 +184,7 @@
    5.13              Exn.capture (fn () =>
    5.14                Multithreading.with_attributes Multithreading.private_interrupts
    5.15                  (fn _ => Position.setmp_thread_data pos e ())) ()
    5.16 -          else Exn.Exn Exn.Interrupt;
    5.17 +          else Exn.interrupt_exn;
    5.18        in assign_result group result res end;
    5.19    in (result, job) end;
    5.20  
    5.21 @@ -359,10 +359,12 @@
    5.22  
    5.23      val _ = broadcast scheduler_event;
    5.24    in continue end
    5.25 -  handle Exn.Interrupt =>
    5.26 -   (Multithreading.tracing 1 (fn () => "Interrupt");
    5.27 -    List.app cancel_later (Task_Queue.cancel_all (! queue));
    5.28 -    broadcast_work (); true);
    5.29 +  handle exn =>
    5.30 +    if Exn.is_interrupt exn then
    5.31 +     (Multithreading.tracing 1 (fn () => "Interrupt");
    5.32 +      List.app cancel_later (Task_Queue.cancel_all (! queue));
    5.33 +      broadcast_work (); true)
    5.34 +    else reraise exn;
    5.35  
    5.36  fun scheduler_loop () =
    5.37    while
    5.38 @@ -415,11 +417,12 @@
    5.39  fun get_result x =
    5.40    (case peek x of
    5.41      NONE => Exn.Exn (Fail "Unfinished future")
    5.42 -  | SOME (exn as Exn.Exn Exn.Interrupt) =>
    5.43 -      (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
    5.44 -        [] => exn
    5.45 -      | exns => Exn.Exn (Exn.EXCEPTIONS exns))
    5.46 -  | SOME res => res);
    5.47 +  | SOME res =>
    5.48 +      if Exn.is_interrupt_exn res then
    5.49 +        (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
    5.50 +          [] => res
    5.51 +        | exns => Exn.Exn (Exn.EXCEPTIONS exns))
    5.52 +      else res);
    5.53  
    5.54  fun join_next deps = (*requires SYNCHRONIZED*)
    5.55    if null deps then NONE
    5.56 @@ -486,7 +489,11 @@
    5.57  fun promise_group group : 'a future =
    5.58    let
    5.59      val result = Single_Assignment.var "promise" : 'a result;
    5.60 -    fun abort () = assign_result group result (Exn.Exn Exn.Interrupt) handle Fail _ => true;
    5.61 +    fun abort () = assign_result group result Exn.interrupt_exn
    5.62 +      handle Fail _ => true
    5.63 +        | exn =>
    5.64 +            if Exn.is_interrupt exn then raise Fail "Concurrent attempt to fulfill promise"
    5.65 +            else reraise exn;
    5.66      val task = SYNCHRONIZED "enqueue_passive" (fn () =>
    5.67        Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
    5.68    in Future {promised = true, task = task, group = group, result = result} end;
    5.69 @@ -494,11 +501,20 @@
    5.70  fun promise () = promise_group (worker_subgroup ());
    5.71  
    5.72  fun fulfill_result (Future {promised, task, group, result}) res =
    5.73 -  let
    5.74 -    val _ = promised orelse raise Fail "Not a promised future";
    5.75 -    fun job ok = assign_result group result (if ok then res else Exn.Exn Exn.Interrupt);
    5.76 -    val _ = execute (task, group, [job]);
    5.77 -  in () end;
    5.78 +  if not promised then raise Fail "Not a promised future"
    5.79 +  else
    5.80 +    let
    5.81 +      fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn);
    5.82 +      val _ =
    5.83 +        Multithreading.with_attributes Multithreading.no_interrupts (fn _ =>
    5.84 +          let
    5.85 +            val still_passive =
    5.86 +              SYNCHRONIZED "fulfill_result" (fn () =>
    5.87 +                Unsynchronized.change_result queue
    5.88 +                  (Task_Queue.dequeue_passive (Thread.self ()) task));
    5.89 +          in if still_passive then execute (task, group, [job]) else () end);
    5.90 +      val _ = Single_Assignment.await result;
    5.91 +    in () end;
    5.92  
    5.93  fun fulfill x res = fulfill_result x (Exn.Result res);
    5.94  
     6.1 --- a/src/Pure/Concurrent/lazy.ML	Fri Sep 10 14:37:57 2010 +0200
     6.2 +++ b/src/Pure/Concurrent/lazy.ML	Fri Sep 10 15:17:44 2010 +0200
     6.3 @@ -60,9 +60,9 @@
     6.4                  (*semantic race: some other threads might see the same
     6.5                    Interrupt, until there is a fresh start*)
     6.6                  val _ =
     6.7 -                  (case res of
     6.8 -                    Exn.Exn Exn.Interrupt => Synchronized.change var (fn _ => Expr e)
     6.9 -                  | _ => ());
    6.10 +                  if Exn.is_interrupt_exn res then
    6.11 +                    Synchronized.change var (fn _ => Expr e)
    6.12 +                  else ();
    6.13                in res end
    6.14            | NONE => restore_interrupts (fn () => Future.join_result x) ())
    6.15          end) ());
     7.1 --- a/src/Pure/Concurrent/lazy_sequential.ML	Fri Sep 10 14:37:57 2010 +0200
     7.2 +++ b/src/Pure/Concurrent/lazy_sequential.ML	Fri Sep 10 15:17:44 2010 +0200
     7.3 @@ -34,10 +34,7 @@
     7.4        (case ! r of
     7.5          Expr e => Exn.capture e ()
     7.6        | Result res => res);
     7.7 -    val _ =
     7.8 -      (case result of
     7.9 -        Exn.Exn Exn.Interrupt => ()
    7.10 -      | _ => r := Result result);
    7.11 +    val _ = if Exn.is_interrupt_exn result then () else r := Result result;
    7.12    in result end;
    7.13  
    7.14  fun force r = Exn.release (force_result r);
     8.1 --- a/src/Pure/Concurrent/simple_thread.ML	Fri Sep 10 14:37:57 2010 +0200
     8.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Fri Sep 10 15:17:44 2010 +0200
     8.3 @@ -19,7 +19,9 @@
     8.4    if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;
     8.5  
     8.6  fun fork interrupts body =
     8.7 -  Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
     8.8 +  Thread.fork (fn () =>
     8.9 +    exception_trace (fn () =>
    8.10 +      body () handle exn => if Exn.is_interrupt exn then () else reraise exn),
    8.11      attributes interrupts);
    8.12  
    8.13  fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
     9.1 --- a/src/Pure/Concurrent/task_queue.ML	Fri Sep 10 14:37:57 2010 +0200
     9.2 +++ b/src/Pure/Concurrent/task_queue.ML	Fri Sep 10 15:17:44 2010 +0200
     9.3 @@ -27,6 +27,7 @@
     9.4    val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
     9.5    val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
     9.6    val extend: task -> (bool -> bool) -> queue -> queue option
     9.7 +  val dequeue_passive: Thread.thread -> task -> queue -> bool * queue
     9.8    val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
     9.9    val depend: task -> task list -> queue -> queue
    9.10    val dequeue_towards: Thread.thread -> task list -> queue ->
    9.11 @@ -80,9 +81,8 @@
    9.12  fun cancel_group (Group {status, ...}) exn =
    9.13    Synchronized.change status
    9.14      (fn exns =>
    9.15 -      (case exn of
    9.16 -        Exn.Interrupt => if null exns then [exn] else exns
    9.17 -      | _ => exn :: exns));
    9.18 +      if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
    9.19 +      else exns);
    9.20  
    9.21  fun is_canceled (Group {parent, status, ...}) =
    9.22    not (null (Synchronized.value status)) orelse
    9.23 @@ -217,12 +217,19 @@
    9.24  
    9.25  (* dequeue *)
    9.26  
    9.27 +fun dequeue_passive thread task (queue as Queue {groups, jobs}) =
    9.28 +  (case try (get_job jobs) task of
    9.29 +    SOME (Passive _) =>
    9.30 +      let val jobs' = set_job task (Running thread) jobs
    9.31 +      in (true, make_queue groups jobs') end
    9.32 +  | _ => (false, queue));
    9.33 +
    9.34  fun dequeue thread (queue as Queue {groups, jobs}) =
    9.35    (case Task_Graph.get_first (uncurry ready_job) jobs of
    9.36 -    NONE => (NONE, queue)
    9.37 -  | SOME (result as (task, _, _)) =>
    9.38 +    SOME (result as (task, _, _)) =>
    9.39        let val jobs' = set_job task (Running thread) jobs
    9.40 -      in (SOME result, make_queue groups jobs') end);
    9.41 +      in (SOME result, make_queue groups jobs') end
    9.42 +  | NONE => (NONE, queue));
    9.43  
    9.44  
    9.45  (* dequeue_towards -- adhoc dependencies *)
    10.1 --- a/src/Pure/General/basics.ML	Fri Sep 10 14:37:57 2010 +0200
    10.2 +++ b/src/Pure/General/basics.ML	Fri Sep 10 15:17:44 2010 +0200
    10.3 @@ -94,7 +94,7 @@
    10.4  (* partiality *)
    10.5  
    10.6  fun try f x = SOME (f x)
    10.7 -  handle (exn as Exn.Interrupt) => reraise exn | _ => NONE;
    10.8 +  handle exn => if Exn.is_interrupt exn then reraise exn else NONE;
    10.9  
   10.10  fun can f x = is_some (try f x);
   10.11  
    11.1 --- a/src/Pure/General/exn.ML	Fri Sep 10 14:37:57 2010 +0200
    11.2 +++ b/src/Pure/General/exn.ML	Fri Sep 10 15:17:44 2010 +0200
    11.3 @@ -12,6 +12,10 @@
    11.4    val capture: ('a -> 'b) -> 'a -> 'b result
    11.5    val release: 'a result -> 'a
    11.6    exception Interrupt
    11.7 +  val interrupt: unit -> 'a
    11.8 +  val is_interrupt: exn -> bool
    11.9 +  val interrupt_exn: 'a result
   11.10 +  val is_interrupt_exn: 'a result -> bool
   11.11    exception EXCEPTIONS of exn list
   11.12    val flatten: exn -> exn list
   11.13    val flatten_list: exn list -> exn list
   11.14 @@ -40,14 +44,28 @@
   11.15    | release (Exn e) = reraise e;
   11.16  
   11.17  
   11.18 -(* interrupt and nested exceptions *)
   11.19 +(* interrupts *)
   11.20  
   11.21  exception Interrupt = Interrupt;
   11.22 +
   11.23 +fun interrupt () = raise Interrupt;
   11.24 +
   11.25 +fun is_interrupt Interrupt = true
   11.26 +  | is_interrupt (IO.Io {cause = Interrupt, ...}) = true
   11.27 +  | is_interrupt _ = false;
   11.28 +
   11.29 +val interrupt_exn = Exn Interrupt;
   11.30 +
   11.31 +fun is_interrupt_exn (Exn exn) = is_interrupt exn
   11.32 +  | is_interrupt_exn _ = false;
   11.33 +
   11.34 +
   11.35 +(* nested exceptions *)
   11.36 +
   11.37  exception EXCEPTIONS of exn list;
   11.38  
   11.39 -fun flatten Interrupt = []
   11.40 -  | flatten (EXCEPTIONS exns) = flatten_list exns
   11.41 -  | flatten exn = [exn]
   11.42 +fun flatten (EXCEPTIONS exns) = flatten_list exns
   11.43 +  | flatten exn = if is_interrupt exn then [] else [exn]
   11.44  and flatten_list exns = List.concat (map flatten exns);
   11.45  
   11.46  fun release_all results =
    12.1 --- a/src/Pure/Isar/proof.ML	Fri Sep 10 14:37:57 2010 +0200
    12.2 +++ b/src/Pure/Isar/proof.ML	Fri Sep 10 15:17:44 2010 +0200
    12.3 @@ -990,8 +990,9 @@
    12.4        (case test_proof goal_state of
    12.5          Exn.Result (SOME _) => goal_state
    12.6        | Exn.Result NONE => error (fail_msg (context_of goal_state))
    12.7 -      | Exn.Exn Exn.Interrupt => raise Exn.Interrupt
    12.8 -      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
    12.9 +      | Exn.Exn exn =>
   12.10 +          if Exn.is_interrupt exn then reraise exn
   12.11 +          else raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
   12.12    end;
   12.13  
   12.14  in
    13.1 --- a/src/Pure/Isar/runtime.ML	Fri Sep 10 14:37:57 2010 +0200
    13.2 +++ b/src/Pure/Isar/runtime.ML	Fri Sep 10 15:17:44 2010 +0200
    13.3 @@ -54,30 +54,38 @@
    13.4  
    13.5      val detailed = ! Output.debugging;
    13.6  
    13.7 -    fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
    13.8 -      | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
    13.9 -      | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
   13.10 -          map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
   13.11 -      | exn_msgs _ TERMINATE = ["Exit"]
   13.12 -      | exn_msgs _ Exn.Interrupt = []
   13.13 -      | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
   13.14 -      | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
   13.15 -      | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
   13.16 -      | exn_msgs _ (ERROR msg) = [msg]
   13.17 -      | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
   13.18 -      | exn_msgs _ (exn as THEORY (msg, thys)) =
   13.19 -          [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
   13.20 -      | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
   13.21 -            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
   13.22 -      | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
   13.23 -            (if detailed then
   13.24 -              if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
   13.25 -             else []))]
   13.26 -      | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
   13.27 -            (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
   13.28 -      | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
   13.29 -            (if detailed then if_context ctxt Display.string_of_thm thms else []))]
   13.30 -      | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
   13.31 +    fun exn_msgs context exn =
   13.32 +      if Exn.is_interrupt exn then []
   13.33 +      else
   13.34 +        (case exn of
   13.35 +          Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
   13.36 +        | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
   13.37 +        | EXCURSION_FAIL (exn, loc) =>
   13.38 +            map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs context exn)
   13.39 +        | TERMINATE => ["Exit"]
   13.40 +        | TimeLimit.TimeOut => ["Timeout"]
   13.41 +        | TOPLEVEL_ERROR => ["Error"]
   13.42 +        | SYS_ERROR msg => ["## SYSTEM ERROR ##\n" ^ msg]
   13.43 +        | ERROR msg => [msg]
   13.44 +        | Fail msg => [raised exn "Fail" [msg]]
   13.45 +        | THEORY (msg, thys) =>
   13.46 +            [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
   13.47 +        | Syntax.AST (msg, asts) =>
   13.48 +            [raised exn "AST" (msg ::
   13.49 +              (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
   13.50 +        | TYPE (msg, Ts, ts) =>
   13.51 +            [raised exn "TYPE" (msg ::
   13.52 +              (if detailed then
   13.53 +                if_context context Syntax.string_of_typ Ts @
   13.54 +                if_context context Syntax.string_of_term ts
   13.55 +               else []))]
   13.56 +        | TERM (msg, ts) =>
   13.57 +            [raised exn "TERM" (msg ::
   13.58 +              (if detailed then if_context context Syntax.string_of_term ts else []))]
   13.59 +        | THM (msg, i, thms) =>
   13.60 +            [raised exn ("THM " ^ string_of_int i) (msg ::
   13.61 +              (if detailed then if_context context Display.string_of_thm thms else []))]
   13.62 +        | _ => [raised exn (General.exnMessage exn) []]);
   13.63    in exn_msgs NONE e end;
   13.64  
   13.65  fun exn_message exn_position exn =
   13.66 @@ -102,9 +110,14 @@
   13.67    |> debugging
   13.68    |> Future.interruptible_task;
   13.69  
   13.70 -fun toplevel_error output_exn f x =
   13.71 -  let val ctxt = Option.map Context.proof_of (Context.thread_data ())
   13.72 -  in f x handle exn => (output_exn (exn_context ctxt exn); raise TOPLEVEL_ERROR) end;
   13.73 +fun toplevel_error output_exn f x = f x
   13.74 +  handle exn =>
   13.75 +    if Exn.is_interrupt exn then reraise exn
   13.76 +    else
   13.77 +      let
   13.78 +        val ctxt = Option.map Context.proof_of (Context.thread_data ());
   13.79 +        val _ = output_exn (exn_context ctxt exn);
   13.80 +      in raise TOPLEVEL_ERROR end;
   13.81  
   13.82  end;
   13.83  
    14.1 --- a/src/Pure/Isar/toplevel.ML	Fri Sep 10 14:37:57 2010 +0200
    14.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Sep 10 15:17:44 2010 +0200
    14.3 @@ -30,7 +30,6 @@
    14.4    val timing: bool Unsynchronized.ref
    14.5    val profiling: int Unsynchronized.ref
    14.6    val skip_proofs: bool Unsynchronized.ref
    14.7 -  exception TOPLEVEL_ERROR
    14.8    val program: (unit -> 'a) -> 'a
    14.9    val thread: bool -> (unit -> unit) -> Thread.thread
   14.10    type transition
   14.11 @@ -222,8 +221,6 @@
   14.12  val profiling = Unsynchronized.ref 0;
   14.13  val skip_proofs = Unsynchronized.ref false;
   14.14  
   14.15 -exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
   14.16 -
   14.17  fun program body =
   14.18   (body
   14.19    |> Runtime.controlled_execution
   14.20 @@ -231,7 +228,7 @@
   14.21  
   14.22  fun thread interrupts body =
   14.23    Thread.fork
   14.24 -    (((fn () => body () handle Exn.Interrupt => ())
   14.25 +    (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
   14.26          |> Runtime.debugging
   14.27          |> Runtime.toplevel_error
   14.28            (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
    15.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Fri Sep 10 14:37:57 2010 +0200
    15.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Fri Sep 10 15:17:44 2010 +0200
    15.3 @@ -37,8 +37,10 @@
    15.4        (while not (List.null (! in_buffer)) do
    15.5          PolyML.compiler (get, parameters) ())
    15.6        handle exn =>
    15.7 -       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    15.8 -        error (output ()); reraise exn);
    15.9 +        if Exn.is_interrupt exn then reraise exn
   15.10 +        else
   15.11 +         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
   15.12 +          error (output ()); reraise exn);
   15.13    in if verbose then print (output ()) else () end;
   15.14  
   15.15  fun use_file context verbose name =
    16.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Fri Sep 10 14:37:57 2010 +0200
    16.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Fri Sep 10 15:17:44 2010 +0200
    16.3 @@ -41,8 +41,10 @@
    16.4        (while not (List.null (! in_buffer)) do
    16.5          PolyML.compiler (get, parameters) ())
    16.6        handle exn =>
    16.7 -       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    16.8 -        error (output ()); reraise exn);
    16.9 +        if Exn.is_interrupt exn then reraise exn
   16.10 +        else
   16.11 +         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
   16.12 +          error (output ()); reraise exn);
   16.13    in if verbose then print (output ()) else () end;
   16.14  
   16.15  fun use_file context verbose name =
    17.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Sep 10 14:37:57 2010 +0200
    17.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Sep 10 15:17:44 2010 +0200
    17.3 @@ -148,7 +148,7 @@
    17.4        (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
    17.5  
    17.6      val result = Exn.capture (restore_attributes f) x;
    17.7 -    val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false);
    17.8 +    val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
    17.9  
   17.10      val _ = Thread.interrupt watchdog handle Thread _ => ();
   17.11    in if was_timeout then raise TimeOut else Exn.release result end) ();
   17.12 @@ -209,7 +209,7 @@
   17.13          let val res =
   17.14            sync_wait (SOME orig_atts)
   17.15              (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
   17.16 -        in case res of Exn.Exn Exn.Interrupt => kill 10 | _ => () end;
   17.17 +        in if Exn.is_interrupt_exn res then kill 10 else () end;
   17.18  
   17.19      (*cleanup*)
   17.20      val output = read_file output_name handle IO.Io _ => "";
   17.21 @@ -217,7 +217,7 @@
   17.22      val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
   17.23      val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   17.24      val _ = Thread.interrupt system_thread handle Thread _ => ();
   17.25 -    val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
   17.26 +    val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
   17.27    in (output, rc) end);
   17.28  
   17.29  
    18.1 --- a/src/Pure/ML-Systems/smlnj.ML	Fri Sep 10 14:37:57 2010 +0200
    18.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Fri Sep 10 15:17:44 2010 +0200
    18.3 @@ -142,7 +142,7 @@
    18.4  
    18.5  fun interruptible (f: 'a -> 'b) x =
    18.6    let
    18.7 -    val result = ref (Exn.Exn Interrupt: 'b Exn.result);
    18.8 +    val result = ref (Exn.interrupt_exn: 'b Exn.result);
    18.9      val old_handler = Signals.inqHandler Signals.sigINT;
   18.10    in
   18.11      SMLofNJ.Cont.callcc (fn cont =>
   18.12 @@ -159,16 +159,6 @@
   18.13  end;
   18.14  
   18.15  
   18.16 -(* basis library fixes *)
   18.17 -
   18.18 -structure TextIO =
   18.19 -struct
   18.20 -  open TextIO;
   18.21 -  fun inputLine is = TextIO.inputLine is
   18.22 -    handle IO.Io _ => raise Interrupt;
   18.23 -end;
   18.24 -
   18.25 -
   18.26  
   18.27  (** OS related **)
   18.28  
    19.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 10 14:37:57 2010 +0200
    19.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 10 15:17:44 2010 +0200
    19.3 @@ -25,6 +25,10 @@
    19.4      loc_props
    19.5    end |> Position.of_properties;
    19.6  
    19.7 +fun offset_position_of loc =
    19.8 +  let val pos = position_of loc
    19.9 +  in if is_some (Position.offset_of pos) then pos else Position.none end;
   19.10 +
   19.11  fun exn_position exn =
   19.12    (case PolyML.exceptionLocation exn of
   19.13      NONE => Position.none
   19.14 @@ -44,12 +48,12 @@
   19.15        | _ => Position.report_text);
   19.16  
   19.17      fun report_decl markup loc decl =
   19.18 -      report_text Markup.ML_ref (position_of loc)
   19.19 +      report_text Markup.ML_ref (offset_position_of loc)
   19.20          (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
   19.21      fun report loc (PolyML.PTtype types) =
   19.22            PolyML.NameSpace.displayTypeExpression (types, depth, space)
   19.23            |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
   19.24 -          |> report_text Markup.ML_typing (position_of loc)
   19.25 +          |> report_text Markup.ML_typing (offset_position_of loc)
   19.26        | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
   19.27        | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
   19.28        | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
   19.29 @@ -67,7 +71,7 @@
   19.30  fun eval verbose pos toks =
   19.31    let
   19.32      val _ = Secure.secure_mltext ();
   19.33 -    val {name_space = space, print, error = err, ...} = ML_Env.local_context;
   19.34 +    val space = ML_Env.name_space;
   19.35  
   19.36  
   19.37      (* input *)
   19.38 @@ -99,15 +103,29 @@
   19.39             SOME c));
   19.40  
   19.41  
   19.42 -    (* output *)
   19.43 +    (* output channels *)
   19.44 +
   19.45 +    val writeln_buffer = Unsynchronized.ref Buffer.empty;
   19.46 +    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
   19.47 +    fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
   19.48 +
   19.49 +    val warnings = Unsynchronized.ref ([]: string list);
   19.50 +    fun warn msg = Unsynchronized.change warnings (cons msg);
   19.51 +    fun output_warnings () = List.app warning (rev (! warnings));
   19.52  
   19.53 -    val output_buffer = Unsynchronized.ref Buffer.empty;
   19.54 -    fun output () = Buffer.content (! output_buffer);
   19.55 -    fun put s = Unsynchronized.change output_buffer (Buffer.add s);
   19.56 +    val error_buffer = Unsynchronized.ref Buffer.empty;
   19.57 +    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
   19.58 +    fun flush_error () = writeln (Buffer.content (! error_buffer));
   19.59 +    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
   19.60  
   19.61 -    fun put_message {message, hard, location, context = _} =
   19.62 -     (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");
   19.63 -      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)) ^ "\n"));
   19.64 +    fun message {message = msg, hard, location = loc, context = _} =
   19.65 +      let
   19.66 +        val txt =
   19.67 +          Markup.markup Markup.location
   19.68 +            ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
   19.69 +          Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
   19.70 +          Markup.markup (Position.report_markup (offset_position_of loc)) "";
   19.71 +      in if hard then err txt else warn txt end;
   19.72  
   19.73  
   19.74      (* results *)
   19.75 @@ -118,7 +136,7 @@
   19.76        let
   19.77          fun display disp x =
   19.78            if depth > 0 then
   19.79 -            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
   19.80 +            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
   19.81            else ();
   19.82  
   19.83          fun apply_fix (a, b) =
   19.84 @@ -142,25 +160,27 @@
   19.85          List.app apply_val values
   19.86        end;
   19.87  
   19.88 +    exception STATIC_ERRORS of unit;
   19.89 +
   19.90      fun result_fun (phase1, phase2) () =
   19.91       ((case phase1 of
   19.92          NONE => ()
   19.93        | SOME parse_tree => report_parse_tree depth space parse_tree);
   19.94        (case phase2 of
   19.95 -        NONE => err "Static Errors"
   19.96 +        NONE => raise STATIC_ERRORS ()
   19.97        | SOME code =>
   19.98            apply_result
   19.99              ((code
  19.100                |> Runtime.debugging
  19.101 -              |> Runtime.toplevel_error (Output.error_msg o exn_message)) ())));
  19.102 +              |> Runtime.toplevel_error (err o exn_message)) ())));
  19.103  
  19.104  
  19.105      (* compiler invocation *)
  19.106  
  19.107      val parameters =
  19.108 -     [PolyML.Compiler.CPOutStream put,
  19.109 +     [PolyML.Compiler.CPOutStream write,
  19.110        PolyML.Compiler.CPNameSpace space,
  19.111 -      PolyML.Compiler.CPErrorMessageProc put_message,
  19.112 +      PolyML.Compiler.CPErrorMessageProc message,
  19.113        PolyML.Compiler.CPLineNo (fn () => ! line),
  19.114        PolyML.Compiler.CPLineOffset get_offset,
  19.115        PolyML.Compiler.CPFileName location_props,
  19.116 @@ -170,9 +190,21 @@
  19.117        (while not (List.null (! input_buffer)) do
  19.118          PolyML.compiler (get, parameters) ())
  19.119        handle exn =>
  19.120 -       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
  19.121 -        err (output ()); reraise exn);
  19.122 -  in if verbose then print (output ()) else () end;
  19.123 +        if Exn.is_interrupt exn then reraise exn
  19.124 +        else
  19.125 +          let
  19.126 +            val exn_msg =
  19.127 +              (case exn of
  19.128 +                STATIC_ERRORS () => ""
  19.129 +              | Runtime.TOPLEVEL_ERROR => ""
  19.130 +              | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
  19.131 +            val _ = output_warnings ();
  19.132 +            val _ = output_writeln ();
  19.133 +          in raise_error exn_msg end;
  19.134 +  in
  19.135 +    if verbose then (output_warnings (); flush_error (); output_writeln ())
  19.136 +    else ()
  19.137 +  end;
  19.138  
  19.139  end;
  19.140  
    20.1 --- a/src/Pure/PIDE/document.ML	Fri Sep 10 14:37:57 2010 +0200
    20.2 +++ b/src/Pure/PIDE/document.ML	Fri Sep 10 15:17:44 2010 +0200
    20.3 @@ -225,7 +225,7 @@
    20.4              SOME (st', NONE) => ([], SOME st')
    20.5            | SOME (_, SOME exn_info) =>
    20.6                (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
    20.7 -                [] => raise Exn.Interrupt
    20.8 +                [] => Exn.interrupt ()
    20.9                | errs => (errs, NONE))
   20.10            | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
   20.11          val _ = List.app (Toplevel.error_msg tr) errs;
   20.12 @@ -238,7 +238,10 @@
   20.13                if int then () else async_state tr st'));
   20.14        in result end
   20.15    | Exn.Exn exn =>
   20.16 -     (Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE))
   20.17 +      if Exn.is_interrupt exn then reraise exn
   20.18 +      else
   20.19 +       (Toplevel.error_msg tr (ML_Compiler.exn_message exn);
   20.20 +        Toplevel.status tr Markup.failed; NONE));
   20.21  
   20.22  end;
   20.23  
    21.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Sep 10 14:37:57 2010 +0200
    21.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Sep 10 15:17:44 2010 +0200
    21.3 @@ -983,17 +983,18 @@
    21.4      end handle e => handler (e,SOME src)  (* error in XML parse or Ready issue *)
    21.5  
    21.6  and handler (e,srco) =
    21.7 -    case (e,srco) of
    21.8 -        (XML_PARSE,SOME src) =>
    21.9 -        panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
   21.10 -      | (Exn.Interrupt,SOME src) =>
   21.11 -        (Output.error_msg "Interrupt during PGIP processing"; loop true src)
   21.12 -      | (Toplevel.UNDEF,SOME src) =>
   21.13 -        (Output.error_msg "No working context defined"; loop true src)
   21.14 -      | (e,SOME src) =>
   21.15 -        (Output.error_msg (ML_Compiler.exn_message e); loop true src)
   21.16 -      | (PGIP_QUIT,_) => ()
   21.17 -      | (_,NONE) => ()
   21.18 +    if Exn.is_interrupt e andalso is_some srco then
   21.19 +        (Output.error_msg "Interrupt during PGIP processing"; loop true (the srco))
   21.20 +    else
   21.21 +        case (e,srco) of
   21.22 +            (XML_PARSE,SOME src) =>
   21.23 +            panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
   21.24 +          | (Toplevel.UNDEF,SOME src) =>
   21.25 +            (Output.error_msg "No working context defined"; loop true src)
   21.26 +          | (e,SOME src) =>
   21.27 +            (Output.error_msg (ML_Compiler.exn_message e); loop true src)
   21.28 +          | (PGIP_QUIT,_) => ()
   21.29 +          | (_,NONE) => ()
   21.30  in
   21.31    (* TODO: add socket interface *)
   21.32  
    22.1 --- a/src/Pure/System/isabelle_process.ML	Fri Sep 10 14:37:57 2010 +0200
    22.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Sep 10 15:17:44 2010 +0200
    22.3 @@ -117,7 +117,7 @@
    22.4  end;
    22.5  
    22.6  
    22.7 -(* protocol loop *)
    22.8 +(* protocol loop -- uninterruptible *)
    22.9  
   22.10  val crashes = Unsynchronized.ref ([]: exn list);
   22.11  
    23.1 --- a/src/Pure/System/isar.ML	Fri Sep 10 14:37:57 2010 +0200
    23.2 +++ b/src/Pure/System/isar.ML	Fri Sep 10 15:17:44 2010 +0200
    23.3 @@ -111,7 +111,7 @@
    23.4    | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
    23.5  
    23.6  
    23.7 -(* toplevel loop *)
    23.8 +(* toplevel loop -- uninterruptible *)
    23.9  
   23.10  val crashes = Unsynchronized.ref ([]: exn list);
   23.11  
    24.1 --- a/src/Tools/jEdit/README	Fri Sep 10 14:37:57 2010 +0200
    24.2 +++ b/src/Tools/jEdit/README	Fri Sep 10 15:17:44 2010 +0200
    24.3 @@ -26,9 +26,6 @@
    24.4      previous commands (proof end on proof head), or markup produced by
    24.5      loading external files.
    24.6  
    24.7 -  * Some performance bottlenecks for massive amount of markup,
    24.8 -    e.g. when processing large ML sections.
    24.9 -
   24.10    * General lack of various conveniences known from Proof General.
   24.11  
   24.12  Despite these shortcomings, Isabelle/jEdit already demonstrates that
    25.1 --- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 10 14:37:57 2010 +0200
    25.2 +++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 10 15:17:44 2010 +0200
    25.3 @@ -8,6 +8,8 @@
    25.4  .error { background-color: #FFC1C1; }
    25.5  .debug { background-color: #FFE4E1; }
    25.6  
    25.7 +.location { display: none; }
    25.8 +
    25.9  .hilite { background-color: #FFFACD; }
   25.10  
   25.11  .keyword { font-weight: bold; color: #009966; }
    26.1 --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Sep 10 14:37:57 2010 +0200
    26.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Sep 10 15:17:44 2010 +0200
    26.3 @@ -11,7 +11,6 @@
    26.4  
    26.5  import java.awt.Color
    26.6  
    26.7 -import org.gjt.sp.jedit.GUIUtilities
    26.8  import org.gjt.sp.jedit.syntax.Token
    26.9  
   26.10  
   26.11 @@ -31,8 +30,8 @@
   26.12    {
   26.13      def >= (that: Icon): Boolean = this.priority >= that.priority
   26.14    }
   26.15 -  val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
   26.16 -  val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
   26.17 +  val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png"))
   26.18 +  val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png"))
   26.19  
   26.20  
   26.21    /* command status */
   26.22 @@ -100,7 +99,7 @@
   26.23    val tooltip: Markup_Tree.Select[String] =
   26.24    {
   26.25      case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
   26.26 -      Pretty.string_of(List(Pretty.block(body)), margin = 40)
   26.27 +      Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), margin = 40)
   26.28      case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
   26.29      case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
   26.30      case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
    27.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Sep 10 14:37:57 2010 +0200
    27.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Fri Sep 10 15:17:44 2010 +0200
    27.3 @@ -15,12 +15,15 @@
    27.4  
    27.5  import scala.collection.mutable
    27.6  
    27.7 -import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
    27.8 +import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
    27.9 +  Buffer, EditPane, ServiceManager, View}
   27.10  import org.gjt.sp.jedit.buffer.JEditBuffer
   27.11  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
   27.12  import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
   27.13  import org.gjt.sp.jedit.gui.DockableWindowManager
   27.14  
   27.15 +import org.gjt.sp.util.Log
   27.16 +
   27.17  
   27.18  object Isabelle
   27.19  {
   27.20 @@ -106,6 +109,17 @@
   27.21    }
   27.22  
   27.23  
   27.24 +  /* icons */
   27.25 +
   27.26 +  def load_icon(name: String): javax.swing.Icon =
   27.27 +  {
   27.28 +    val icon = GUIUtilities.loadIcon(name)
   27.29 +    if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
   27.30 +      Log.log(Log.ERROR, icon, "Bad icon: " + name);
   27.31 +    icon
   27.32 +  }
   27.33 +
   27.34 +
   27.35    /* settings */
   27.36  
   27.37    def default_logic(): String =