src/Pure/PIDE/document.ML
changeset 52570 26d84a0b9209
parent 52569 18dde2cf7aa7
child 52573 815461c835b9
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Jul 09 23:49:19 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 10 11:26:55 2013 +0200
     1.3 @@ -398,22 +398,6 @@
     1.4    is_some (Thy_Info.lookup_theory name) orelse
     1.5    can get_header node andalso (not full orelse is_some (get_result node));
     1.6  
     1.7 -fun check_prints prints (prints': Command.print list) =
     1.8 -  if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
     1.9 -  else SOME prints';
    1.10 -
    1.11 -fun update_prints command_visible command_name eval prints =
    1.12 -  if command_visible then
    1.13 -    let
    1.14 -      val new_prints = Command.print command_name eval;
    1.15 -      val prints' =
    1.16 -        new_prints |> map (fn new_print =>
    1.17 -          (case find_first (fn {name, ...} => name = #name new_print) prints of
    1.18 -            SOME print => if Command.stable_print print then print else new_print
    1.19 -          | NONE => new_print));
    1.20 -    in check_prints prints prints' end
    1.21 -  else check_prints prints (filter Command.stable_print prints);
    1.22 -
    1.23  fun last_common state node0 node =
    1.24    let
    1.25      fun update_flags prev (visible, initial) =
    1.26 @@ -444,7 +428,7 @@
    1.27                    val command_visible = visible_command node command_id;
    1.28                    val command_name = the_command_name state command_id;
    1.29                  in
    1.30 -                  (case update_prints command_visible command_name eval prints of
    1.31 +                  (case Command.print command_visible command_name eval prints of
    1.32                      SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
    1.33                    | NONE => I)
    1.34                  end
    1.35 @@ -470,13 +454,12 @@
    1.36        val (command_name, span) = the_command state command_id' ||> Lazy.force;
    1.37  
    1.38        val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
    1.39 -      val prints' = perhaps (update_prints command_visible command_name eval') [];
    1.40 +      val prints' = perhaps (Command.print command_visible command_name eval') [];
    1.41        val exec' = (eval', prints');
    1.42  
    1.43        val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    1.44        val init' = if Keyword.is_theory_begin command_name then NONE else init;
    1.45      in SOME (assign_update', (command_id', (eval', prints')), init') end;
    1.46 -
    1.47  in
    1.48  
    1.49  fun update old_version_id new_version_id edits state =