1.1 --- a/src/Pure/PIDE/command.ML Tue Jul 09 23:49:19 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Wed Jul 10 11:26:55 2013 +0200
1.3 @@ -16,7 +16,7 @@
1.4 val exec_ids: exec option -> Document_ID.exec list
1.5 val read: (unit -> theory) -> Token.T list -> Toplevel.transition
1.6 val eval: (unit -> theory) -> Token.T list -> eval -> eval
1.7 - val print: string -> eval -> print list
1.8 + val print: bool -> string -> eval -> print list -> print list option
1.9 type print_fn = Toplevel.transition -> Toplevel.state -> unit
1.10 val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
1.11 val execute: exec -> unit
1.12 @@ -94,6 +94,18 @@
1.13 | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints;
1.14
1.15
1.16 +(* stable results *)
1.17 +
1.18 +fun stable_goals exec_id =
1.19 + not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
1.20 +
1.21 +fun stable_eval ({exec_id, eval_process}: eval) =
1.22 + stable_goals exec_id andalso memo_stable eval_process;
1.23 +
1.24 +fun stable_print ({exec_id, print_process, ...}: print) =
1.25 + stable_goals exec_id andalso memo_stable print_process;
1.26 +
1.27 +
1.28 (* read *)
1.29
1.30 fun read init span =
1.31 @@ -200,37 +212,46 @@
1.32 type print_function = string * (int * (string -> print_fn option));
1.33 val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
1.34
1.35 -fun output_error tr exn =
1.36 - List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
1.37 -
1.38 -fun print_error tr f x =
1.39 - (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) f x
1.40 - handle exn => output_error tr exn;
1.41 +fun print_error tr e =
1.42 + (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
1.43 + List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
1.44
1.45 in
1.46
1.47 -fun print command_name eval =
1.48 - rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
1.49 - (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
1.50 - Exn.Res NONE => NONE
1.51 - | Exn.Res (SOME print_fn) =>
1.52 - let
1.53 - val exec_id = Document_ID.make ();
1.54 - fun process () =
1.55 - let
1.56 - val {failed, command, state = st', ...} = eval_result eval;
1.57 - val tr = Toplevel.exec_id exec_id command;
1.58 - in if failed then () else print_error tr (fn () => print_fn tr st') () end;
1.59 - in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
1.60 - | Exn.Exn exn =>
1.61 - let
1.62 - val exec_id = Document_ID.make ();
1.63 - fun process () =
1.64 - let
1.65 - val {command, ...} = eval_result eval;
1.66 - val tr = Toplevel.exec_id exec_id command;
1.67 - in output_error tr exn end;
1.68 - in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
1.69 +fun print command_visible command_name eval old_prints =
1.70 + let
1.71 + fun new_print (name, (pri, get_print_fn)) =
1.72 + let
1.73 + fun make_print strict print_fn =
1.74 + let
1.75 + val exec_id = Document_ID.make ();
1.76 + fun process () =
1.77 + let
1.78 + val {failed, command, state = st', ...} = eval_result eval;
1.79 + val tr = Toplevel.exec_id exec_id command;
1.80 + in
1.81 + if failed andalso not strict then ()
1.82 + else print_error tr (fn () => print_fn tr st')
1.83 + end;
1.84 + in {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end;
1.85 + in
1.86 + (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
1.87 + Exn.Res NONE => NONE
1.88 + | Exn.Res (SOME print_fn) => SOME (make_print false print_fn)
1.89 + | Exn.Exn exn => SOME (make_print true (fn _ => fn _ => reraise exn)))
1.90 + end;
1.91 +
1.92 + val new_prints =
1.93 + if command_visible then
1.94 + rev (Synchronized.value print_functions) |> map_filter (fn pr =>
1.95 + (case find_first (equal (fst pr) o #name) old_prints of
1.96 + SOME print => if stable_print print then SOME print else new_print pr
1.97 + | NONE => new_print pr))
1.98 + else filter stable_print old_prints;
1.99 + in
1.100 + if eq_list (op = o pairself #exec_id) (old_prints, new_prints) then NONE
1.101 + else SOME new_prints
1.102 + end;
1.103
1.104 fun print_function {name, pri} f =
1.105 Synchronized.change print_functions (fn funs =>
1.106 @@ -261,14 +282,5 @@
1.107 fun execute (({eval_process, ...}, prints): exec) =
1.108 (memo_eval eval_process; List.app run_print prints);
1.109
1.110 -fun stable_goals exec_id =
1.111 - not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
1.112 -
1.113 -fun stable_eval ({exec_id, eval_process}: eval) =
1.114 - stable_goals exec_id andalso memo_stable eval_process;
1.115 -
1.116 -fun stable_print ({exec_id, print_process, ...}: print) =
1.117 - stable_goals exec_id andalso memo_stable print_process;
1.118 -
1.119 end;
1.120
2.1 --- a/src/Pure/PIDE/document.ML Tue Jul 09 23:49:19 2013 +0200
2.2 +++ b/src/Pure/PIDE/document.ML Wed Jul 10 11:26:55 2013 +0200
2.3 @@ -398,22 +398,6 @@
2.4 is_some (Thy_Info.lookup_theory name) orelse
2.5 can get_header node andalso (not full orelse is_some (get_result node));
2.6
2.7 -fun check_prints prints (prints': Command.print list) =
2.8 - if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
2.9 - else SOME prints';
2.10 -
2.11 -fun update_prints command_visible command_name eval prints =
2.12 - if command_visible then
2.13 - let
2.14 - val new_prints = Command.print command_name eval;
2.15 - val prints' =
2.16 - new_prints |> map (fn new_print =>
2.17 - (case find_first (fn {name, ...} => name = #name new_print) prints of
2.18 - SOME print => if Command.stable_print print then print else new_print
2.19 - | NONE => new_print));
2.20 - in check_prints prints prints' end
2.21 - else check_prints prints (filter Command.stable_print prints);
2.22 -
2.23 fun last_common state node0 node =
2.24 let
2.25 fun update_flags prev (visible, initial) =
2.26 @@ -444,7 +428,7 @@
2.27 val command_visible = visible_command node command_id;
2.28 val command_name = the_command_name state command_id;
2.29 in
2.30 - (case update_prints command_visible command_name eval prints of
2.31 + (case Command.print command_visible command_name eval prints of
2.32 SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
2.33 | NONE => I)
2.34 end
2.35 @@ -470,13 +454,12 @@
2.36 val (command_name, span) = the_command state command_id' ||> Lazy.force;
2.37
2.38 val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
2.39 - val prints' = perhaps (update_prints command_visible command_name eval') [];
2.40 + val prints' = perhaps (Command.print command_visible command_name eval') [];
2.41 val exec' = (eval', prints');
2.42
2.43 val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
2.44 val init' = if Keyword.is_theory_begin command_name then NONE else init;
2.45 in SOME (assign_update', (command_id', (eval', prints')), init') end;
2.46 -
2.47 in
2.48
2.49 fun update old_version_id new_version_id edits state =