more explicit / functional ML version of document model;
authorwenzelm
Sun Aug 15 18:41:23 2010 +0200 (2010-08-15 ago)
changeset 384189a7af64d71bb
parent 38417 b8922ae21111
child 38419 f9dc924e54f8
more explicit / functional ML version of document model;
tuned;
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/ROOT.ML
src/Pure/System/isar_document.ML
src/Pure/System/isar_document.scala
     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 +
     2.1 --- a/src/Pure/PIDE/document.scala	Sun Aug 15 14:18:52 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sun Aug 15 18:41:23 2010 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4      Author:     Makarius
     2.5  
     2.6  Document as collection of named nodes, each consisting of an editable
     2.7 -list of commands.
     2.8 +list of commands, associated with asynchronous execution process.
     2.9  */
    2.10  
    2.11  package isabelle
    2.12 @@ -124,7 +124,7 @@
    2.13  
    2.14  
    2.15  
    2.16 -  /** global state -- accumulated prover results **/
    2.17 +  /** global state -- document structure and execution process **/
    2.18  
    2.19    object State
    2.20    {
     3.1 --- a/src/Pure/ROOT.ML	Sun Aug 15 14:18:52 2010 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Sun Aug 15 18:41:23 2010 +0200
     3.3 @@ -236,9 +236,9 @@
     3.4  use "Thy/term_style.ML";
     3.5  use "Thy/thy_output.ML";
     3.6  use "Thy/thy_syntax.ML";
     3.7 -use "PIDE/document.ML";
     3.8  use "old_goals.ML";
     3.9  use "Isar/outer_syntax.ML";
    3.10 +use "PIDE/document.ML";
    3.11  use "Thy/thy_info.ML";
    3.12  
    3.13  (*theory and proof operations*)
     4.1 --- a/src/Pure/System/isar_document.ML	Sun Aug 15 14:18:52 2010 +0200
     4.2 +++ b/src/Pure/System/isar_document.ML	Sun Aug 15 18:41:23 2010 +0200
     4.3 @@ -1,295 +1,52 @@
     4.4  (*  Title:      Pure/System/isar_document.ML
     4.5      Author:     Makarius
     4.6  
     4.7 -Interactive Isar documents, which are structured as follows:
     4.8 -
     4.9 -  - history: tree of documents (i.e. changes without merge)
    4.10 -  - document: graph of nodes (cf. theory files)
    4.11 -  - node: linear set of commands, potentially with proof structure
    4.12 +Protocol commands for interactive Isar documents.
    4.13  *)
    4.14  
    4.15  structure Isar_Document: sig end =
    4.16  struct
    4.17  
    4.18 -(* unique identifiers *)
    4.19 -
    4.20 -local
    4.21 -  val id_count = Synchronized.var "id" 0;
    4.22 -in
    4.23 -  fun create_id () =
    4.24 -    Synchronized.change_result id_count
    4.25 -      (fn i =>
    4.26 -        let val i' = i + 1
    4.27 -        in (i', i') end);
    4.28 -end;
    4.29 -
    4.30 -fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id);
    4.31 -fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
    4.32 -
    4.33 -
    4.34 -(** document versions **)
    4.35 -
    4.36 -datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
    4.37 -type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
    4.38 -type version = node Graph.T;   (*development graph via static imports*)
    4.39 -
    4.40 -
    4.41 -(* command entries *)
    4.42 -
    4.43 -fun make_entry next exec = Entry {next = next, exec = exec};
    4.44 +(* global document state *)
    4.45  
    4.46 -fun the_entry (node: node) (id: Document.command_id) =
    4.47 -  (case Inttab.lookup node id of
    4.48 -    NONE => err_undef "command entry" id
    4.49 -  | SOME (Entry entry) => entry);
    4.50 -
    4.51 -fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
    4.52 -
    4.53 -fun put_entry_exec (id: Document.command_id) exec (node: node) =
    4.54 -  let val {next, ...} = the_entry node id
    4.55 -  in put_entry (id, make_entry next exec) node end;
    4.56 -
    4.57 -fun reset_entry_exec id = put_entry_exec id NONE;
    4.58 -fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
    4.59 -
    4.60 -
    4.61 -(* iterate entries *)
    4.62 -
    4.63 -fun fold_entries id0 f (node: node) =
    4.64 -  let
    4.65 -    fun apply NONE x = x
    4.66 -      | apply (SOME id) x =
    4.67 -          let val entry = the_entry node id
    4.68 -          in apply (#next entry) (f (id, entry) x) end;
    4.69 -  in if Inttab.defined node id0 then apply (SOME id0) else I end;
    4.70 -
    4.71 -fun first_entry P (node: node) =
    4.72 -  let
    4.73 -    fun first _ NONE = NONE
    4.74 -      | first prev (SOME id) =
    4.75 -          let val entry = the_entry node id
    4.76 -          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
    4.77 -  in first NONE (SOME Document.no_id) end;
    4.78 +local val global_state = Unsynchronized.ref Document.init_state in
    4.79  
    4.80 -
    4.81 -(* modify entries *)
    4.82 -
    4.83 -fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
    4.84 -  let val {next, exec} = the_entry node id in
    4.85 -    node
    4.86 -    |> put_entry (id, make_entry (SOME id2) exec)
    4.87 -    |> put_entry (id2, make_entry next NONE)
    4.88 -  end;
    4.89 -
    4.90 -fun delete_after (id: Document.command_id) (node: node) =
    4.91 -  let val {next, exec} = the_entry node id in
    4.92 -    (case next of
    4.93 -      NONE => error ("No next entry to delete: " ^ Document.print_id id)
    4.94 -    | SOME id2 =>
    4.95 -        node |>
    4.96 -          (case #next (the_entry node id2) of
    4.97 -            NONE => put_entry (id, make_entry NONE exec)
    4.98 -          | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
    4.99 -  end;
   4.100 -
   4.101 -
   4.102 -(* node operations *)
   4.103 -
   4.104 -val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
   4.105 -
   4.106 -fun the_node (version: version) name =
   4.107 -  Graph.get_node version name handle Graph.UNDEF _ => empty_node;
   4.108 +fun change_state f =
   4.109 +  NAMED_CRITICAL "Isar_Document" (fn () => Unsynchronized.change global_state f);
   4.110  
   4.111 -fun edit_node (id, SOME id2) = insert_after id id2
   4.112 -  | edit_node (id, NONE) = delete_after id;
   4.113 -
   4.114 -fun edit_nodes (name, SOME edits) =
   4.115 -      Graph.default_node (name, empty_node) #>
   4.116 -      Graph.map_node name (fold edit_node edits)
   4.117 -  | edit_nodes (name, NONE) = Graph.del_node name;
   4.118 -
   4.119 -
   4.120 -
   4.121 -(** global configuration **)
   4.122 -
   4.123 -(* command executions *)
   4.124 -
   4.125 -local
   4.126 -
   4.127 -val global_execs =
   4.128 -  Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
   4.129 -
   4.130 -in
   4.131 -
   4.132 -fun define_exec (id: Document.exec_id) exec =
   4.133 -  NAMED_CRITICAL "Isar" (fn () =>
   4.134 -    Unsynchronized.change global_execs (Inttab.update_new (id, exec))
   4.135 -      handle Inttab.DUP dup => err_dup "exec" dup);
   4.136 -
   4.137 -fun the_exec (id: Document.exec_id) =
   4.138 -  (case Inttab.lookup (! global_execs) id of
   4.139 -    NONE => err_undef "exec" id
   4.140 -  | SOME exec => exec);
   4.141 +fun current_state () = ! global_state;
   4.142  
   4.143  end;
   4.144  
   4.145  
   4.146 -(* commands *)
   4.147 -
   4.148 -local
   4.149 -
   4.150 -val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]);
   4.151 -
   4.152 -in
   4.153 +(* define command *)
   4.154  
   4.155 -fun define_command (id: Document.command_id) text =
   4.156 -  let
   4.157 -    val id_string = Document.print_id id;
   4.158 -    val tr =
   4.159 -      Position.setmp_thread_data (Position.id_only id_string) (fn () =>
   4.160 -        Outer_Syntax.prepare_command (Position.id id_string) text) ();
   4.161 -  in
   4.162 -    NAMED_CRITICAL "Isar" (fn () =>
   4.163 -      Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr))
   4.164 -        handle Inttab.DUP dup => err_dup "command" dup)
   4.165 -  end;
   4.166 -
   4.167 -fun the_command (id: Document.command_id) =
   4.168 -  (case Inttab.lookup (! global_commands) id of
   4.169 -    NONE => err_undef "command" id
   4.170 -  | SOME tr => tr);
   4.171 -
   4.172 -end;
   4.173 +val _ =
   4.174 +  Isabelle_Process.add_command "Isar_Document.define_command"
   4.175 +    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
   4.176  
   4.177  
   4.178 -(* document versions *)
   4.179 -
   4.180 -local
   4.181 -
   4.182 -val global_versions = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: version)]);
   4.183 -
   4.184 -in
   4.185 +(* edit document version *)
   4.186  
   4.187 -fun define_version (id: Document.version_id) version =
   4.188 -  NAMED_CRITICAL "Isar" (fn () =>
   4.189 -    Unsynchronized.change global_versions (Inttab.update_new (id, version))
   4.190 -      handle Inttab.DUP dup => err_dup "version" dup);
   4.191 +val _ =
   4.192 +  Isabelle_Process.add_command "Isar_Document.edit_version"
   4.193 +    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
   4.194 +      let
   4.195 +        val old_id = Document.parse_id old_id_string;
   4.196 +        val new_id = Document.parse_id new_id_string;
   4.197 +        val edits =
   4.198 +          XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
   4.199 +            (XML_Data.dest_option (XML_Data.dest_list
   4.200 +                (XML_Data.dest_pair XML_Data.dest_int
   4.201 +                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
   4.202  
   4.203 -fun the_version (id: Document.version_id) =
   4.204 -  (case Inttab.lookup (! global_versions) id of
   4.205 -    NONE => err_undef "version" id
   4.206 -  | SOME version => version);
   4.207 +      val (updates, state') = Document.edit old_id new_id edits state;
   4.208 +      val _ =
   4.209 +        implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
   4.210 +        |> Markup.markup (Markup.assign new_id)
   4.211 +        |> Output.status;
   4.212 +      val state'' = Document.execute new_id state';
   4.213 +    in state'' end));
   4.214  
   4.215  end;
   4.216  
   4.217 -
   4.218 -
   4.219 -(** document editing **)
   4.220 -
   4.221 -(* execution *)
   4.222 -
   4.223 -local
   4.224 -
   4.225 -val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
   4.226 -
   4.227 -fun force_exec NONE = ()
   4.228 -  | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id));
   4.229 -
   4.230 -in
   4.231 -
   4.232 -fun execute version =
   4.233 -  NAMED_CRITICAL "Isar" (fn () =>
   4.234 -    let
   4.235 -      val old_execution = ! execution;
   4.236 -      val _ = List.app Future.cancel old_execution;
   4.237 -      fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
   4.238 -      (* FIXME proper node deps *)
   4.239 -      val new_execution = Graph.keys version |> map (fn name =>
   4.240 -        Future.fork_pri 1 (fn () =>
   4.241 -          let
   4.242 -            val _ = await_cancellation ();
   4.243 -            val exec =
   4.244 -              fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
   4.245 -                (the_node version name);
   4.246 -          in exec () end));
   4.247 -    in execution := new_execution end);
   4.248 -
   4.249 -end;
   4.250 -
   4.251 -
   4.252 -(* editing *)
   4.253 -
   4.254 -local
   4.255 -
   4.256 -fun is_changed node' (id, {next = _, exec}) =
   4.257 -  (case try (the_entry node') id of
   4.258 -    NONE => true
   4.259 -  | SOME {next = _, exec = exec'} => exec' <> exec);
   4.260 -
   4.261 -fun new_exec name (id: Document.command_id) (exec_id, updates) =
   4.262 -  let
   4.263 -    val exec = the_exec exec_id;
   4.264 -    val exec_id' = create_id ();
   4.265 -    val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id);
   4.266 -    val exec' =
   4.267 -      Lazy.lazy (fn () =>
   4.268 -        (case Lazy.force exec of
   4.269 -          NONE => NONE
   4.270 -        | SOME st => Toplevel.run_command name tr st));
   4.271 -    val _ = define_exec exec_id' exec';
   4.272 -  in (exec_id', (id, exec_id') :: updates) end;
   4.273 -
   4.274 -fun updates_status new_id updates =
   4.275 -  implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
   4.276 -  |> Markup.markup (Markup.assign new_id)
   4.277 -  |> Output.status;
   4.278 -
   4.279 -in
   4.280 -
   4.281 -fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
   4.282 -  NAMED_CRITICAL "Isar" (fn () =>
   4.283 -    let
   4.284 -      val old_version = the_version old_id;
   4.285 -      val new_version = fold edit_nodes edits old_version;
   4.286 -
   4.287 -      fun update_node name node =
   4.288 -        (case first_entry (is_changed (the_node old_version name)) node of
   4.289 -          NONE => ([], node)
   4.290 -        | SOME (prev, id, _) =>
   4.291 -            let
   4.292 -              val prev_exec_id = the (#exec (the_entry node (the prev)));
   4.293 -              val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []);
   4.294 -              val node' = fold set_entry_exec updates node;
   4.295 -            in (rev updates, node') end);
   4.296 -
   4.297 -      (* FIXME proper node deps *)
   4.298 -      val (updatess, new_version') =
   4.299 -        (Graph.keys new_version, new_version)
   4.300 -          |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
   4.301 -
   4.302 -      val _ = define_version new_id new_version';
   4.303 -      val _ = updates_status new_id (flat updatess);
   4.304 -      val _ = execute new_version';
   4.305 -    in () end);
   4.306 -
   4.307 -end;
   4.308 -
   4.309 -
   4.310 -
   4.311 -(** Isabelle process commands **)
   4.312 -
   4.313 -val _ =
   4.314 -  Isabelle_Process.add_command "Isar_Document.define_command"
   4.315 -    (fn [id, text] => define_command (Document.parse_id id) text);
   4.316 -
   4.317 -val _ =
   4.318 -  Isabelle_Process.add_command "Isar_Document.edit_version"
   4.319 -    (fn [old_id, new_id, edits] =>
   4.320 -      edit_document (Document.parse_id old_id) (Document.parse_id new_id)
   4.321 -        (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
   4.322 -            (XML_Data.dest_option (XML_Data.dest_list
   4.323 -                (XML_Data.dest_pair XML_Data.dest_int
   4.324 -                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits)));
   4.325 -
   4.326 -end;
   4.327 -
     5.1 --- a/src/Pure/System/isar_document.scala	Sun Aug 15 14:18:52 2010 +0200
     5.2 +++ b/src/Pure/System/isar_document.scala	Sun Aug 15 18:41:23 2010 +0200
     5.3 @@ -1,7 +1,7 @@
     5.4  /*  Title:      Pure/System/isar_document.scala
     5.5      Author:     Makarius
     5.6  
     5.7 -Interactive Isar documents.
     5.8 +Protocol commands for interactive Isar documents.
     5.9  */
    5.10  
    5.11  package isabelle