# HG changeset patch # User wenzelm # Date 1373036968 -7200 # Node ID a95440dcd59c0a8ff3aa1ddf03de2be41deebf31 # Parent c81d76f7f63dda7b3121629e57e5bd2a565ead3d clarified type Command.eval; diff -r c81d76f7f63d -r a95440dcd59c src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Fri Jul 05 16:22:28 2013 +0200 +++ b/src/Pure/PIDE/command.ML Fri Jul 05 17:09:28 2013 +0200 @@ -19,19 +19,20 @@ val read: span -> Toplevel.transition type eval_state = {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state} - type eval = eval_state memo + type eval = {exec_id: Document_ID.exec, eval: eval_state memo} val no_eval: eval + val eval_result: eval -> eval_state val eval: span -> Toplevel.transition -> eval_state -> eval_state type print_fn = Toplevel.transition -> Toplevel.state -> unit type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo} val print: string -> eval -> print list val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit - type exec = Document_ID.exec * (eval * print list) + type exec = eval * print list val no_exec: exec val exec_ids: exec -> Document_ID.exec list val exec_result: exec -> eval_state val exec_run: exec -> unit - val stable_eval: exec -> bool + val stable_eval: eval -> bool val stable_print: print -> bool end; @@ -125,8 +126,10 @@ val no_eval_state: eval_state = {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel}; -type eval = eval_state memo; -val no_eval = memo_value no_eval_state; +type eval = {exec_id: Document_ID.exec, eval: eval_state memo}; + +val no_eval: eval = {exec_id = Document_ID.none, eval = memo_value no_eval_state}; +fun eval_result ({eval, ...}: eval) = memo_result eval; local @@ -210,7 +213,7 @@ val exec_id = Document_ID.make (); fun body () = let - val {failed, command, state = st', ...} = memo_result eval; + val {failed, command, state = st', ...} = eval_result eval; val tr = Toplevel.put_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 = memo body} end @@ -219,7 +222,7 @@ val exec_id = Document_ID.make (); fun body () = let - val {command, ...} = memo_result eval; + val {command, ...} = eval_result eval; val tr = Toplevel.put_id exec_id command; in output_error tr exn end; in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end)); @@ -244,29 +247,29 @@ -(** managed evaluation with potential interrupts **) +(** managed evaluation **) (* execution *) -type exec = Document_ID.exec * (eval * print list); -val no_exec: exec = (Document_ID.none, (no_eval, [])); +type exec = eval * print list; +val no_exec: exec = (no_eval, []); -fun exec_ids ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints; +fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints; -fun exec_result ((_, (eval, _)): exec) = memo_result eval; +fun exec_result (({eval, ...}, _): exec) = memo_result eval; -fun exec_run ((_, (eval, prints)): exec) = +fun exec_run (({eval, ...}, prints): exec) = (memo_eval eval; prints |> List.app (fn {name, pri, print, ...} => memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print)); -(* stable situations *) +(* stable situations after cancellation *) fun stable_goals exec_id = not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))); -fun stable_eval ((exec_id, (eval, _)): exec) = +fun stable_eval ({exec_id, eval}: eval) = stable_goals exec_id andalso memo_stable eval; fun stable_print ({exec_id, print, ...}: print) = diff -r c81d76f7f63d -r a95440dcd59c src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Jul 05 16:22:28 2013 +0200 +++ b/src/Pure/PIDE/document.ML Fri Jul 05 17:09:28 2013 +0200 @@ -108,6 +108,11 @@ fun set_result result = map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); +fun finished_theory node = + (case Exn.capture (Command.eval_result o the) (get_result node) of + Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st + | _ => false); + fun get_node nodes name = String_Graph.get_node nodes name handle String_Graph.UNDEF _ => empty_node; fun default_node name = String_Graph.default_node (name, empty_node); @@ -275,12 +280,6 @@ in (versions', commands', execution) end); -fun finished_theory node = - (case Exn.capture (Command.memo_result o the) (get_result node) of - Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st - | _ => false); - - (** document execution **) @@ -349,7 +348,7 @@ | NONE => Toplevel.end_theory (Position.file_only import) (#state - (Command.memo_result + (Command.eval_result (the_default Command.no_eval (get_result (snd (the (AList.lookup (op =) deps import))))))))); val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); @@ -376,11 +375,11 @@ val same' = (case opt_exec of NONE => false - | SOME (exec_id, exec) => + | SOME (eval, _) => (case lookup_entry node0 id of NONE => false - | SOME (exec_id0, _) => - exec_id = exec_id0 andalso Command.stable_eval (exec_id, exec))); + | SOME (eval0, _) => + #exec_id eval = #exec_id eval0 andalso Command.stable_eval eval)); in SOME (same', (prev, flags')) end else NONE; val (same, (common, flags)) = @@ -405,7 +404,7 @@ else (I, init); val exec_id' = Document_ID.make (); - val eval' = + val eval_body' = Command.memo (fn () => let val eval_state = Command.exec_result (snd command_exec); @@ -416,13 +415,14 @@ |> modify_init |> Toplevel.put_id exec_id') (); in Command.eval span tr eval_state end); + val eval' = {exec_id = exec_id', eval = eval_body'}; val prints' = if command_visible then Command.print command_name eval' else []; - val command_exec' = (command_id', (exec_id', (eval', prints'))); + 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 (exec_id, (eval, prints)) => + SOME (eval, prints) => let val (command_name, _) = the_command state command_id; val new_prints = Command.print command_name eval; @@ -433,7 +433,7 @@ | NONE => new_print)); in if eq_list (op = o pairself #exec_id) (prints, prints') then NONE - else SOME (command_id, (exec_id, (eval, prints'))) + else SOME (command_id, (eval, prints')) end | NONE => NONE); @@ -479,7 +479,7 @@ else last_common state last_visible node0 node; val common_command_exec = the_default_entry node common; - val (new_execs, (command_id', (_, (eval', _))), _) = + val (new_execs, (command_id', (eval', _)), _) = ([], common_command_exec, if initial then SOME init else NONE) |> (still_visible orelse node_required) ? iterate_entries_after common @@ -489,14 +489,14 @@ val updated_execs = (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) => - if exists (fn (_, (id', _)) => id = id') new_execs then I + if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I else append (the_list (update_prints state node id))); val no_execs = iterate_entries_after common (fn ((_, id0), exec0) => fn res => if is_none exec0 then NONE - else if exists (fn (_, (id, _)) => id0 = id) updated_execs + else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs then SOME res else SOME (id0 :: res)) node0 [];