src/Pure/PIDE/document.ML

     Header of node_header |
     Perspective of command_id list
   type edit = string * node_edit
   type state
   val init_state: state
+  val define_command: command_id -> string -> state -> state
   val join_commands: state -> unit
   val cancel_execution: state -> Future.task list
-  val define_command: command_id -> string -> state -> state
   val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
   val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   val execute: version_id -> state -> state
   val state: unit -> state
   val change_state: (state -> state) -> unit

   Node {header = header, perspective = perspective, entries = entries, result = result};
 
 fun map_node f (Node {header, perspective, entries, result}) =
   make_node (f (header, perspective, entries, result));
 
-val no_perspective: perspective = (K false, []);
+fun make_perspective ids : perspective =
+  (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids);
+
+val no_perspective = make_perspective [];
 val no_print = Lazy.value ();
 val no_result = Lazy.value Toplevel.toplevel;
 
 val empty_node =
   make_node (Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);

 fun get_header (Node {header, ...}) = header;
 fun set_header header =
   map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
 
 fun get_perspective (Node {perspective, ...}) = perspective;
-fun set_perspective perspective =
-  let val pred = Inttab.defined (Inttab.make (map (rpair ()) perspective)) in
-    map_node (fn (header, _, entries, result) => (header, (pred, perspective), entries, result))
-  end;
+fun set_perspective ids =
+  map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
 
 fun map_entries f (Node {header, perspective, entries, result}) =
   make_node (header, perspective, f entries, result);
 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;

 fun is_changed node' ((_, id), exec) =
   (case try (the_entry node') id of
     NONE => true
   | SOME exec' => exec' <> exec);
 
-fun init_theory deps (name, node) =
+fun init_theory deps name node =
   let
     val (thy_name, imports, uses) = Exn.release (get_header node);
     (* FIXME provide files via Scala layer *)
     val (dir, files) =
       if ML_System.platform_is_cygwin then (Path.current, [])
       else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
 
     val parents =
       imports |> map (fn import =>
-        (case Thy_Info.lookup_theory import of
+        (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
           SOME thy => thy
         | NONE =>
             get_theory (Position.file_only import)
               (#2 (Future.join (the (AList.lookup (op =) deps import))))));
   in Thy_Load.begin_theory dir thy_name imports files parents end;
 
-fun new_exec (command_id, command) (assigns, execs, exec) =
+fun new_exec state init command_id (assigns, execs, exec) =
   let
+    val command = the_command state command_id;
     val exec_id' = new_id ();
     val exec' = exec |> Lazy.map (fn (st, _) =>
-      let val tr = Toplevel.put_id (print_id exec_id') (Future.join command)
+      let val tr =
+        Future.join command
+        |> Toplevel.modify_init init
+        |> Toplevel.put_id (print_id exec_id');
       in run_command tr st end);
   in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end;
 
 in
 

         (fn deps => fn (name, node) =>
           (case first_entry NONE (is_changed (node_of old_version name)) node of
             NONE => Future.value (([], [], []), node)
           | SOME ((prev, id), _) =>
               let
-                fun init () = init_theory deps (name, node);
-                fun get_command id =
-                  (id, the_command state id |> Future.map (Toplevel.modify_init init));
+                fun init () = init_theory deps name node;
               in
                 (singleton o Future.forks)
                   {name = "Document.edit", group = NONE,
                     deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
                   (fn () =>

                       val prev_exec =
                         (case prev of
                           NONE => no_id
                         | SOME prev_id => the_default no_id (the_entry node prev_id));
                       val (assigns, execs, last_exec) =
-                        fold_entries (SOME id) (new_exec o get_command o #2 o #1)
+                        fold_entries (SOME id) (new_exec state init o #2 o #1)
                           node ([], [], #2 (the_exec state prev_exec));
                       val node' = node
                         |> fold update_entry assigns
                         |> set_result (Lazy.map #1 last_exec);
                     in ((assigns, execs, [(name, node')]), node') end)