# HG changeset patch # User wenzelm # Date 1373448415 -7200 # Node ID 26d84a0b92090824c18870d5c11b45a003ef4b39 # Parent 18dde2cf7aa76fb6d95d4450acf3efcad8a1bb69 clarified Command.print: update old prints here; diff -r 18dde2cf7aa7 -r 26d84a0b9209 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Tue Jul 09 23:49:19 2013 +0200 +++ b/src/Pure/PIDE/command.ML Wed Jul 10 11:26:55 2013 +0200 @@ -16,7 +16,7 @@ val exec_ids: exec option -> Document_ID.exec list 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 execute: exec -> unit @@ -94,6 +94,18 @@ | 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 *) fun read init span = @@ -200,37 +212,46 @@ type print_function = string * (int * (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, get_print_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, exec_id = exec_id, print_process = memo process} end; + in + (case Exn.capture (Runtime.controlled_execution get_print_fn) 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; + + 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 stable_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} f = Synchronized.change print_functions (fn funs => @@ -261,14 +282,5 @@ fun execute (({eval_process, ...}, prints): exec) = (memo_eval eval_process; List.app run_print prints); -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; - end; diff -r 18dde2cf7aa7 -r 26d84a0b9209 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Jul 09 23:49:19 2013 +0200 +++ b/src/Pure/PIDE/document.ML Wed Jul 10 11:26:55 2013 +0200 @@ -398,22 +398,6 @@ is_some (Thy_Info.lookup_theory name) orelse can get_header node andalso (not full orelse is_some (get_result node)); -fun check_prints prints (prints': Command.print list) = - if eq_list (op = o pairself #exec_id) (prints, prints') then NONE - else SOME prints'; - -fun update_prints command_visible command_name eval prints = - if command_visible then - let - 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 check_prints prints prints' end - else check_prints prints (filter Command.stable_print prints); - fun last_common state node0 node = let fun update_flags prev (visible, initial) = @@ -444,7 +428,7 @@ val command_visible = visible_command node command_id; val command_name = the_command_name state command_id; in - (case update_prints command_visible command_name eval prints of + (case Command.print command_visible command_name eval prints of SOME prints' => assign_update_new (command_id, SOME (eval, prints')) | NONE => I) end @@ -470,13 +454,12 @@ val (command_name, span) = the_command state command_id' ||> Lazy.force; val eval' = Command.eval (fn () => the_default illegal_init init span) span eval; - val prints' = perhaps (update_prints command_visible command_name 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 =