1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 15 14:54:36 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 15 16:38:42 2011 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    type edit = string * node_edit
     1.5    type state
     1.6    val init_state: state
     1.7 -  val get_theory: state -> version_id -> Position.T -> string -> theory
     1.8 +  val join_commands: state -> unit
     1.9    val cancel_execution: state -> unit -> unit
    1.10    val define_command: command_id -> string -> state -> state
    1.11    val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
    1.12 @@ -61,28 +61,29 @@
    1.13  abstype node = Node of
    1.14   {header: node_header,
    1.15    entries: exec_id option Entries.T,  (*command entries with excecutions*)
    1.16 -  last: exec_id}  (*last entry with main result*)
    1.17 +  result: Toplevel.state lazy}
    1.18  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.19  with
    1.20  
    1.21 -fun make_node (header, entries, last) =
    1.22 -  Node {header = header, entries = entries, last = last};
    1.23 +fun make_node (header, entries, result) =
    1.24 +  Node {header = header, entries = entries, result = result};
    1.25  
    1.26 -fun map_node f (Node {header, entries, last}) =
    1.27 -  make_node (f (header, entries, last));
    1.28 +fun map_node f (Node {header, entries, result}) =
    1.29 +  make_node (f (header, entries, result));
    1.30  
    1.31  fun get_header (Node {header, ...}) = header;
    1.32 -fun set_header header = map_node (fn (_, entries, last) => (header, entries, last));
    1.33 +fun set_header header = map_node (fn (_, entries, result) => (header, entries, result));
    1.34  
    1.35 -fun map_entries f (Node {header, entries, last}) = make_node (header, f entries, last);
    1.36 +fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result);
    1.37  fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
    1.38  fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
    1.39  
    1.40 -fun get_last (Node {last, ...}) = last;
    1.41 -fun set_last last = map_node (fn (header, entries, _) => (header, entries, last));
    1.42 +fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
    1.43 +fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
    1.44  
    1.45 -val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id);
    1.46 -val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, no_id));
    1.47 +val empty_exec = Lazy.value Toplevel.toplevel;
    1.48 +val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec);
    1.49 +val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
    1.50  
    1.51  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    1.52  fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
    1.53 @@ -143,7 +144,7 @@
    1.54                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes');
    1.55          in Graph.map_node name (set_header header') nodes'' end);
    1.56  
    1.57 -fun put_node name node (Version nodes) =
    1.58 +fun put_node (name, node) (Version nodes) =
    1.59    Version (nodes
    1.60      |> Graph.default_node (name, empty_node)
    1.61      |> Graph.map_node name (K node));
    1.62 @@ -170,7 +171,7 @@
    1.63  val init_state =
    1.64    make_state (Inttab.make [(no_id, empty_version)],
    1.65      Inttab.make [(no_id, Future.value Toplevel.empty)],
    1.66 -    Inttab.make [(no_id, Lazy.value Toplevel.toplevel)],
    1.67 +    Inttab.make [(no_id, empty_exec)],
    1.68      []);
    1.69  
    1.70  
    1.71 @@ -213,26 +214,17 @@
    1.72  
    1.73  (* command executions *)
    1.74  
    1.75 -fun define_exec (id: exec_id) exec =
    1.76 +fun define_exec (exec_id, exec) =
    1.77    map_state (fn (versions, commands, execs, execution) =>
    1.78 -    let val execs' = Inttab.update_new (id, exec) execs
    1.79 +    let val execs' = Inttab.update_new (exec_id, exec) execs
    1.80        handle Inttab.DUP dup => err_dup "command execution" dup
    1.81      in (versions, commands, execs', execution) end);
    1.82  
    1.83 -fun the_exec (State {execs, ...}) (id: exec_id) =
    1.84 -  (case Inttab.lookup execs id of
    1.85 -    NONE => err_undef "command execution" id
    1.86 +fun the_exec (State {execs, ...}) exec_id =
    1.87 +  (case Inttab.lookup execs exec_id of
    1.88 +    NONE => err_undef "command execution" exec_id
    1.89    | SOME exec => exec);
    1.90  
    1.91 -fun get_theory state version_id pos name =
    1.92 -  let
    1.93 -    val last = get_last (node_of (the_version state version_id) name);
    1.94 -    val st =
    1.95 -      (case Lazy.peek (the_exec state last) of
    1.96 -        SOME result => Exn.release result
    1.97 -      | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos));
    1.98 -  in Toplevel.end_theory pos st end;
    1.99 -
   1.100  
   1.101  (* document execution *)
   1.102  
   1.103 @@ -324,19 +316,16 @@
   1.104      NONE => true
   1.105    | SOME exec' => exec' <> exec);
   1.106  
   1.107 -fun new_exec node_info (id: command_id) (exec_id, updates, state) =
   1.108 +fun new_exec node_info (command, command_id) (assigns, execs, exec) =
   1.109    let
   1.110 -    val exec = the_exec state exec_id;
   1.111      val exec_id' = new_id ();
   1.112 -    val future_tr = the_command state id;
   1.113      val exec' =
   1.114        Lazy.lazy (fn () =>
   1.115          let
   1.116 -          val st = Lazy.force exec;
   1.117 -          val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
   1.118 -        in run_command node_info exec_tr st end);
   1.119 -    val state' = define_exec exec_id' exec' state;
   1.120 -  in (exec_id', (id, exec_id') :: updates, state') end;
   1.121 +          val tr = Toplevel.put_id (print_id exec_id') (Future.join command); (* FIXME Future.join_finished !? *)
   1.122 +          val st = Lazy.force exec;  (* FIXME Lazy.force_finished !? *)
   1.123 +        in run_command node_info tr st end);
   1.124 +  in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end;
   1.125  
   1.126  in
   1.127  
   1.128 @@ -346,32 +335,31 @@
   1.129      val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
   1.130      val new_version = fold edit_nodes edits old_version;
   1.131  
   1.132 -    fun update_node name (rev_updates, version, st) =
   1.133 -      let
   1.134 -        val node = node_of version name;
   1.135 -        val header = get_header node;
   1.136 -      in
   1.137 -        (case first_entry NONE (is_changed (node_of old_version name)) node of
   1.138 -          NONE => (rev_updates, version, st)
   1.139 -        | SOME ((prev, id), _) =>
   1.140 -            let
   1.141 -              val prev_exec =
   1.142 -                (case prev of
   1.143 -                  NONE => no_id
   1.144 -                | SOME prev_id => the_default no_id (the_entry node prev_id));
   1.145 -              val (last, rev_upds, st') =
   1.146 -                fold_entries (SOME id) (new_exec (name, header) o #2 o #1) node (prev_exec, [], st);
   1.147 -              val node' = node |> fold update_entry rev_upds |> set_last last;
   1.148 -            in (rev_upds @ rev_updates, put_node name node' version, st') end)
   1.149 -      end;
   1.150 +    (* FIXME futures *)
   1.151 +    val updates =
   1.152 +      nodes_of new_version |> Graph.schedule
   1.153 +        (fn _ => fn (name, node) =>
   1.154 +          (case first_entry NONE (is_changed (node_of old_version name)) node of
   1.155 +            NONE => (([], [], []), node)
   1.156 +          | SOME ((prev, id), _) =>
   1.157 +              let
   1.158 +                val prev_exec =
   1.159 +                  (case prev of
   1.160 +                    NONE => no_id
   1.161 +                  | SOME prev_id => the_default no_id (the_entry node prev_id));
   1.162 +                val (assigns, execs, result) =
   1.163 +                  fold_entries (SOME id)
   1.164 +                    (new_exec (name, get_header node) o `(the_command state) o #2 o #1)
   1.165 +                      node ([], [], the_exec state prev_exec);
   1.166 +                val node' = node |> fold update_entry assigns |> set_result result;
   1.167 +              in ((assigns, execs, [(name, node')]), node') end))
   1.168 +      |> map #1;
   1.169  
   1.170 -    (* FIXME Graph.schedule *)
   1.171 -    val (rev_updates, new_version', state') =
   1.172 -      fold update_node (node_names_of new_version) ([], new_version, state);
   1.173 -    val state'' = define_version new_id new_version' state';
   1.174 +    val state' = state
   1.175 +      |> fold (fold define_exec o #2) updates
   1.176 +      |> define_version new_id (fold (fold put_node o #3) updates new_version);
   1.177  
   1.178 -    val _ = join_commands state'';  (* FIXME async!? *)
   1.179 -  in (rev rev_updates, state'') end;
   1.180 +  in (maps #1 (rev updates), state') end;
   1.181  
   1.182  end;
   1.183  

     2.1 --- a/src/Pure/PIDE/isar_document.ML	Mon Aug 15 14:54:36 2011 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.ML	Mon Aug 15 16:38:42 2011 +0200
     2.3 @@ -33,6 +33,7 @@
     2.4        val await_cancellation = Document.cancel_execution state;
     2.5        val (updates, state') = Document.edit old_id new_id edits state;
     2.6        val _ = await_cancellation ();
     2.7 +      val _ = Document.join_commands state';
     2.8        val _ =
     2.9          Output.status (Markup.markup (Markup.assign new_id)
    2.10            (implode (map (Markup.markup_only o Markup.edit) updates)));