src/Pure/PIDE/document.ML
changeset 38448 62d16c415019
parent 38421 6cfc6fce7bfb
child 38449 2eb6bad282b1
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 16 22:56:28 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 17 15:10:49 2010 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val new_id: unit -> id
     1.5    val parse_id: string -> id
     1.6    val print_id: id -> string
     1.7 -  type edit = string * ((command_id * command_id option) list) option
     1.8 +  type edit = string * ((command_id option * command_id option) list) option
     1.9    type state
    1.10    val init_state: state
    1.11    val define_command: command_id -> string -> state -> state
    1.12 @@ -55,82 +55,43 @@
    1.13  
    1.14  (** document structure **)
    1.15  
    1.16 -abstype entry = Entry of {next: command_id option, exec: exec_id option}
    1.17 -  and node = Node of entry Inttab.table  (*unique entries indexed by command_id, start with no_id*)
    1.18 +structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.19 +
    1.20 +abstype node = Node of exec_id option Entries.T  (*command entries with excecutions*)
    1.21    and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.22  with
    1.23  
    1.24 -
    1.25 -(* command entries *)
    1.26 -
    1.27 -fun make_entry next exec = Entry {next = next, exec = exec};
    1.28 -
    1.29 -fun the_entry (Node entries) (id: command_id) =
    1.30 -  (case Inttab.lookup entries id of
    1.31 -    NONE => err_undef "command entry" id
    1.32 -  | SOME (Entry entry) => entry);
    1.33 +val empty_node = Node Entries.empty;
    1.34 +val empty_version = Version Graph.empty;
    1.35  
    1.36 -fun put_entry (id: command_id, entry: entry) (Node entries) =
    1.37 -  Node (Inttab.update (id, entry) entries);
    1.38 -
    1.39 -fun put_entry_exec (id: command_id) exec node =
    1.40 -  let val {next, ...} = the_entry node id
    1.41 -  in put_entry (id, make_entry next exec) node end;
    1.42 -
    1.43 -fun reset_entry_exec id = put_entry_exec id NONE;
    1.44 -fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
    1.45 +fun fold_entries start f (Node entries) = Entries.fold start f entries;
    1.46 +fun first_entry start P (Node entries) = Entries.get_first start P entries;
    1.47  
    1.48  
    1.49 -(* iterate entries *)
    1.50 -
    1.51 -fun fold_entries id0 f (node as Node entries) =
    1.52 -  let
    1.53 -    fun apply NONE x = x
    1.54 -      | apply (SOME id) x =
    1.55 -          let val entry = the_entry node id
    1.56 -          in apply (#next entry) (f (id, entry) x) end;
    1.57 -  in if Inttab.defined entries id0 then apply (SOME id0) else I end;
    1.58 -
    1.59 -fun first_entry P node =
    1.60 -  let
    1.61 -    fun first _ NONE = NONE
    1.62 -      | first prev (SOME id) =
    1.63 -          let val entry = the_entry node id
    1.64 -          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
    1.65 -  in first NONE (SOME no_id) end;
    1.66 -
    1.67 -
    1.68 -(* modify entries *)
    1.69 -
    1.70 -fun insert_after (id: command_id) (id2: command_id) node =
    1.71 -  let val {next, exec} = the_entry node id in
    1.72 -    node
    1.73 -    |> put_entry (id, make_entry (SOME id2) exec)
    1.74 -    |> put_entry (id2, make_entry next NONE)
    1.75 -  end;
    1.76 -
    1.77 -fun delete_after (id: command_id) node =
    1.78 -  let val {next, exec} = the_entry node id in
    1.79 -    (case next of
    1.80 -      NONE => error ("No next entry to delete: " ^ print_id id)
    1.81 -    | SOME id2 =>
    1.82 -        node |>
    1.83 -          (case #next (the_entry node id2) of
    1.84 -            NONE => put_entry (id, make_entry NONE exec)
    1.85 -          | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
    1.86 -  end;
    1.87 -
    1.88 -
    1.89 -(* node edits *)
    1.90 +(* node edits and associated executions *)
    1.91  
    1.92  type edit =
    1.93 -  string *  (*node name*)
    1.94 -  ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
    1.95 +  string *
    1.96 +  (*NONE: remove node, SOME: insert/remove commands*)
    1.97 +  ((command_id option * command_id option) list) option;
    1.98 +
    1.99 +fun the_entry (Node entries) id =
   1.100 +  (case Entries.lookup entries id of
   1.101 +    NONE => err_undef "command entry" id
   1.102 +  | SOME entry => entry);
   1.103  
   1.104 -val empty_node = Node (Inttab.make [(no_id, make_entry NONE (SOME no_id))]);
   1.105 +fun update_entry (id, exec_id) (Node entries) =
   1.106 +  Node (Entries.update (id, SOME exec_id) entries);
   1.107  
   1.108 -fun edit_node (id, SOME id2) = insert_after id id2
   1.109 -  | edit_node (id, NONE) = delete_after id;
   1.110 +fun reset_after id entries =
   1.111 +  (case Entries.get_after entries id of
   1.112 +    NONE => entries
   1.113 +  | SOME next => Entries.update (next, NONE) entries);
   1.114 +
   1.115 +fun edit_node (hook, SOME id2) (Node entries) =
   1.116 +      Node (Entries.insert_after hook (id2, NONE) entries)
   1.117 +  | edit_node (hook, NONE) (Node entries) =
   1.118 +      Node (entries |> Entries.delete_after hook |> reset_after hook);
   1.119  
   1.120  
   1.121  (* version operations *)
   1.122 @@ -138,16 +99,15 @@
   1.123  fun nodes_of (Version nodes) = nodes;
   1.124  val node_names_of = Graph.keys o nodes_of;
   1.125  
   1.126 +fun get_node version name = Graph.get_node (nodes_of version) name
   1.127 +  handle Graph.UNDEF _ => empty_node;
   1.128 +
   1.129  fun edit_nodes (name, SOME edits) (Version nodes) =
   1.130        Version (nodes
   1.131          |> Graph.default_node (name, empty_node)
   1.132          |> Graph.map_node name (fold edit_node edits))
   1.133 -  | edit_nodes (name, NONE) (Version nodes) = Version (Graph.del_node name nodes);
   1.134 -
   1.135 -val empty_version = Version Graph.empty;
   1.136 -
   1.137 -fun the_node version name =
   1.138 -  Graph.get_node (nodes_of version) name handle Graph.UNDEF _ => empty_node;
   1.139 +  | edit_nodes (name, NONE) (Version nodes) =
   1.140 +      Version (Graph.del_node name nodes);  (* FIXME Graph.UNDEF !? *)
   1.141  
   1.142  fun put_node name node (Version nodes) =
   1.143    Version (Graph.map_node name (K node) nodes);  (* FIXME Graph.UNDEF !? *)
   1.144 @@ -173,8 +133,8 @@
   1.145  
   1.146  val init_state =
   1.147    make_state (Inttab.make [(no_id, empty_version)],
   1.148 -    Inttab.make [(no_id, Future.value Toplevel.empty)],
   1.149 -    Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],
   1.150 +    Inttab.make [(no_id, Future.value Toplevel.empty)],          (* FIXME no_id !?? *)
   1.151 +    Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],  (* FIXME no_id !?? *)
   1.152      []);
   1.153  
   1.154  
   1.155 @@ -238,10 +198,10 @@
   1.156  
   1.157  local
   1.158  
   1.159 -fun is_changed node' (id, {next = _, exec}) =
   1.160 +fun is_changed node' ((_, id), exec) =
   1.161    (case try (the_entry node') id of
   1.162      NONE => true
   1.163 -  | SOME {next = _, exec = exec'} => exec' <> exec);
   1.164 +  | SOME exec' => exec' <> exec);
   1.165  
   1.166  fun new_exec name (id: command_id) (exec_id, updates, state) =
   1.167    let
   1.168 @@ -266,15 +226,18 @@
   1.169      val new_version = fold edit_nodes edits old_version;
   1.170  
   1.171      fun update_node name (rev_updates, version, st) =
   1.172 -      let val node = the_node version name in
   1.173 -        (case first_entry (is_changed (the_node old_version name)) node of
   1.174 +      let val node = get_node version name in
   1.175 +        (case first_entry NONE (is_changed (get_node old_version name)) node of
   1.176            NONE => (rev_updates, version, st)
   1.177 -        | SOME (prev, id, _) =>
   1.178 +        | SOME ((prev, id), _) =>
   1.179              let
   1.180 -              val prev_exec = the (#exec (the_entry node (the prev)));
   1.181 +              val prev_exec =
   1.182 +                (case prev of
   1.183 +                  NONE => no_id
   1.184 +                | SOME prev_id => the_default no_id (the_entry node prev_id));
   1.185                val (_, rev_upds, st') =
   1.186 -                fold_entries id (new_exec name o #1) node (prev_exec, [], st);
   1.187 -              val node' = fold set_entry_exec rev_upds node;
   1.188 +                fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
   1.189 +              val node' = fold update_entry rev_upds node;
   1.190              in (rev_upds @ rev_updates, put_node name node' version, st') end)
   1.191        end;
   1.192  
   1.193 @@ -306,8 +269,8 @@
   1.194          node_names_of version |> map (fn name =>
   1.195            Future.fork_pri 1 (fn () =>
   1.196              (await_cancellation ();
   1.197 -              fold_entries no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
   1.198 -                (the_node version name) ())));
   1.199 +              fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
   1.200 +                (get_node version name) ())));
   1.201      in (versions, commands, execs, execution') end);
   1.202  
   1.203  end;