src/Pure/PIDE/document.ML
changeset 47341 00f6279bb67a
parent 47340 9bbf7fd96bcd
child 47342 7828c7b3c143
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Apr 05 10:45:53 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Apr 05 11:58:46 2012 +0200
     1.3 @@ -62,8 +62,8 @@
     1.4  type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
     1.5  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
     1.6  
     1.7 -type exec = (Toplevel.state * unit lazy) lazy;  (*eval/print process*)
     1.8 -val no_exec = (no_id, Lazy.value (Toplevel.toplevel, Lazy.value ()));
     1.9 +type exec = (Toplevel.state * unit lazy) Command.memo;  (*eval/print process*)
    1.10 +val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
    1.11  
    1.12  abstype node = Node of
    1.13   {touched: bool,
    1.14 @@ -71,7 +71,7 @@
    1.15    perspective: perspective,
    1.16    entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
    1.17    last_exec: command_id option,  (*last command with exec state assignment*)
    1.18 -  result: Toplevel.state lazy}
    1.19 +  result: exec}
    1.20  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.21  with
    1.22  
    1.23 @@ -87,11 +87,10 @@
    1.24  
    1.25  val no_header = Exn.Exn (ERROR "Bad theory header");
    1.26  val no_perspective = make_perspective [];
    1.27 -val no_result = Lazy.value Toplevel.toplevel;
    1.28  
    1.29 -val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result);
    1.30 +val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec);
    1.31  val clear_node = map_node (fn (_, header, _, _, _, _) =>
    1.32 -  (false, header, no_perspective, Entries.empty, NONE, no_result));
    1.33 +  (false, header, no_perspective, Entries.empty, NONE, no_exec));
    1.34  
    1.35  
    1.36  (* basic components *)
    1.37 @@ -159,8 +158,8 @@
    1.38      NONE => err_undef "command entry" id
    1.39    | SOME (exec, _) => exec);
    1.40  
    1.41 -fun the_default_entry node (SOME id) = (id, (the_default no_exec (the_entry node id)))
    1.42 -  | the_default_entry _ NONE = (no_id, no_exec);
    1.43 +fun the_default_entry node (SOME id) = (id, (the_default (no_id, no_exec) (the_entry node id)))
    1.44 +  | the_default_entry _ NONE = (no_id, (no_id, no_exec));
    1.45  
    1.46  fun update_entry id exec =
    1.47    map_entries (Entries.update (id, exec));
    1.48 @@ -193,7 +192,7 @@
    1.49    fold (fn desc =>
    1.50        update_node desc
    1.51          (set_touched true #>
    1.52 -          desc <> name ? (map_entries (reset_after NONE) #> set_result no_result)))
    1.53 +          desc <> name ? (map_entries (reset_after NONE) #> set_result no_exec)))
    1.54      (Graph.all_succs nodes [name]) nodes;
    1.55  
    1.56  in
    1.57 @@ -338,8 +337,8 @@
    1.58            SOME thy => thy
    1.59          | NONE =>
    1.60              Toplevel.end_theory (Position.file_only import)
    1.61 -              (Lazy.force
    1.62 -                (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))));
    1.63 +              (fst (Exn.release (Command.memo_result
    1.64 +                (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))))));
    1.65    in Thy_Load.begin_theory master_dir header parents end;
    1.66  
    1.67  fun check_theory nodes name =
    1.68 @@ -363,6 +362,7 @@
    1.69            (case opt_exec of
    1.70              NONE => true
    1.71            | SOME (exec_id, exec) =>
    1.72 +              not (Command.memo_stable exec) orelse
    1.73                (case lookup_entry node0 id of
    1.74                  NONE => true
    1.75                | SOME (exec_id0, _) => exec_id <> exec_id0));
    1.76 @@ -395,8 +395,9 @@
    1.77              #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
    1.78              |> modify_init
    1.79              |> Toplevel.put_id exec_id'_string);
    1.80 -      val exec' =
    1.81 -        snd (snd command_exec) |> Lazy.map (fn (st, _) => Command.run_command (tr ()) st);
    1.82 +      val exec' = Command.memo (fn () =>
    1.83 +        let val (st, _) = Exn.release (Command.memo_result (snd (snd command_exec)));
    1.84 +        in Command.run_command (tr ()) st end);
    1.85        val command_exec' = (command_id', (exec_id', exec'));
    1.86      in SOME (command_exec' :: execs, command_exec', init') end;
    1.87  
    1.88 @@ -448,8 +449,8 @@
    1.89  
    1.90                      val last_exec = if command_id = no_id then NONE else SOME command_id;
    1.91                      val result =
    1.92 -                      if is_some (after_entry node last_exec) then no_result
    1.93 -                      else Lazy.map #1 exec;
    1.94 +                      if is_some (after_entry node last_exec) then no_exec
    1.95 +                      else exec;
    1.96  
    1.97                      val node' = node
    1.98                        |> fold reset_entry no_execs
    1.99 @@ -485,7 +486,7 @@
   1.100        fun force_exec _ _ NONE = ()
   1.101          | force_exec node command_id (SOME (_, exec)) =
   1.102              let
   1.103 -              val (_, print) = Lazy.force exec;
   1.104 +              val (_, print) = Exn.release (Command.memo_result exec);
   1.105                val _ =
   1.106                  if #1 (get_perspective node) command_id
   1.107                  then ignore (Lazy.future Future.default_params print)