src/Pure/PIDE/document.ML
changeset 38418 9a7af64d71bb
parent 38414 49f1f657adc2
child 38419 f9dc924e54f8
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Aug 15 14:18:52 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Aug 15 18:41:23 2010 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Makarius
     1.5  
     1.6  Document as collection of named nodes, each consisting of an editable
     1.7 -list of commands.
     1.8 +list of commands, associated with asynchronous execution process.
     1.9  *)
    1.10  
    1.11  signature DOCUMENT =
    1.12 @@ -12,9 +12,15 @@
    1.13    type command_id = id
    1.14    type exec_id = id
    1.15    val no_id: id
    1.16 +  val create_id: unit -> id
    1.17    val parse_id: string -> id
    1.18    val print_id: id -> string
    1.19    type edit = string * ((command_id * command_id option) list) option
    1.20 +  type state
    1.21 +  val init_state: state
    1.22 +  val define_command: command_id -> string -> state -> state
    1.23 +  val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
    1.24 +  val execute: version_id -> state -> state
    1.25  end;
    1.26  
    1.27  structure Document: DOCUMENT =
    1.28 @@ -29,15 +35,273 @@
    1.29  
    1.30  val no_id = 0;
    1.31  
    1.32 +local
    1.33 +  val id_count = Synchronized.var "id" 0;
    1.34 +in
    1.35 +  fun create_id () =
    1.36 +    Synchronized.change_result id_count
    1.37 +      (fn i =>
    1.38 +        let val i' = i + 1
    1.39 +        in (i', i') end);
    1.40 +end;
    1.41 +
    1.42  val parse_id = Markup.parse_int;
    1.43  val print_id = Markup.print_int;
    1.44  
    1.45 +fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id);
    1.46 +fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
    1.47  
    1.48 -(* edits *)
    1.49 +
    1.50 +
    1.51 +(** document structure **)
    1.52 +
    1.53 +abstype entry = Entry of {next: command_id option, exec: exec_id option}
    1.54 +  and node = Node of entry Inttab.table  (*unique entries indexed by command_id, start with no_id*)
    1.55 +  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.56 +with
    1.57 +
    1.58 +
    1.59 +(* command entries *)
    1.60 +
    1.61 +fun make_entry next exec = Entry {next = next, exec = exec};
    1.62 +
    1.63 +fun the_entry (Node entries) (id: command_id) =
    1.64 +  (case Inttab.lookup entries id of
    1.65 +    NONE => err_undef "command entry" id
    1.66 +  | SOME (Entry entry) => entry);
    1.67 +
    1.68 +fun put_entry (id: command_id, entry: entry) (Node entries) =
    1.69 +  Node (Inttab.update (id, entry) entries);
    1.70 +
    1.71 +fun put_entry_exec (id: command_id) exec node =
    1.72 +  let val {next, ...} = the_entry node id
    1.73 +  in put_entry (id, make_entry next exec) node end;
    1.74 +
    1.75 +fun reset_entry_exec id = put_entry_exec id NONE;
    1.76 +fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
    1.77 +
    1.78 +
    1.79 +(* iterate entries *)
    1.80 +
    1.81 +fun fold_entries id0 f (node as Node entries) =
    1.82 +  let
    1.83 +    fun apply NONE x = x
    1.84 +      | apply (SOME id) x =
    1.85 +          let val entry = the_entry node id
    1.86 +          in apply (#next entry) (f (id, entry) x) end;
    1.87 +  in if Inttab.defined entries id0 then apply (SOME id0) else I end;
    1.88 +
    1.89 +fun first_entry P node =
    1.90 +  let
    1.91 +    fun first _ NONE = NONE
    1.92 +      | first prev (SOME id) =
    1.93 +          let val entry = the_entry node id
    1.94 +          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
    1.95 +  in first NONE (SOME no_id) end;
    1.96 +
    1.97 +
    1.98 +(* modify entries *)
    1.99 +
   1.100 +fun insert_after (id: command_id) (id2: command_id) node =
   1.101 +  let val {next, exec} = the_entry node id in
   1.102 +    node
   1.103 +    |> put_entry (id, make_entry (SOME id2) exec)
   1.104 +    |> put_entry (id2, make_entry next NONE)
   1.105 +  end;
   1.106 +
   1.107 +fun delete_after (id: command_id) node =
   1.108 +  let val {next, exec} = the_entry node id in
   1.109 +    (case next of
   1.110 +      NONE => error ("No next entry to delete: " ^ print_id id)
   1.111 +    | SOME id2 =>
   1.112 +        node |>
   1.113 +          (case #next (the_entry node id2) of
   1.114 +            NONE => put_entry (id, make_entry NONE exec)
   1.115 +          | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
   1.116 +  end;
   1.117 +
   1.118 +
   1.119 +(* node edits *)
   1.120  
   1.121  type edit =
   1.122    string *  (*node name*)
   1.123    ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
   1.124  
   1.125 +val empty_node = Node (Inttab.make [(no_id, make_entry NONE (SOME no_id))]);
   1.126 +
   1.127 +fun edit_node (id, SOME id2) = insert_after id id2
   1.128 +  | edit_node (id, NONE) = delete_after id;
   1.129 +
   1.130 +
   1.131 +(* version operations *)
   1.132 +
   1.133 +fun nodes_of (Version nodes) = nodes;
   1.134 +val node_names_of = Graph.keys o nodes_of;
   1.135 +
   1.136 +fun edit_nodes (name, SOME edits) (Version nodes) =
   1.137 +      Version (nodes
   1.138 +        |> Graph.default_node (name, empty_node)
   1.139 +        |> Graph.map_node name (fold edit_node edits))
   1.140 +  | edit_nodes (name, NONE) (Version nodes) = Version (Graph.del_node name nodes);
   1.141 +
   1.142 +val empty_version = Version Graph.empty;
   1.143 +
   1.144 +fun the_node version name =
   1.145 +  Graph.get_node (nodes_of version) name handle Graph.UNDEF _ => empty_node;
   1.146 +
   1.147 +fun put_node name node (Version nodes) =
   1.148 +  Version (Graph.map_node name (K node) nodes);  (* FIXME Graph.UNDEF !? *)
   1.149 +
   1.150  end;
   1.151  
   1.152 +
   1.153 +
   1.154 +(** global state -- document structure and execution process **)
   1.155 +
   1.156 +abstype state = State of
   1.157 + {versions: version Inttab.table,                   (*version_id -> document content*)
   1.158 +  commands: Toplevel.transition Inttab.table,       (*command_id -> transition function*)
   1.159 +  execs: Toplevel.state option lazy Inttab.table,   (*exec_id -> execution process*)
   1.160 +  execution: unit future list}                      (*global execution process*)
   1.161 +with
   1.162 +
   1.163 +fun make_state (versions, commands, execs, execution) =
   1.164 +  State {versions = versions, commands = commands, execs = execs, execution = execution};
   1.165 +
   1.166 +fun map_state f (State {versions, commands, execs, execution}) =
   1.167 +  make_state (f (versions, commands, execs, execution));
   1.168 +
   1.169 +val init_state =
   1.170 +  make_state (Inttab.make [(no_id, empty_version)],
   1.171 +    Inttab.make [(no_id, Toplevel.empty)],
   1.172 +    Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],
   1.173 +    []);
   1.174 +
   1.175 +
   1.176 +(* document versions *)
   1.177 +
   1.178 +fun define_version (id: version_id) version =
   1.179 +  map_state (fn (versions, commands, execs, execution) =>
   1.180 +    let val versions' = Inttab.update_new (id, version) versions
   1.181 +      handle Inttab.DUP dup => err_dup "document version" dup
   1.182 +    in (versions', commands, execs, execution) end);
   1.183 +
   1.184 +fun the_version (State {versions, ...}) (id: version_id) =
   1.185 +  (case Inttab.lookup versions id of
   1.186 +    NONE => err_undef "document version" id
   1.187 +  | SOME version => version);
   1.188 +
   1.189 +
   1.190 +(* commands *)
   1.191 +
   1.192 +fun define_command (id: command_id) text =
   1.193 +  map_state (fn (versions, commands, execs, execution) =>
   1.194 +    let
   1.195 +      val id_string = print_id id;
   1.196 +      val tr =
   1.197 +        Position.setmp_thread_data (Position.id_only id_string)
   1.198 +          (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ();
   1.199 +      val commands' =
   1.200 +        Inttab.update_new (id, Toplevel.put_id id_string tr) commands
   1.201 +          handle Inttab.DUP dup => err_dup "command" dup;
   1.202 +    in (versions, commands', execs, execution) end);
   1.203 +
   1.204 +fun the_command (State {commands, ...}) (id: command_id) =
   1.205 +  (case Inttab.lookup commands id of
   1.206 +    NONE => err_undef "command" id
   1.207 +  | SOME tr => tr);
   1.208 +
   1.209 +
   1.210 +(* command executions *)
   1.211 +
   1.212 +fun define_exec (id: exec_id) exec =
   1.213 +  map_state (fn (versions, commands, execs, execution) =>
   1.214 +    let val execs' = Inttab.update_new (id, exec) execs
   1.215 +      handle Inttab.DUP dup => err_dup "command execution" dup
   1.216 +    in (versions, commands, execs', execution) end);
   1.217 +
   1.218 +fun the_exec (State {execs, ...}) (id: exec_id) =
   1.219 +  (case Inttab.lookup execs id of
   1.220 +    NONE => err_undef "command execution" id
   1.221 +  | SOME exec => exec);
   1.222 +
   1.223 +end;
   1.224 +
   1.225 +
   1.226 +
   1.227 +(** editing **)
   1.228 +
   1.229 +(* edit *)
   1.230 +
   1.231 +local
   1.232 +
   1.233 +fun is_changed node' (id, {next = _, exec}) =
   1.234 +  (case try (the_entry node') id of
   1.235 +    NONE => true
   1.236 +  | SOME {next = _, exec = exec'} => exec' <> exec);
   1.237 +
   1.238 +fun new_exec name (id: command_id) (exec_id, updates, state) =
   1.239 +  let
   1.240 +    val exec = the_exec state exec_id;
   1.241 +    val exec_id' = create_id ();
   1.242 +    val tr = Toplevel.put_id (print_id exec_id') (the_command state id);
   1.243 +    val exec' =
   1.244 +      Lazy.lazy (fn () =>
   1.245 +        (case Lazy.force exec of
   1.246 +          NONE => NONE
   1.247 +        | SOME st => Toplevel.run_command name tr st));
   1.248 +    val state' = define_exec exec_id' exec' state;
   1.249 +  in (exec_id', (id, exec_id') :: updates, state') end;
   1.250 +
   1.251 +in
   1.252 +
   1.253 +fun edit (old_id: version_id) (new_id: version_id) edits state =
   1.254 +  let
   1.255 +    val old_version = the_version state old_id;
   1.256 +    val new_version = fold edit_nodes edits old_version;
   1.257 +
   1.258 +    fun update_node name (rev_updates, version, st) =
   1.259 +      let val node = the_node version name in
   1.260 +        (case first_entry (is_changed (the_node old_version name)) node of
   1.261 +          NONE => (rev_updates, version, st)
   1.262 +        | SOME (prev, id, _) =>
   1.263 +            let
   1.264 +              val prev_exec = the (#exec (the_entry node (the prev)));
   1.265 +              val (_, rev_upds, st') =
   1.266 +                fold_entries id (new_exec name o #1) node (prev_exec, [], st);
   1.267 +              val node' = fold set_entry_exec rev_upds node;
   1.268 +            in (rev_upds @ rev_updates, put_node name node' version, st') end)
   1.269 +      end;
   1.270 +
   1.271 +    (* FIXME proper node deps *)
   1.272 +    val (rev_updates, new_version', state') =
   1.273 +      fold update_node (node_names_of new_version) ([], new_version, state);
   1.274 +    val state'' = define_version new_id new_version' state';
   1.275 +  in (rev rev_updates, state'') end;
   1.276 +
   1.277 +end;
   1.278 +
   1.279 +
   1.280 +(* execute *)
   1.281 +
   1.282 +fun execute version_id state =
   1.283 +  state |> map_state (fn (versions, commands, execs, execution) =>
   1.284 +    let
   1.285 +      val version = the_version state version_id;
   1.286 +
   1.287 +      fun force_exec NONE = ()
   1.288 +        | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
   1.289 +
   1.290 +      val _ = List.app Future.cancel execution;
   1.291 +      fun await_cancellation () = uninterruptible (fn _ => Future.join_results) execution;
   1.292 +
   1.293 +      val execution' = (* FIXME proper node deps *)
   1.294 +        node_names_of version |> map (fn name =>
   1.295 +          Future.fork_pri 1 (fn () =>
   1.296 +            (await_cancellation ();
   1.297 +              fold_entries no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
   1.298 +                (the_node version name) ())));
   1.299 +    in (versions, commands, execs, execution') end);
   1.300 +
   1.301 +end;
   1.302 +