clarified Command.print: update old prints here;
authorwenzelm
Wed Jul 10 11:26:55 2013 +0200 (2013-07-10)
changeset 5257026d84a0b9209
parent 52569 18dde2cf7aa7
child 52571 344527354323
clarified Command.print: update old prints here;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
     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 =