--- a/src/Pure/Concurrent/future.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Concurrent/future.ML Fri Aug 19 23:48:18 2011 +0200
@@ -31,6 +31,9 @@
that lack regular result information, will pick up parallel
exceptions from the cumulative group context (as Par_Exn).
+ * Future task groups may be canceled: present and future group
+ members will be interrupted eventually.
+
* Promised "passive" futures are fulfilled by external means. There
is no associated evaluation task, but other futures can depend on
them via regular join operations.
@@ -38,31 +41,35 @@
signature FUTURE =
sig
- val worker_task: unit -> Task_Queue.task option
- val worker_group: unit -> Task_Queue.group option
- val worker_subgroup: unit -> Task_Queue.group
+ type task = Task_Queue.task
+ type group = Task_Queue.group
+ val new_group: group option -> group
+ val worker_task: unit -> task option
+ val worker_group: unit -> group option
+ val worker_subgroup: unit -> group
type 'a future
- val task_of: 'a future -> Task_Queue.task
+ val task_of: 'a future -> task
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
val get_finished: 'a future -> 'a
val interruptible_task: ('a -> 'b) -> 'a -> 'b
- val cancel_group: Task_Queue.group -> unit
- val cancel: 'a future -> unit
+ val cancel_group: group -> task list
+ val cancel: 'a future -> task list
type fork_params =
- {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
- pri: int, interrupts: bool}
+ {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
val forks: fork_params -> (unit -> 'a) list -> 'a future list
val fork_pri: int -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
+ val join_tasks: task list -> unit
+ val value_result: 'a Exn.result -> 'a future
val value: 'a -> 'a future
val map: ('a -> 'b) -> 'a future -> 'b future
val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
- val promise_group: Task_Queue.group -> 'a future
- val promise: unit -> 'a future
+ val promise_group: group -> (unit -> unit) -> 'a future
+ val promise: (unit -> unit) -> 'a future
val fulfill_result: 'a future -> 'a Exn.result -> unit
val fulfill: 'a future -> 'a -> unit
val shutdown: unit -> unit
@@ -74,17 +81,22 @@
(** future values **)
+type task = Task_Queue.task;
+type group = Task_Queue.group;
+val new_group = Task_Queue.new_group;
+
+
(* identifiers *)
local
- val tag = Universal.tag () : Task_Queue.task option Universal.tag;
+ val tag = Universal.tag () : task option Universal.tag;
in
fun worker_task () = the_default NONE (Thread.getLocal tag);
fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
end;
val worker_group = Option.map Task_Queue.group_of_task o worker_task;
-fun worker_subgroup () = Task_Queue.new_group (worker_group ());
+fun worker_subgroup () = new_group (worker_group ());
fun worker_joining e =
(case worker_task () of
@@ -103,7 +115,7 @@
datatype 'a future = Future of
{promised: bool,
- task: Task_Queue.task,
+ task: task,
result: 'a result};
fun task_of (Future {task, ...}) = task;
@@ -157,7 +169,7 @@
val queue = Unsynchronized.ref Task_Queue.empty;
val next = Unsynchronized.ref 0;
val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
-val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
+val canceled = Unsynchronized.ref ([]: group list);
val do_shutdown = Unsynchronized.ref false;
val max_workers = Unsynchronized.ref 0;
val max_active = Unsynchronized.ref 0;
@@ -172,15 +184,6 @@
(* cancellation primitives *)
-fun interruptible_task f x =
- if Multithreading.available then
- Multithreading.with_attributes
- (if is_some (worker_task ())
- then Multithreading.private_interrupts
- else Multithreading.public_interrupts)
- (fn _ => f x)
- else interruptible f x;
-
fun cancel_now group = (*requires SYNCHRONIZED*)
Task_Queue.cancel (! queue) group;
@@ -189,6 +192,17 @@
broadcast scheduler_event);
+fun interruptible_task f x =
+ (if Multithreading.available then
+ Multithreading.with_attributes
+ (if is_some (worker_task ())
+ then Multithreading.private_interrupts
+ else Multithreading.public_interrupts)
+ (fn _ => f x)
+ else interruptible f x)
+ before Multithreading.interrupted ();
+
+
(* worker threads *)
fun worker_exec (task, jobs) =
@@ -208,10 +222,10 @@
val _ = SYNCHRONIZED "finish" (fn () =>
let
val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
- val _ = Exn.capture Multithreading.interrupted ();
+ val test = Exn.capture Multithreading.interrupted ();
val _ =
- if ok then ()
- else if cancel_now group then ()
+ if ok andalso not (Exn.is_interrupt_exn test) then ()
+ else if null (cancel_now group) then ()
else cancel_later group;
val _ = broadcast work_finished;
val _ = if maximal then () else signal work_available;
@@ -244,7 +258,7 @@
fun worker_loop name =
(case SYNCHRONIZED name (fn () => worker_next ()) of
NONE => ()
- | SOME work => (Exn.capture Multithreading.interrupted (); worker_exec work; worker_loop name));
+ | SOME work => (worker_exec work; worker_loop name));
fun worker_start name = (*requires SYNCHRONIZED*)
Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
@@ -345,7 +359,7 @@
else
(Multithreading.tracing 1 (fn () =>
string_of_int (length (! canceled)) ^ " canceled groups");
- Unsynchronized.change canceled (filter_out cancel_now);
+ Unsynchronized.change canceled (filter_out (null o cancel_now));
broadcast_work ());
@@ -388,12 +402,15 @@
(** futures **)
-(* cancellation *)
+(* cancel *)
-(*cancel: present and future group members will be interrupted eventually*)
-fun cancel_group group = SYNCHRONIZED "cancel" (fn () =>
- (if cancel_now group then () else cancel_later group;
- signal work_available; scheduler_check ()));
+fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () =>
+ let
+ val running = cancel_now group;
+ val _ =
+ if null running then ()
+ else (cancel_later group; signal work_available; scheduler_check ());
+ in running end);
fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
@@ -430,8 +447,7 @@
Multithreading.with_attributes
(if interrupts
then Multithreading.private_interrupts else Multithreading.no_interrupts)
- (fn _ => Position.setmp_thread_data pos e ()) before
- Multithreading.interrupted ()) ()
+ (fn _ => Position.setmp_thread_data pos e ())) ()
else Exn.interrupt_exn;
in assign_result group result res end;
in (result, job) end;
@@ -440,8 +456,7 @@
(* fork *)
type fork_params =
- {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
- pri: int, interrupts: bool};
+ {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
if null es then []
@@ -469,7 +484,7 @@
end;
fun fork_pri pri e =
- singleton (forks {name = "", group = NONE, deps = [], pri = pri, interrupts = true}) e;
+ (singleton o forks) {name = "fork", group = NONE, deps = [], pri = pri, interrupts = true} e;
fun fork e = fork_pri 0 e;
@@ -521,21 +536,30 @@
fun join_result x = singleton join_results x;
fun join x = Exn.release (join_result x);
+fun join_tasks [] = ()
+ | join_tasks tasks =
+ (singleton o forks)
+ {name = "join_tasks", group = SOME (new_group NONE),
+ deps = tasks, pri = 0, interrupts = false} I
+ |> join;
+
(* fast-path versions -- bypassing task queue *)
-fun value (x: 'a) =
+fun value_result (res: 'a Exn.result) =
let
val task = Task_Queue.dummy_task ();
val group = Task_Queue.group_of_task task;
val result = Single_Assignment.var "value" : 'a result;
- val _ = assign_result group result (Exn.Res x);
+ val _ = assign_result group result res;
in Future {promised = false, task = task, result = result} end;
+fun value x = value_result (Exn.Res x);
+
fun map_future f x =
let
val task = task_of x;
- val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
+ val group = new_group (SOME (Task_Queue.group_of_task task));
val (result, job) = future_job group true (fn () => f (join x));
val extended = SYNCHRONIZED "extend" (fn () =>
@@ -545,32 +569,36 @@
in
if extended then Future {promised = false, task = task, result = result}
else
- singleton
- (forks {name = "Future.map", group = SOME group, deps = [task],
- pri = Task_Queue.pri_of_task task, interrupts = true})
+ (singleton o forks)
+ {name = "map_future", group = SOME group, deps = [task],
+ pri = Task_Queue.pri_of_task task, interrupts = true}
(fn () => f (join x))
end;
fun cond_forks args es =
if Multithreading.enabled () then forks args es
- else map (fn e => value (e ())) es;
+ else map (fn e => value_result (Exn.interruptible_capture e ())) es;
(* promised futures -- fulfilled by external means *)
-fun promise_group group : 'a future =
+fun promise_group group abort : 'a future =
let
val result = Single_Assignment.var "promise" : 'a result;
- fun abort () = assign_result group result Exn.interrupt_exn
+ fun assign () = assign_result group result Exn.interrupt_exn
handle Fail _ => true
| exn =>
- if Exn.is_interrupt exn then raise Fail "Concurrent attempt to fulfill promise"
+ if Exn.is_interrupt exn
+ then raise Fail "Concurrent attempt to fulfill promise"
else reraise exn;
+ fun job () =
+ Multithreading.with_attributes Multithreading.no_interrupts
+ (fn _ => assign () before abort ());
val task = SYNCHRONIZED "enqueue_passive" (fn () =>
- Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
+ Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
in Future {promised = true, task = task, result = result} end;
-fun promise () = promise_group (worker_subgroup ());
+fun promise abort = promise_group (worker_subgroup ()) abort;
fun fulfill_result (Future {promised, task, result}) res =
if not promised then raise Fail "Not a promised future"
--- a/src/Pure/Concurrent/lazy.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Concurrent/lazy.ML Fri Aug 19 23:48:18 2011 +0200
@@ -57,7 +57,7 @@
val (expr, x) =
Synchronized.change_result var
(fn Expr e =>
- let val x = Future.promise ()
+ let val x = Future.promise I
in ((SOME e, x), Result x) end
| Result x => ((NONE, x), Result x));
in
--- a/src/Pure/Concurrent/par_exn.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Concurrent/par_exn.ML Fri Aug 19 23:48:18 2011 +0200
@@ -22,7 +22,11 @@
fun serial exn =
(case get_exn_serial exn of
SOME i => (i, exn)
- | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
+ | NONE =>
+ let
+ val i = Library.serial ();
+ val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
+ in (i, exn') end);
val the_serial = the o get_exn_serial;
--- a/src/Pure/Concurrent/par_list.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Concurrent/par_list.ML Fri Aug 19 23:48:18 2011 +0200
@@ -34,12 +34,13 @@
then map (Exn.capture f) xs
else
let
- val group = Task_Queue.new_group (Future.worker_group ());
+ val group = Future.new_group (Future.worker_group ());
val futures =
Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
(map (fn x => fn () => f x) xs);
val results = Future.join_results futures
- handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
+ handle exn =>
+ (if Exn.is_interrupt exn then ignore (Future.cancel_group group) else (); reraise exn);
in results end;
fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
--- a/src/Pure/Concurrent/task_queue.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Concurrent/task_queue.ML Fri Aug 19 23:48:18 2011 +0200
@@ -31,7 +31,7 @@
val known_task: queue -> task -> bool
val all_passive: queue -> bool
val status: queue -> {ready: int, pending: int, running: int, passive: int}
- val cancel: queue -> group -> bool
+ val cancel: queue -> group -> task list
val cancel_all: queue -> group list
val finish: task -> queue -> bool * queue
val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
@@ -248,10 +248,12 @@
let
val _ = cancel_group group Exn.Interrupt;
val running =
- Tasks.fold (#1 #> get_job jobs #> (fn Running t => insert Thread.equal t | _ => I))
+ Tasks.fold (fn (task, _) =>
+ (case get_job jobs task of Running thread => cons (task, thread) | _ => I))
(get_tasks groups (group_id group)) [];
- val _ = List.app Simple_Thread.interrupt_unsynchronized running;
- in null running end;
+ val threads = fold (insert Thread.equal o #2) running [];
+ val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+ in map #1 running end;
fun cancel_all (Queue {jobs, ...}) =
let
--- a/src/Pure/General/markup.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/General/markup.ML Fri Aug 19 23:48:18 2011 +0200
@@ -119,6 +119,7 @@
val badN: string val bad: T
val functionN: string
val invoke_scala: string -> string -> Properties.T
+ val cancel_scala: string -> Properties.T
val no_output: Output.output * Output.output
val default_output: T -> Output.output * Output.output
val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -377,6 +378,7 @@
val functionN = "function"
fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
+fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
--- a/src/Pure/General/markup.scala Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/General/markup.scala Fri Aug 19 23:48:18 2011 +0200
@@ -283,6 +283,16 @@
}
}
+ val CANCEL_SCALA = "cancel_scala"
+ object Cancel_Scala
+ {
+ def unapply(props: Properties.T): Option[String] =
+ props match {
+ case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
+ case _ => None
+ }
+ }
+
/* system data */
--- a/src/Pure/Isar/runtime.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Isar/runtime.ML Fri Aug 19 23:48:18 2011 +0200
@@ -119,7 +119,7 @@
else f x;
fun controlled_execution f x =
- ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
+ (f |> debugging |> Future.interruptible_task) x;
fun toplevel_error output_exn f x = f x
handle exn =>
--- a/src/Pure/Isar/toplevel.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Isar/toplevel.ML Fri Aug 19 23:48:18 2011 +0200
@@ -419,6 +419,14 @@
(* theory transitions *)
+val global_theory_group =
+ Sign.new_group #>
+ Global_Theory.begin_recent_proofs #> Theory.checkpoint;
+
+val local_theory_group =
+ Local_Theory.new_group #>
+ Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
+
fun generic_theory f = transaction (fn _ =>
(fn Theory (gthy, _) => Theory (f gthy, NONE)
| _ => raise UNDEF));
@@ -426,8 +434,7 @@
fun theory' f = transaction (fn int =>
(fn Theory (Context.Theory thy, _) =>
let val thy' = thy
- |> Sign.new_group
- |> Theory.checkpoint
+ |> global_theory_group
|> f int
|> Sign.reset_group;
in Theory (Context.Theory thy', NONE) end
@@ -454,7 +461,7 @@
let
val finish = loc_finish loc gthy;
val lthy' = loc_begin loc gthy
- |> Local_Theory.new_group
+ |> local_theory_group
|> f int
|> Local_Theory.reset_group;
in Theory (finish lthy', SOME lthy') end
@@ -506,13 +513,13 @@
in
fun local_theory_to_proof' loc f = begin_proof
- (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
+ (fn int => fn gthy => f int (local_theory_group (loc_begin loc gthy)))
(fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
fun theory_to_proof f = begin_proof
- (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
+ (K (fn Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))
(K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
end;
--- a/src/Pure/PIDE/document.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/PIDE/document.ML Fri Aug 19 23:48:18 2011 +0200
@@ -24,7 +24,7 @@
type state
val init_state: state
val join_commands: state -> unit
- val cancel_execution: state -> unit -> unit
+ val cancel_execution: state -> Future.task list
val define_command: command_id -> string -> state -> state
val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
val execute: version_id -> state -> state
@@ -164,7 +164,7 @@
{versions: version Inttab.table, (*version_id -> document content*)
commands: Toplevel.transition future Inttab.table, (*command_id -> transition (future parsing)*)
execs: Toplevel.state lazy Inttab.table, (*exec_id -> execution process*)
- execution: unit future list} (*global execution process*)
+ execution: Future.group} (*global execution process*)
with
fun make_state (versions, commands, execs, execution) =
@@ -177,7 +177,7 @@
make_state (Inttab.make [(no_id, empty_version)],
Inttab.make [(no_id, Future.value Toplevel.empty)],
Inttab.make [(no_id, empty_exec)],
- []);
+ Future.new_group NONE);
(* document versions *)
@@ -200,9 +200,10 @@
map_state (fn (versions, commands, execs, execution) =>
let
val id_string = print_id id;
- val tr = Future.fork_pri 2 (fn () =>
- Position.setmp_thread_data (Position.id_only id_string)
- (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
+ val tr =
+ Future.fork_pri 2 (fn () =>
+ Position.setmp_thread_data (Position.id_only id_string)
+ (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
val commands' =
Inttab.update_new (id, tr) commands
handle Inttab.DUP dup => err_dup "command" dup;
@@ -233,9 +234,7 @@
(* document execution *)
-fun cancel_execution (State {execution, ...}) =
- (List.app Future.cancel execution;
- fn () => ignore (Future.join_results execution));
+fun cancel_execution (State {execution, ...}) = Future.cancel_group execution;
end;
@@ -253,13 +252,13 @@
| NONE => ());
fun async_state tr st =
- ignore
- (singleton
- (Future.forks {name = "Document.async_state",
- group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
- (fn () =>
- Toplevel.setmp_thread_position tr
- (fn () => Toplevel.print_state false st) ()));
+ (singleton o Future.forks)
+ {name = "Document.async_state", group = SOME (Future.new_group NONE),
+ deps = [], pri = 0, interrupts = true}
+ (fn () =>
+ Toplevel.setmp_thread_position tr
+ (fn () => Toplevel.print_state false st) ())
+ |> ignore;
fun run int tr st =
(case Toplevel.transition int tr st of
@@ -355,9 +354,9 @@
fun get_command id =
(id, the_command state id |> Future.map (Toplevel.modify_init init));
in
- singleton
- (Future.forks {name = "Document.edit", group = NONE,
- deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false})
+ (singleton o Future.forks)
+ {name = "Document.edit", group = NONE,
+ deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
(fn () =>
let
val prev_exec =
@@ -393,17 +392,16 @@
fun force_exec NONE = ()
| force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
- val execution' =
+ val execution = Future.new_group NONE;
+ val _ =
nodes_of version |> Graph.schedule
(fn deps => fn (name, node) =>
- singleton
- (Future.forks
- {name = "theory:" ^ name, group = NONE,
- deps = map (Future.task_of o #2) deps,
- pri = 1, interrupts = true})
+ (singleton o Future.forks)
+ {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
+ deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
(fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
- in (versions, commands, execs, execution') end);
+ in (versions, commands, execs, execution) end);
--- a/src/Pure/PIDE/isar_document.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/PIDE/isar_document.ML Fri Aug 19 23:48:18 2011 +0200
@@ -30,9 +30,9 @@
fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
end;
- val await_cancellation = Document.cancel_execution state;
+ val running = Document.cancel_execution state;
val (updates, state') = Document.edit old_id new_id edits state;
- val _ = await_cancellation ();
+ val _ = Future.join_tasks running;
val _ = Document.join_commands state';
val _ =
Output.status (Markup.markup (Markup.assign new_id)
--- a/src/Pure/System/invoke_scala.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/System/invoke_scala.ML Fri Aug 19 23:48:18 2011 +0200
@@ -33,7 +33,8 @@
fun promise_method name arg =
let
val id = new_id ();
- val promise = Future.promise () : string future;
+ fun abort () = Output.raw_message (Markup.cancel_scala id) "";
+ val promise = Future.promise abort : string future;
val _ = Synchronized.change promises (Symtab.update (id, promise));
val _ = Output.raw_message (Markup.invoke_scala name id) arg;
in promise end;
--- a/src/Pure/System/session.scala Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/System/session.scala Fri Aug 19 23:48:18 2011 +0200
@@ -275,6 +275,8 @@
val (tag, res) = Invoke_Scala.method(name, arg)
prover.get.invoke_scala(id, tag, res)
}
+ case Markup.Cancel_Scala(id) =>
+ System.err.println("cancel_scala " + id) // FIXME cancel JVM task
case _ =>
if (result.is_syslog) {
reverse_syslog ::= result.message
--- a/src/Pure/Thy/thy_info.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Thy/thy_info.ML Fri Aug 19 23:48:18 2011 +0200
@@ -194,11 +194,9 @@
Graph.schedule (fn deps => fn (name, task) =>
(case task of
Task (parents, body) =>
- singleton
- (Future.forks
- {name = "theory:" ^ name, group = NONE,
- deps = map (Future.task_of o #2) deps,
- pri = 0, interrupts = true})
+ (singleton o Future.forks)
+ {name = "theory:" ^ name, group = NONE,
+ deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
(fn () =>
(case filter (not o can Future.join o #2) deps of
[] => body (map (#1 o Future.join) (task_parents deps parents))
--- a/src/Pure/global_theory.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/global_theory.ML Fri Aug 19 23:48:18 2011 +0200
@@ -10,6 +10,8 @@
val intern_fact: theory -> xstring -> string
val defined_fact: theory -> string -> bool
val hide_fact: bool -> string -> theory -> theory
+ val begin_recent_proofs: theory -> theory
+ val join_recent_proofs: theory -> unit
val join_proofs: theory -> unit
val get_fact: Context.generic -> theory -> Facts.ref -> thm list
val get_thms: theory -> xstring -> thm list
@@ -49,10 +51,10 @@
structure Data = Theory_Data
(
- type T = Facts.T * thm list;
- val empty = (Facts.empty, []);
- fun extend (facts, _) = (facts, []);
- fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+ type T = Facts.T * (thm list * thm list);
+ val empty = (Facts.empty, ([], []));
+ fun extend (facts, _) = (facts, ([], []));
+ fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
);
@@ -68,10 +70,11 @@
(* proofs *)
-fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms);
+fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (append thms))) thy, thms);
-fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy)));
-
+val begin_recent_proofs = Data.map (apsnd (fn (_, thms) => ([], thms)));
+val join_recent_proofs = Thm.join_proofs o rev o #1 o #2 o Data.get;
+val join_proofs = Thm.join_proofs o rev o #2 o #2 o Data.get;
(** retrieve theorems **)
--- a/src/Pure/goal.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/goal.ML Fri Aug 19 23:48:18 2011 +0200
@@ -124,8 +124,8 @@
let
val _ = forked 1;
val future =
- singleton
- (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
+ (singleton o Future.forks)
+ {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
(fn () =>
Exn.release
(Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
--- a/src/Pure/proofterm.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/proofterm.ML Fri Aug 19 23:48:18 2011 +0200
@@ -37,11 +37,11 @@
type oracle = string * term
type pthm = serial * (string * term * proof_body future)
+ val join_body: proof_body -> unit
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
- val join_bodies: proof_body list -> unit
val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
val oracle_ord: oracle * oracle -> order
@@ -171,6 +171,10 @@
type oracle = string * term;
type pthm = serial * (string * term * proof_body future);
+fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm)));
+fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms);
+fun join_body (PBody {thms, ...}) = join_thms thms;
+
fun proof_of (PBody {proof, ...}) = proof;
val join_proof = Future.join #> proof_of;
@@ -195,18 +199,15 @@
fun fold_body_thms f =
let
fun app (PBody {thms, ...}) =
- (Future.join_results (map (#3 o #2) thms);
- thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+ tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
let
val body' = Future.join body;
val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
- in (f (name, prop, body') x', seen') end));
+ in (f (name, prop, body') x', seen') end);
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
-fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
-
fun status_of bodies =
let
fun status (PBody {oracles, thms, ...}) x =
@@ -242,14 +243,13 @@
val all_oracles_of =
let
fun collect (PBody {oracles, thms, ...}) =
- (Future.join_results (map (#3 o #2) thms);
- thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+ tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
let
val body' = Future.join body;
val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
- in (merge_oracles oracles x', seen') end));
+ in (merge_oracles oracles x', seen') end);
in fn body => #1 (collect body ([], Inttab.empty)) end;
fun approximate_proof_body prf =
@@ -1396,16 +1396,17 @@
| fill _ = NONE;
val (rules, procs) = get_data thy;
val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
+ val _ = join_thms thms;
in PBody {oracles = oracles, thms = thms, proof = proof} end;
fun fulfill_proof_future _ [] postproc body =
if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
else Future.map postproc body
| fulfill_proof_future thy promises postproc body =
- singleton
- (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
- deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
- interrupts = true})
+ (singleton o Future.forks)
+ {name = "Proofterm.fulfill_proof_future", group = NONE,
+ deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
+ interrupts = true}
(fn () =>
postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
@@ -1461,10 +1462,9 @@
if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
else
- singleton
- (Future.forks
- {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
- interrupts = true})
+ (singleton o Future.forks)
+ {name = "Proofterm.prepare_thm_proof", group = NONE,
+ deps = [], pri = ~1, interrupts = true}
(make_body0 o full_proof0);
fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
--- a/src/Pure/thm.ML Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/thm.ML Fri Aug 19 23:48:18 2011 +0200
@@ -517,9 +517,9 @@
(map #1 promises ~~ fulfill_bodies (map #2 promises)) body
and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
-val join_proofs = Proofterm.join_bodies o map fulfill_body;
+fun join_proofs thms = ignore (map fulfill_body thms);
-fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
+fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
val proof_of = Proofterm.proof_of o proof_body_of;
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Fri Aug 19 23:48:18 2011 +0200
@@ -21,7 +21,6 @@
extends Dockable(view: View, position: String)
{
private val text_area = new TextArea
- text_area.editable = false
set_content(new ScrollPane(text_area))
--- a/src/Tools/jEdit/src/session_dockable.scala Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Tools/jEdit/src/session_dockable.scala Fri Aug 19 23:48:18 2011 +0200
@@ -28,7 +28,6 @@
readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
private val syslog = new TextArea(Isabelle.session.syslog())
- syslog.editable = false
private val tabs = new TabbedPane {
pages += new TabbedPane.Page("README", Component.wrap(readme))