# HG changeset patch # User wenzelm # Date 1284124664 -7200 # Node ID f263522ab226aa02eff1cb575972c65ed4b98adc # Parent 2ad95934521f66b72eb649147966b402d7892a03# Parent cc155a9bf3a23462e31da14b551e420115a621b9 merged diff -r 2ad95934521f -r f263522ab226 NEWS --- 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 *** diff -r 2ad95934521f -r f263522ab226 src/HOL/Import/proof_kernel.ML --- 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 diff -r 2ad95934521f -r f263522ab226 src/HOL/Mirabelle/Tools/mirabelle.ML --- 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 diff -r 2ad95934521f -r f263522ab226 src/HOL/Tools/meson.ML --- 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)*) diff -r 2ad95934521f -r f263522ab226 src/Pure/Concurrent/future.ML --- 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); diff -r 2ad95934521f -r f263522ab226 src/Pure/Concurrent/lazy.ML --- 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) ()); diff -r 2ad95934521f -r f263522ab226 src/Pure/Concurrent/lazy_sequential.ML --- 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); diff -r 2ad95934521f -r f263522ab226 src/Pure/Concurrent/simple_thread.ML --- 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 _ => (); diff -r 2ad95934521f -r f263522ab226 src/Pure/Concurrent/task_queue.ML --- 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 *) diff -r 2ad95934521f -r f263522ab226 src/Pure/General/basics.ML --- 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); diff -r 2ad95934521f -r f263522ab226 src/Pure/General/exn.ML --- 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 = diff -r 2ad95934521f -r f263522ab226 src/Pure/Isar/proof.ML --- 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 diff -r 2ad95934521f -r f263522ab226 src/Pure/Isar/runtime.ML --- 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; diff -r 2ad95934521f -r f263522ab226 src/Pure/Isar/toplevel.ML --- 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))), diff -r 2ad95934521f -r f263522ab226 src/Pure/ML-Systems/compiler_polyml-5.2.ML --- 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 = diff -r 2ad95934521f -r f263522ab226 src/Pure/ML-Systems/compiler_polyml-5.3.ML --- 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 = diff -r 2ad95934521f -r f263522ab226 src/Pure/ML-Systems/multithreading_polyml.ML --- 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); diff -r 2ad95934521f -r f263522ab226 src/Pure/ML-Systems/smlnj.ML --- 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 **) diff -r 2ad95934521f -r f263522ab226 src/Pure/ML/ml_compiler_polyml-5.3.ML --- 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; diff -r 2ad95934521f -r f263522ab226 src/Pure/PIDE/document.ML --- 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; diff -r 2ad95934521f -r f263522ab226 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 *) diff -r 2ad95934521f -r f263522ab226 src/Pure/System/isabelle_process.ML --- 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); diff -r 2ad95934521f -r f263522ab226 src/Pure/System/isar.ML --- 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); diff -r 2ad95934521f -r f263522ab226 src/Tools/jEdit/README --- 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 diff -r 2ad95934521f -r f263522ab226 src/Tools/jEdit/dist-template/etc/isabelle-jedit.css --- 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; } diff -r 2ad95934521f -r f263522ab226 src/Tools/jEdit/src/jedit/isabelle_markup.scala --- 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" diff -r 2ad95934521f -r f263522ab226 src/Tools/jEdit/src/jedit/plugin.scala --- 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 =