# HG changeset patch # User wenzelm # Date 1373452518 -7200 # Node ID 17138170ed7fa15dfdbef07681e3025d6ed59873 # Parent 92ed2926596d91e689f397db94ad86186e290bc8# Parent 815461c835b9b49d2e77593130ec1c97b3272661 merged diff -r 92ed2926596d -r 17138170ed7f Admin/lib/Tools/makedist_bundle --- 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" < s \ (\i::nat=0..i=0..j \ Suc (\i::nat=0..i=0.. 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 diff -r 92ed2926596d -r 17138170ed7f src/Pure/Concurrent/task_queue.ML --- 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 diff -r 92ed2926596d -r 17138170ed7f src/Pure/General/linear_set.ML --- 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 []); diff -r 92ed2926596d -r 17138170ed7f src/Pure/Isar/toplevel.ML --- 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" diff -r 92ed2926596d -r 17138170ed7f src/Pure/PIDE/command.ML --- 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; diff -r 92ed2926596d -r 17138170ed7f src/Pure/PIDE/document.ML --- 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; diff -r 92ed2926596d -r 17138170ed7f src/Pure/PIDE/document.scala --- 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 } } } diff -r 92ed2926596d -r 17138170ed7f src/Pure/PIDE/markup.ML --- 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)]; diff -r 92ed2926596d -r 17138170ed7f src/Pure/PIDE/markup.scala --- 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 diff -r 92ed2926596d -r 17138170ed7f src/Pure/PIDE/protocol.ML --- 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 _ = diff -r 92ed2926596d -r 17138170ed7f src/Pure/PIDE/protocol.scala --- 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) diff -r 92ed2926596d -r 17138170ed7f src/Pure/System/isabelle_process.ML --- 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); diff -r 92ed2926596d -r 17138170ed7f src/Pure/System/session.scala --- 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() }