Command.memo including physical interrupts (unlike Lazy.lazy);
authorwenzelm
Thu Apr 05 11:58:46 2012 +0200 (2012-04-05)
changeset 4734100f6279bb67a
parent 47340 9bbf7fd96bcd
child 47342 7828c7b3c143
Command.memo including physical interrupts (unlike Lazy.lazy);
re-assign unstable exec, i.e. reset interrupted transaction;
node result as direct exec -- avoid potential interrupt instability of Lazy.map;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Thu Apr 05 10:45:53 2012 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Apr 05 11:58:46 2012 +0200
     1.3 @@ -7,13 +7,18 @@
     1.4  signature COMMAND =
     1.5  sig
     1.6    val parse_command: string -> string -> Token.T list
     1.7 +  type 'a memo
     1.8 +  val memo: (unit -> 'a) -> 'a memo
     1.9 +  val memo_value: 'a -> 'a memo
    1.10 +  val memo_result: 'a memo -> 'a Exn.result
    1.11 +  val memo_stable: 'a memo -> bool
    1.12    val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
    1.13  end;
    1.14  
    1.15  structure Command: COMMAND =
    1.16  struct
    1.17  
    1.18 -(* parse *)
    1.19 +(* parse command *)
    1.20  
    1.21  fun parse_command id text =
    1.22    Position.setmp_thread_data (Position.id_only id)
    1.23 @@ -24,7 +29,37 @@
    1.24        in toks end) ();
    1.25  
    1.26  
    1.27 -(* run *)
    1.28 +(* memo results *)
    1.29 +
    1.30 +datatype 'a expr =
    1.31 +  Expr of unit -> 'a |
    1.32 +  Result of 'a Exn.result;
    1.33 +
    1.34 +abstype 'a memo = Memo of 'a expr Synchronized.var
    1.35 +with
    1.36 +
    1.37 +fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
    1.38 +fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    1.39 +
    1.40 +fun memo_result (Memo v) =
    1.41 +  (case Synchronized.value v of
    1.42 +    Result res => res
    1.43 +  | _ =>
    1.44 +      Synchronized.guarded_access v
    1.45 +        (fn Result res => SOME (res, Result res)
    1.46 +          | Expr e =>
    1.47 +              let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
    1.48 +              in SOME (res, Result res) end));
    1.49 +
    1.50 +fun memo_stable (Memo v) =
    1.51 +  (case Synchronized.value v of
    1.52 +    Result (Exn.Exn exn) => not (Exn.is_interrupt exn)
    1.53 +  | _ => true);
    1.54 +
    1.55 +end;
    1.56 +
    1.57 +
    1.58 +(* run command *)
    1.59  
    1.60  local
    1.61  
     2.1 --- a/src/Pure/PIDE/document.ML	Thu Apr 05 10:45:53 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Apr 05 11:58:46 2012 +0200
     2.3 @@ -62,8 +62,8 @@
     2.4  type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
     2.5  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
     2.6  
     2.7 -type exec = (Toplevel.state * unit lazy) lazy;  (*eval/print process*)
     2.8 -val no_exec = (no_id, Lazy.value (Toplevel.toplevel, Lazy.value ()));
     2.9 +type exec = (Toplevel.state * unit lazy) Command.memo;  (*eval/print process*)
    2.10 +val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
    2.11  
    2.12  abstype node = Node of
    2.13   {touched: bool,
    2.14 @@ -71,7 +71,7 @@
    2.15    perspective: perspective,
    2.16    entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
    2.17    last_exec: command_id option,  (*last command with exec state assignment*)
    2.18 -  result: Toplevel.state lazy}
    2.19 +  result: exec}
    2.20  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    2.21  with
    2.22  
    2.23 @@ -87,11 +87,10 @@
    2.24  
    2.25  val no_header = Exn.Exn (ERROR "Bad theory header");
    2.26  val no_perspective = make_perspective [];
    2.27 -val no_result = Lazy.value Toplevel.toplevel;
    2.28  
    2.29 -val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result);
    2.30 +val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec);
    2.31  val clear_node = map_node (fn (_, header, _, _, _, _) =>
    2.32 -  (false, header, no_perspective, Entries.empty, NONE, no_result));
    2.33 +  (false, header, no_perspective, Entries.empty, NONE, no_exec));
    2.34  
    2.35  
    2.36  (* basic components *)
    2.37 @@ -159,8 +158,8 @@
    2.38      NONE => err_undef "command entry" id
    2.39    | SOME (exec, _) => exec);
    2.40  
    2.41 -fun the_default_entry node (SOME id) = (id, (the_default no_exec (the_entry node id)))
    2.42 -  | the_default_entry _ NONE = (no_id, no_exec);
    2.43 +fun the_default_entry node (SOME id) = (id, (the_default (no_id, no_exec) (the_entry node id)))
    2.44 +  | the_default_entry _ NONE = (no_id, (no_id, no_exec));
    2.45  
    2.46  fun update_entry id exec =
    2.47    map_entries (Entries.update (id, exec));
    2.48 @@ -193,7 +192,7 @@
    2.49    fold (fn desc =>
    2.50        update_node desc
    2.51          (set_touched true #>
    2.52 -          desc <> name ? (map_entries (reset_after NONE) #> set_result no_result)))
    2.53 +          desc <> name ? (map_entries (reset_after NONE) #> set_result no_exec)))
    2.54      (Graph.all_succs nodes [name]) nodes;
    2.55  
    2.56  in
    2.57 @@ -338,8 +337,8 @@
    2.58            SOME thy => thy
    2.59          | NONE =>
    2.60              Toplevel.end_theory (Position.file_only import)
    2.61 -              (Lazy.force
    2.62 -                (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))));
    2.63 +              (fst (Exn.release (Command.memo_result
    2.64 +                (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))))));
    2.65    in Thy_Load.begin_theory master_dir header parents end;
    2.66  
    2.67  fun check_theory nodes name =
    2.68 @@ -363,6 +362,7 @@
    2.69            (case opt_exec of
    2.70              NONE => true
    2.71            | SOME (exec_id, exec) =>
    2.72 +              not (Command.memo_stable exec) orelse
    2.73                (case lookup_entry node0 id of
    2.74                  NONE => true
    2.75                | SOME (exec_id0, _) => exec_id <> exec_id0));
    2.76 @@ -395,8 +395,9 @@
    2.77              #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
    2.78              |> modify_init
    2.79              |> Toplevel.put_id exec_id'_string);
    2.80 -      val exec' =
    2.81 -        snd (snd command_exec) |> Lazy.map (fn (st, _) => Command.run_command (tr ()) st);
    2.82 +      val exec' = Command.memo (fn () =>
    2.83 +        let val (st, _) = Exn.release (Command.memo_result (snd (snd command_exec)));
    2.84 +        in Command.run_command (tr ()) st end);
    2.85        val command_exec' = (command_id', (exec_id', exec'));
    2.86      in SOME (command_exec' :: execs, command_exec', init') end;
    2.87  
    2.88 @@ -448,8 +449,8 @@
    2.89  
    2.90                      val last_exec = if command_id = no_id then NONE else SOME command_id;
    2.91                      val result =
    2.92 -                      if is_some (after_entry node last_exec) then no_result
    2.93 -                      else Lazy.map #1 exec;
    2.94 +                      if is_some (after_entry node last_exec) then no_exec
    2.95 +                      else exec;
    2.96  
    2.97                      val node' = node
    2.98                        |> fold reset_entry no_execs
    2.99 @@ -485,7 +486,7 @@
   2.100        fun force_exec _ _ NONE = ()
   2.101          | force_exec node command_id (SOME (_, exec)) =
   2.102              let
   2.103 -              val (_, print) = Lazy.force exec;
   2.104 +              val (_, print) = Exn.release (Command.memo_result exec);
   2.105                val _ =
   2.106                  if #1 (get_perspective node) command_id
   2.107                  then ignore (Lazy.future Future.default_params print)