--- a/Admin/lib/Tools/makedist_bundle Wed Jul 10 12:25:11 2013 +0200
+++ b/Admin/lib/Tools/makedist_bundle Wed Jul 10 12:35:18 2013 +0200
@@ -147,15 +147,15 @@
"contrib/cygwin/isabelle/."
done
- find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 | \
- sort > "contrib/cygwin/isabelle/executables"
+ find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 \
+ -print0 > "contrib/cygwin/isabelle/executables"
cat >> "contrib/cygwin/isabelle/postinstall" <<EOF
find -type d -exec chmod 755 '{}' +
find -type f \( -name '*.exe' -o -name '*.dll' \) -exec chmod 755 '{}' +
find -type f -not -name '*.exe' -not -name '*.dll' -exec chmod 644 '{}' +
-xargs < contrib/cygwin/isabelle/executables chmod 755
+xargs -0 < contrib/cygwin/isabelle/executables chmod 755
EOF
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy Wed Jul 10 12:25:11 2013 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Wed Jul 10 12:35:18 2013 +0200
@@ -167,9 +167,7 @@
lemma Example2_lemma2_aux2:
"j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
-apply(induct j)
- apply (simp_all cong:setsum_cong)
-done
+ by (induct j) simp_all
lemma Example2_lemma2:
"\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat=0..<n. b i)=(\<Sum>i=0..<n. (b (j := Suc 0)) i)"
@@ -212,7 +210,7 @@
apply(force)
apply clarify
apply simp
-apply(simp cong:setsum_ivl_cong)
+apply simp
apply clarify
apply simp
apply(rule Await)
@@ -228,7 +226,7 @@
apply clarify
apply simp
apply(simp add:Example2_lemma2_Suc0 cong:if_cong)
-apply simp+
+apply simp_all
done
subsection {* Find Least Element *}
--- a/src/Pure/Concurrent/future.ML Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Jul 10 12:35:18 2013 +0200
@@ -47,6 +47,7 @@
val worker_task: unit -> task option
val worker_group: unit -> group option
val worker_subgroup: unit -> group
+ val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b
type 'a future
val task_of: 'a future -> task
val peek: 'a future -> 'a Exn.result option
@@ -100,6 +101,11 @@
val worker_group = Option.map Task_Queue.group_of_task o worker_task;
fun worker_subgroup () = new_group (worker_group ());
+fun worker_guest name group f x =
+ if is_some (worker_task ()) then
+ raise Fail "Already running as worker thread"
+ else setmp_worker_task (Task_Queue.new_task group name NONE) f x;
+
fun worker_joining e =
(case worker_task () of
NONE => e ()
@@ -266,15 +272,12 @@
in () end;
fun worker_wait active cond = (*requires SYNCHRONIZED*)
- let
- val state =
- (case AList.lookup Thread.equal (! workers) (Thread.self ()) of
- SOME state => state
- | NONE => raise Fail "Unregistered worker thread");
- val _ = state := (if active then Waiting else Sleeping);
- val _ = wait cond;
- val _ = state := Working;
- in () end;
+ (case AList.lookup Thread.equal (! workers) (Thread.self ()) of
+ SOME state =>
+ (state := (if active then Waiting else Sleeping);
+ wait cond;
+ state := Working)
+ | NONE => ignore (wait cond));
fun worker_next () = (*requires SYNCHRONIZED*)
if length (! workers) > ! max_workers then
--- a/src/Pure/Concurrent/task_queue.ML Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Wed Jul 10 12:35:18 2013 +0200
@@ -17,6 +17,7 @@
val str_of_groups: group -> string
type task
val dummy_task: task
+ val new_task: group -> string -> int option -> task
val group_of_task: task -> group
val name_of_task: task -> string
val pri_of_task: task -> int
--- a/src/Pure/General/linear_set.ML Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/General/linear_set.ML Wed Jul 10 12:35:18 2013 +0200
@@ -83,17 +83,17 @@
fun iterate opt_start f set =
let
val entries = entries_of set;
- fun apply _ NONE y = y
- | apply prev (SOME key) y =
+ fun iter _ NONE y = y
+ | iter prev (SOME key) y =
let
val (x, next) = the_entry entries key;
val item = ((prev, key), x);
in
(case f item y of
NONE => y
- | SOME y' => apply (SOME key) next y')
+ | SOME y' => iter (SOME key) next y')
end;
- in apply NONE (optional_start set opt_start) end;
+ in iter NONE (optional_start set opt_start) end;
fun dest set = rev (iterate NONE (fn ((_, key), x) => SOME o cons (key, x)) set []);
--- a/src/Pure/Isar/toplevel.ML Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Jul 10 12:35:18 2013 +0200
@@ -154,7 +154,9 @@
| level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
| level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1; (*different notion of proof depth!*)
-fun str_of_state (State (NONE, _)) = "at top level"
+fun str_of_state (State (NONE, SOME (Theory (Context.Theory thy, _)))) =
+ "at top level, result theory " ^ quote (Context.theory_name thy)
+ | str_of_state (State (NONE, _)) = "at top level"
| str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode"
| str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode"
| str_of_state (State (SOME (Proof _), _)) = "in proof mode"
--- a/src/Pure/PIDE/command.ML Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/PIDE/command.ML Wed Jul 10 12:35:18 2013 +0200
@@ -10,18 +10,22 @@
type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
val eval_result_state: eval -> Toplevel.state
type print_process
- type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
+ type print =
+ {name: string, pri: int, persistent: bool,
+ exec_id: Document_ID.exec, print_process: print_process}
type exec = eval * print list
val no_exec: exec
- val exec_ids: exec -> Document_ID.exec list
+ val exec_ids: exec option -> Document_ID.exec list
+ val stable_eval: eval -> bool
+ val stable_print: print -> bool
val read: (unit -> theory) -> Token.T list -> Toplevel.transition
val eval: (unit -> theory) -> Token.T list -> eval -> eval
- val print: string -> eval -> print list
+ val print: bool -> string -> eval -> print list -> print list option
type print_fn = Toplevel.transition -> Toplevel.state -> unit
- val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
+ val print_function: {name: string, pri: int, persistent: bool} ->
+ ({command_name: string} -> print_fn option) -> unit
+ val no_print_function: string -> unit
val execute: exec -> unit
- val stable_eval: eval -> bool
- val stable_print: print -> bool
end;
structure Command: COMMAND =
@@ -85,12 +89,27 @@
val eval_result_state = #state o eval_result;
type print_process = unit memo;
-type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
+type print =
+ {name: string, pri: int, persistent: bool,
+ exec_id: Document_ID.exec, print_process: print_process};
type exec = eval * print list;
val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
-fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
+fun exec_ids (NONE: exec option) = []
+ | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints;
+
+
+(* stable results *)
+
+fun stable_goals exec_id =
+ not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
+
+fun stable_eval ({exec_id, eval_process}: eval) =
+ stable_goals exec_id andalso memo_stable eval_process;
+
+fun stable_print ({exec_id, print_process, ...}: print) =
+ stable_goals exec_id andalso memo_stable print_process;
(* read *)
@@ -196,75 +215,85 @@
local
-type print_function = string * (int * (string -> print_fn option));
+type print_function = string * (int * bool * ({command_name: string} -> print_fn option));
val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
-fun output_error tr exn =
- List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
-
-fun print_error tr f x =
- (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) f x
- handle exn => output_error tr exn;
+fun print_error tr e =
+ (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
+ List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
in
-fun print command_name eval =
- rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
- (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
- Exn.Res NONE => NONE
- | Exn.Res (SOME print_fn) =>
- let
- val exec_id = Document_ID.make ();
- fun process () =
- let
- val {failed, command, state = st', ...} = eval_result eval;
- val tr = Toplevel.exec_id exec_id command;
- in if failed then () else print_error tr (fn () => print_fn tr st') () end;
- in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
- | Exn.Exn exn =>
- let
- val exec_id = Document_ID.make ();
- fun process () =
- let
- val {command, ...} = eval_result eval;
- val tr = Toplevel.exec_id exec_id command;
- in output_error tr exn end;
- in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
+fun print command_visible command_name eval old_prints =
+ let
+ fun new_print (name, (pri, persistent, get_fn)) =
+ let
+ fun make_print strict print_fn =
+ let
+ val exec_id = Document_ID.make ();
+ fun process () =
+ let
+ val {failed, command, state = st', ...} = eval_result eval;
+ val tr = Toplevel.exec_id exec_id command;
+ in
+ if failed andalso not strict then ()
+ else print_error tr (fn () => print_fn tr st')
+ end;
+ in
+ {name = name, pri = pri, persistent = persistent,
+ exec_id = exec_id, print_process = memo process}
+ end;
+ in
+ (case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
+ Exn.Res NONE => NONE
+ | Exn.Res (SOME print_fn) => SOME (make_print false print_fn)
+ | Exn.Exn exn => SOME (make_print true (fn _ => fn _ => reraise exn)))
+ end;
-fun print_function {name, pri} f =
+ val new_prints =
+ if command_visible then
+ rev (Synchronized.value print_functions) |> map_filter (fn pr =>
+ (case find_first (equal (fst pr) o #name) old_prints of
+ SOME print => if stable_print print then SOME print else new_print pr
+ | NONE => new_print pr))
+ else filter (fn print => #persistent print andalso stable_print print) old_prints;
+ in
+ if eq_list (op = o pairself #exec_id) (old_prints, new_prints) then NONE
+ else SOME new_prints
+ end;
+
+fun print_function {name, pri, persistent} f =
Synchronized.change print_functions (fn funs =>
(if not (AList.defined (op =) funs name) then ()
else warning ("Redefining command print function: " ^ quote name);
- AList.update (op =) (name, (pri, f)) funs));
+ AList.update (op =) (name, (pri, persistent, f)) funs));
+
+fun no_print_function name =
+ Synchronized.change print_functions (filter_out (equal name o #1));
end;
val _ =
- print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' =>
- let
- val is_init = Keyword.is_theory_begin command_name;
- val is_proof = Keyword.is_proof command_name;
- val do_print =
- not is_init andalso
- (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
- in if do_print then Toplevel.print_state false st' else () end));
+ print_function {name = "print_state", pri = 0, persistent = true}
+ (fn {command_name} => SOME (fn tr => fn st' =>
+ let
+ val is_init = Keyword.is_theory_begin command_name;
+ val is_proof = Keyword.is_proof command_name;
+ val do_print =
+ not is_init andalso
+ (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
+ in if do_print then Toplevel.print_state false st' else () end));
(* overall execution process *)
-fun execute (({eval_process, ...}, prints): exec) =
- (memo_eval eval_process;
- prints |> List.app (fn {name, pri, print_process, ...} =>
- memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
+fun run_print ({name, pri, print_process, ...}: print) =
+ (if Multithreading.enabled () then
+ memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
+ else memo_eval) print_process;
-fun stable_goals exec_id =
- not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
-
-fun stable_eval ({exec_id, eval_process}: eval) =
- stable_goals exec_id andalso memo_stable eval_process;
-
-fun stable_print ({exec_id, print_process, ...}: print) =
- stable_goals exec_id andalso memo_stable print_process;
+fun execute (({eval_process, ...}, prints): exec) =
+ (memo_eval eval_process; List.app run_print prints);
end;
--- a/src/Pure/PIDE/document.ML Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/PIDE/document.ML Wed Jul 10 12:35:18 2013 +0200
@@ -84,7 +84,7 @@
fun set_perspective ids =
map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
-val visible_commands = #1 o get_perspective;
+val visible_command = Inttab.defined o #1 o get_perspective;
val visible_last = #2 o get_perspective;
val visible_node = is_some o visible_last
@@ -108,6 +108,12 @@
fun set_result result =
map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
+fun changed_result node node' =
+ (case (get_result node, get_result node') of
+ (SOME eval, SOME eval') => #exec_id eval <> #exec_id eval'
+ | (NONE, NONE) => false
+ | _ => true);
+
fun finished_theory node =
(case Exn.capture (Command.eval_result_state o the) (get_result node) of
Exn.Res st => can (Toplevel.end_theory Position.none) st
@@ -144,11 +150,9 @@
fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
| the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
-fun update_entry id exec =
- map_entries (Entries.update (id, exec));
-
-fun reset_entry id node =
- if is_some (lookup_entry node id) then update_entry id NONE node else node;
+fun assign_entry (command_id, exec) node =
+ if is_none (Entries.lookup (get_entries node) command_id) then node
+ else map_entries (Entries.update (command_id, exec)) node;
fun reset_after id entries =
(case Entries.get_after entries id of
@@ -275,8 +279,13 @@
NONE => err_undef "command" command_id
| SOME command => command);
+val the_command_name = #1 oo the_command;
+
end;
+
+(* remove_versions *)
+
fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
let
val _ =
@@ -304,29 +313,46 @@
let
val {version_id, group, running} = execution_of state;
val _ =
- (singleton o Future.forks)
- {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
- (fn () =>
- (OS.Process.sleep (seconds 0.02);
- nodes_of (the_version state version_id) |> String_Graph.schedule
- (fn deps => fn (name, node) =>
- if not (visible_node node) andalso finished_theory node then
- Future.value ()
- else
- (singleton o Future.forks)
- {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
- deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
- (fn () =>
- iterate_entries (fn (_, opt_exec) => fn () =>
- (case opt_exec of
- SOME exec => if ! running then SOME (Command.execute exec) else NONE
- | NONE => NONE)) node ()))));
+ if not (! running) orelse Task_Queue.is_canceled group then []
+ else
+ nodes_of (the_version state version_id) |> String_Graph.schedule
+ (fn deps => fn (name, node) =>
+ if not (visible_node node) andalso finished_theory node then
+ Future.value ()
+ else
+ (singleton o Future.forks)
+ {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
+ deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
+ (fn () =>
+ iterate_entries (fn (_, opt_exec) => fn () =>
+ (case opt_exec of
+ SOME exec => if ! running then SOME (Command.execute exec) else NONE
+ | NONE => NONE)) node ()));
in () end;
(** document update **)
+(* exec state assignment *)
+
+type assign_update = Command.exec option Inttab.table; (*command id -> exec*)
+
+val assign_update_empty: assign_update = Inttab.empty;
+fun assign_update_null (tab: assign_update) = Inttab.is_empty tab;
+fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
+fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
+
+fun assign_update_new upd (tab: assign_update) =
+ Inttab.update_new upd tab
+ handle Inttab.DUP dup => err_dup "exec state assignment" dup;
+
+fun assign_update_result (tab: assign_update) =
+ Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab [];
+
+
+(* update *)
+
val timing = Unsynchronized.ref false;
fun timeit msg e = cond_timeit (! timing) msg e;
@@ -370,17 +396,18 @@
is_some (Thy_Info.lookup_theory name) orelse
can get_header node andalso (not full orelse is_some (get_result node));
-fun last_common state last_visible node0 node =
+fun last_common state node0 node =
let
fun update_flags prev (visible, initial) =
let
- val visible' = visible andalso prev <> last_visible;
+ val visible' = visible andalso prev <> visible_last node;
val initial' = initial andalso
(case prev of
NONE => true
- | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
+ | SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id)));
in (visible', initial') end;
- fun get_common ((prev, id), opt_exec) (same, (_, flags)) =
+
+ fun get_common ((prev, command_id), opt_exec) (_, same, flags, assign_update) =
if same then
let
val flags' = update_flags prev flags;
@@ -388,52 +415,49 @@
(case opt_exec of
NONE => false
| SOME (eval, _) =>
- (case lookup_entry node0 id of
+ (case lookup_entry node0 command_id of
NONE => false
| SOME (eval0, _) =>
#exec_id eval = #exec_id eval0 andalso Command.stable_eval eval));
- in SOME (same', (prev, flags')) end
+ val assign_update' = assign_update |>
+ (case opt_exec of
+ SOME (eval, prints) =>
+ let
+ val command_visible = visible_command node command_id;
+ val command_name = the_command_name state command_id;
+ in
+ (case Command.print command_visible command_name eval prints of
+ SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
+ | NONE => I)
+ end
+ | NONE => I);
+ in SOME (prev, same', flags', assign_update') end
else NONE;
- val (same, (common, flags)) =
- iterate_entries get_common node (true, (NONE, (true, true)));
- in
- if same then
- let val last = Entries.get_after (get_entries node) common
- in (last, update_flags last flags) end
- else (common, flags)
- end;
+ val (common, same, flags, assign_update') =
+ iterate_entries get_common node (NONE, true, (true, true), assign_update_empty);
+ val (common', flags') =
+ if same then
+ let val last = Entries.get_after (get_entries node) common
+ in (last, update_flags last flags) end
+ else (common, flags);
+ in (assign_update', common', flags') end;
fun illegal_init _ = error "Illegal theory header after end of theory";
-fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
+fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) =
if not proper_init andalso is_none init then NONE
else
let
val (_, (eval, _)) = command_exec;
val (command_name, span) = the_command state command_id' ||> Lazy.force;
- val init' = if Keyword.is_theory_begin command_name then NONE else init;
- val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
- val prints' = if command_visible then Command.print command_name eval' else [];
- val command_exec' = (command_id', (eval', prints'));
- in SOME (command_exec' :: execs, command_exec', init') end;
-fun update_prints state node command_id =
- (case the_entry node command_id of
- SOME (eval, prints) =>
- let
- val (command_name, _) = the_command state command_id;
- val new_prints = Command.print command_name eval;
- val prints' =
- new_prints |> map (fn new_print =>
- (case find_first (fn {name, ...} => name = #name new_print) prints of
- SOME print => if Command.stable_print print then print else new_print
- | NONE => new_print));
- in
- if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
- else SOME (command_id, (eval, prints'))
- end
- | NONE => NONE);
+ val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
+ val prints' = perhaps (Command.print command_visible command_name eval') [];
+ val exec' = (eval', prints');
+ val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
+ val init' = if Keyword.is_theory_begin command_name then NONE else init;
+ in SOME (assign_update', (command_id', (eval', prints')), init') end;
in
fun update old_version_id new_version_id edits state =
@@ -454,10 +478,10 @@
(fn () =>
let
val imports = map (apsnd Future.join) deps;
- val changed_imports = exists (#4 o #1 o #2) imports;
+ val imports_changed = exists (#3 o #1 o #2) imports;
val node_required = is_required name;
in
- if changed_imports orelse AList.defined (op =) edits name orelse
+ if imports_changed orelse AList.defined (op =) edits name orelse
not (stable_entries node) orelse not (finished_theory node)
then
let
@@ -467,64 +491,49 @@
check_theory false name node andalso
forall (fn (name, (_, node)) => check_theory true name node) imports;
- val visible_commands = visible_commands node;
- val visible_command = Inttab.defined visible_commands;
- val last_visible = visible_last node;
-
- val (common, (still_visible, initial)) =
- if changed_imports then (NONE, (true, true))
- else last_common state last_visible node0 node;
+ val (print_execs, common, (still_visible, initial)) =
+ if imports_changed then (assign_update_empty, NONE, (true, true))
+ else last_common state node0 node;
val common_command_exec = the_default_entry node common;
- val (new_execs, (command_id', (eval', _)), _) =
- ([], common_command_exec, if initial then SOME init else NONE) |>
- (still_visible orelse node_required) ?
+ val (updated_execs, (command_id', (eval', _)), _) =
+ (print_execs, common_command_exec, if initial then SOME init else NONE)
+ |> (still_visible orelse node_required) ?
iterate_entries_after common
(fn ((prev, id), _) => fn res =>
- if not node_required andalso prev = last_visible then NONE
- else new_exec state proper_init (visible_command id) id res) node;
-
- val updated_execs =
- (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
- if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I
- else append (the_list (update_prints state node id)));
+ if not node_required andalso prev = visible_last node then NONE
+ else new_exec state proper_init (visible_command node id) id res) node;
- val no_execs =
- iterate_entries_after common
- (fn ((_, id0), exec0) => fn res =>
+ val assigned_execs =
+ (node0, updated_execs) |-> iterate_entries_after common
+ (fn ((_, command_id0), exec0) => fn res =>
if is_none exec0 then NONE
- else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs
- then SOME res
- else SOME (id0 :: res)) node0 [];
+ else if assign_update_defined updated_execs command_id0 then SOME res
+ else SOME (assign_update_new (command_id0, NONE) res));
val last_exec =
if command_id' = Document_ID.none then NONE else SOME command_id';
val result =
- if is_some (after_entry node last_exec) then NONE
+ if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
else SOME eval';
val node' = node
- |> fold reset_entry no_execs
- |> fold (fn (id, exec) => update_entry id (SOME exec)) updated_execs
- |> entries_stable (null updated_execs)
+ |> assign_update_apply assigned_execs
+ |> entries_stable (assign_update_null updated_execs)
|> set_result result;
- val updated_node =
- if null no_execs andalso null updated_execs then NONE
- else SOME (name, node');
- val changed_result = not (null no_execs) orelse not (null new_execs);
- in ((no_execs, updated_execs, updated_node, changed_result), node') end
- else (([], [], NONE, false), node)
+ val assigned_node =
+ if assign_update_null assigned_execs then NONE else SOME (name, node');
+ val result_changed = changed_result node0 node';
+ in
+ ((assign_update_result assigned_execs, assigned_node, result_changed), node')
+ end
+ else (([], NONE, false), node)
end))
|> Future.joins |> map #1);
- val command_execs =
- map (rpair []) (maps #1 updated) @
- map (fn (command_id, exec) => (command_id, Command.exec_ids exec)) (maps #2 updated);
- val updated_nodes = map_filter #3 updated;
-
val state' = state
- |> define_version new_version_id (fold put_node updated_nodes new_version);
- in (command_execs, state') end;
+ |> define_version new_version_id (fold put_node (map_filter #2 updated) new_version);
+ in (maps #1 updated, state') end;
end;
--- a/src/Pure/PIDE/document.scala Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/PIDE/document.scala Wed Jul 10 12:35:18 2013 +0200
@@ -275,7 +275,8 @@
result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
}
- type Assign = List[(Document_ID.Command, List[Document_ID.Exec])] // exec state assignment
+ type Assign_Update =
+ List[(Document_ID.Command, List[Document_ID.Exec])] // update of exec state assignment
object State
{
@@ -293,21 +294,21 @@
def check_finished: Assignment = { require(is_finished); this }
def unfinished: Assignment = new Assignment(command_execs, false)
- def assign(
- add_command_execs: List[(Document_ID.Command, List[Document_ID.Exec])]): Assignment =
+ def assign(update: Assign_Update): Assignment =
{
require(!is_finished)
val command_execs1 =
- (command_execs /: add_command_execs) {
- case (res, (command_id, Nil)) => res - command_id
- case (res, assign) => res + assign
+ (command_execs /: update) {
+ case (res, (command_id, exec_ids)) =>
+ if (exec_ids.isEmpty) res - command_id
+ else res + (command_id -> exec_ids)
}
new Assignment(command_execs1, true)
}
}
val init: State =
- State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
+ State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil)._2
}
final case class State private(
@@ -344,10 +345,9 @@
}
def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
- def the_read_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
- def the_exec_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
- def the_assignment(version: Version): State.Assignment =
- assignments.getOrElse(version.id, fail)
+ def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
+ def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
+ def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
@@ -363,28 +363,30 @@
}
}
- def assign(id: Document_ID.Version, command_execs: Assign = Nil): (List[Command], State) =
+ def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
{
val version = the_version(id)
+ def upd(exec_id: Document_ID.Exec, st: Command.State)
+ : Option[(Document_ID.Exec, Command.State)] =
+ if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
+
val (changed_commands, new_execs) =
- ((Nil: List[Command], execs) /: command_execs) {
- case ((commands1, execs1), (cmd_id, exec)) =>
- val st1 = the_read_state(cmd_id)
- val command = st1.command
- val st0 = command.empty_state
-
+ ((Nil: List[Command], execs) /: update) {
+ case ((commands1, execs1), (command_id, exec)) =>
+ val st = the_static_state(command_id)
+ val command = st.command
val commands2 = command :: commands1
val execs2 =
exec match {
case Nil => execs1
case eval_id :: print_ids =>
- execs1 + (eval_id -> execs.getOrElse(eval_id, st1)) ++
- print_ids.iterator.map(id => id -> execs.getOrElse(id, st0))
+ execs1 ++ upd(eval_id, st) ++
+ (for (id <- print_ids; up <- upd(id, command.empty_state)) yield up)
}
(commands2, execs2)
}
- val new_assignment = the_assignment(version).assign(command_execs)
+ val new_assignment = the_assignment(version).assign(update)
val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
(changed_commands, new_state)
@@ -436,10 +438,9 @@
(_, node) <- version.nodes.entries
command <- node.commands.iterator
} {
- val id = command.id
- if (!commands1.isDefinedAt(id))
- commands.get(id).foreach(st => commands1 += (id -> st))
- for (exec_id <- command_execs.getOrElse(id, Nil)) {
+ if (!commands1.isDefinedAt(command.id))
+ commands.get(command.id).foreach(st => commands1 += (command.id -> st))
+ for (exec_id <- command_execs.getOrElse(command.id, Nil)) {
if (!execs1.isDefinedAt(exec_id))
execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
}
@@ -452,14 +453,14 @@
require(is_assigned(version))
try {
the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
- .map(the_exec_state(_)) match {
+ .map(the_dynamic_state(_)) match {
case eval_state :: print_states => (eval_state /: print_states)(_ ++ _)
case Nil => fail
}
}
catch {
case _: State.Fail =>
- try { the_read_state(command.id) }
+ try { the_static_state(command.id) }
catch { case _: State.Fail => command.init_state }
}
}
--- a/src/Pure/PIDE/markup.ML Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/PIDE/markup.ML Wed Jul 10 12:35:18 2013 +0200
@@ -140,7 +140,7 @@
val padding_line: Properties.entry
val dialogN: string val dialog: serial -> string -> T
val functionN: string
- val assign_execs: Properties.T
+ val assign_update: Properties.T
val removed_versions: Properties.T
val protocol_handler: string -> Properties.T
val invoke_scala: string -> string -> Properties.T
@@ -459,7 +459,7 @@
val functionN = "function"
-val assign_execs = [(functionN, "assign_execs")];
+val assign_update = [(functionN, "assign_update")];
val removed_versions = [(functionN, "removed_versions")];
fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)];
--- a/src/Pure/PIDE/markup.scala Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/PIDE/markup.scala Wed Jul 10 12:35:18 2013 +0200
@@ -313,7 +313,7 @@
val FUNCTION = "function"
val Function = new Properties.String(FUNCTION)
- val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
+ val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
object Protocol_Handler
--- a/src/Pure/PIDE/protocol.ML Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Wed Jul 10 12:35:18 2013 +0200
@@ -50,7 +50,7 @@
val (assignment, state') = Document.update old_id new_id edits state;
val _ =
- Output.protocol_message Markup.assign_execs
+ Output.protocol_message Markup.assign_update
((new_id, assignment) |>
let open XML.Encode
in pair int (list (pair int (list int))) end
@@ -58,7 +58,9 @@
val _ = List.app Future.cancel_group (Goal.reset_futures ());
val _ = Isabelle_Process.reset_tracing ();
- val _ = Document.start_execution state';
+ val _ =
+ Event_Timer.request (Time.now () + seconds 0.02)
+ (fn () => Document.start_execution state');
in state' end));
val _ =
--- a/src/Pure/PIDE/protocol.scala Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Jul 10 12:35:18 2013 +0200
@@ -11,9 +11,9 @@
{
/* document editing */
- object Assign
+ object Assign_Update
{
- def unapply(text: String): Option[(Document_ID.Version, Document.Assign)] =
+ def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
try {
import XML.Decode._
val body = YXML.parse_body(text)
--- a/src/Pure/System/isabelle_process.ML Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Jul 10 12:35:18 2013 +0200
@@ -75,12 +75,12 @@
NONE => ()
| SOME id =>
let
- val (n, ok) =
+ val ok =
Synchronized.change_result tracing_messages (fn tab =>
let
val n = the_default 0 (Inttab.lookup tab id) + 1;
val ok = n <= Options.default_int "editor_tracing_messages";
- in ((n, ok), Inttab.update (id, n) tab) end);
+ in (ok, Inttab.update (id, n) tab) end);
in
if ok then ()
else
@@ -188,13 +188,16 @@
NONE => raise Runtime.TERMINATE
| SOME line => map (read_chunk channel) (space_explode "," line));
+fun worker_guest e =
+ Future.worker_guest "Isabelle_Process.loop" (Future.new_group NONE) e ();
+
in
fun loop channel =
let val continue =
(case read_command channel of
[] => (Output.error_msg "Isabelle process: no input"; true)
- | name :: args => (run_command name args; true))
+ | name :: args => (worker_guest (fn () => run_command name args); true))
handle Runtime.TERMINATE => false
| exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
in if continue then loop channel else () end;
@@ -238,8 +241,6 @@
Future.ML_statistics := true;
Multithreading.trace := Options.int options "threads_trace";
Multithreading.max_threads := Options.int options "threads";
- if Multithreading.max_threads_value () < 2
- then Multithreading.max_threads := 2 else ();
Goal.skip_proofs := Options.bool options "editor_skip_proofs";
Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
end);
--- a/src/Pure/System/session.scala Wed Jul 10 12:25:11 2013 +0200
+++ b/src/Pure/System/session.scala Wed Jul 10 12:35:18 2013 +0200
@@ -396,11 +396,11 @@
val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
accumulate(state_id, prover.get.xml_cache.elem(message))
- case Markup.Assign_Execs =>
+ case Markup.Assign_Update =>
XML.content(output.body) match {
- case Protocol.Assign(id, assign) =>
+ case Protocol.Assign_Update(id, update) =>
try {
- val cmds = global_state >>> (_.assign(id, assign))
+ val cmds = global_state >>> (_.assign(id, update))
delay_commands_changed.invoke(true, cmds)
}
catch { case _: Document.State.Fail => bad_output() }