# HG changeset patch # User wenzelm # Date 1314364194 -7200 # Node ID 9a04e7502e22e56211452d0cf2e0449f6161f1e4 # Parent 4fdb1009a3706c4cf27c326c03e4e3eb6fec585b refined document state assignment: observe perspective, more explicit assignment message; misc tuning and clarification; diff -r 4fdb1009a370 -r 9a04e7502e22 src/Pure/General/linear_set.ML --- a/src/Pure/General/linear_set.ML Thu Aug 25 19:12:58 2011 +0200 +++ b/src/Pure/General/linear_set.ML Fri Aug 26 15:09:54 2011 +0200 @@ -17,7 +17,7 @@ val lookup: 'a T -> key -> ('a * key option) option val update: key * 'a -> 'a T -> 'a T val fold: key option -> - ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b + ((key option * key) * 'a -> 'b -> 'b option) -> 'a T -> 'b -> 'b val get_first: key option -> ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option val get_after: 'a T -> key option -> key option @@ -89,7 +89,11 @@ let val (x, next) = the_entry entries key; val item = ((prev, key), x); - in apply (SOME key) next (f item y) end; + in + (case f item y of + NONE => y + | SOME y' => apply (SOME key) next y') + end; in apply NONE (optional_start set opt_start) end; fun get_first opt_start P set = diff -r 4fdb1009a370 -r 9a04e7502e22 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Aug 25 19:12:58 2011 +0200 +++ b/src/Pure/PIDE/document.ML Fri Aug 26 15:09:54 2011 +0200 @@ -29,7 +29,7 @@ val cancel_execution: state -> Future.task list 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 * (string * command_id option) list) * state + ((command_id * exec_id option) list * (string * command_id option) list) * state val execute: version_id -> state -> state val state: unit -> state val change_state: (state -> state) -> unit @@ -140,15 +140,18 @@ type edit = string * node_edit; +fun next_entry (Node {entries, ...}) id = + (case Entries.lookup entries id of + NONE => err_undef "command entry" id + | SOME (_, next) => next); + fun the_entry (Node {entries, ...}) id = (case Entries.lookup entries id of NONE => err_undef "command entry" id | SOME (exec, _) => exec); -fun is_last_entry (Node {entries, ...}) id = - (case Entries.lookup entries id of - SOME (_, SOME _) => false - | _ => true); +fun the_default_entry node (SOME id) = the_default no_id (the_entry node id) + | the_default_entry _ NONE = no_id; fun update_entry id exec_id = map_entries (Entries.update (id, SOME exec_id)); @@ -208,7 +211,9 @@ in Graph.map_node name (set_header header') nodes3 end |> touch_node name | Perspective perspective => - update_node name (set_perspective perspective) nodes); + nodes + |> update_node name (set_perspective perspective) + |> touch_node name (* FIXME more precise!?! *)); end; @@ -371,10 +376,13 @@ local -fun is_changed node' ((_, id), exec) = - (case try (the_entry node') id of - NONE => true - | SOME exec' => exec' <> exec); +fun after_perspective node ((prev, _), _) = #2 (get_perspective node) = prev; + +fun needs_update node0 ((_, id), SOME exec) = + (case try (the_entry node0) id of + SOME (SOME exec0) => exec0 <> exec + | _ => true) + | needs_update _ _ = true; fun init_theory deps name node = let @@ -418,49 +426,62 @@ val updated = nodes_of new_version |> Graph.schedule (fn deps => fn (name, node) => - if not (is_touched node) then Future.value (([], []), node) + if not (is_touched node) then Future.value (([], [], []), node) else - (case first_entry NONE (is_changed (node_of old_version name)) node of - NONE => Future.value (([], []), set_touched false node) - | SOME ((prev, id), _) => - let - fun init () = init_theory deps name node; - in + let + val node0 = node_of old_version name; + fun init () = init_theory deps name node; + in + (case first_entry NONE (after_perspective node orf needs_update node0) node of + NONE => Future.value (([], [], []), set_touched false node) + | SOME ((prev, id), _) => (singleton o Future.forks) {name = "Document.edit", group = NONE, deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} (fn () => let - val prev_exec = - (case prev of - NONE => no_id - | SOME prev_id => the_default no_id (the_entry node prev_id)); - val (execs, last_exec as (last_id, _)) = - fold_entries (SOME id) (new_exec state init o #2 o #1) - node ([], the_exec state prev_exec); - val node' = + val (execs, exec) = + fold_entries (SOME id) + (fn entry1 as ((_, id1), _) => fn res => + if after_perspective node entry1 then NONE + else SOME (new_exec state init id1 res)) + node ([], the_exec state (the_default_entry node prev)); + + val no_execs = + if can (the_entry node0) id then + fold_entries (SOME id) + (fn ((_, id0), exec0) => fn res => + if is_none exec0 then NONE + else if exists (fn (_, (id1, _)) => id0 = id1) execs then SOME res + else SOME (id0 :: res)) node0 [] + else []; + + val node1 = fold (fn (exec_id, (command_id, _)) => update_entry command_id exec_id) execs node; + val last_exec = if #1 exec = no_id then NONE else SOME (#1 exec); val result = - if is_last_entry node' last_id - then Lazy.map #1 (#2 last_exec) + if is_some last_exec andalso is_none (next_entry node1 (the last_exec)) + then Lazy.map #1 (#2 exec) else no_result; - val node'' = node' - |> set_last_exec (if last_id = no_id then NONE else SOME last_id) + val node2 = node1 + |> set_last_exec last_exec |> set_result result |> set_touched false; - in ((execs, [(name, node'')]), node'') end) - end)) - |> Future.joins |> map #1 |> rev; (* FIXME why rev? *) + in ((no_execs, execs, [(name, node2)]), node2) end)) + end) + |> Future.joins |> map #1; - val updated_nodes = maps #2 updated; - val assignment = map (fn (exec_id, (command_id, _)) => (command_id, exec_id)) (maps #1 updated); + val command_execs = + map (rpair NONE) (maps #1 updated) @ + map (fn (exec_id, (command_id, _)) => (command_id, SOME exec_id)) (maps #2 updated); + val updated_nodes = maps #3 updated; val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes; val state' = state - |> fold (fold define_exec o #1) updated + |> fold (fold define_exec o #2) updated |> define_version new_id (fold put_node updated_nodes new_version); - in ((assignment, last_execs), state') end; + in ((command_execs, last_execs), state') end; end; @@ -490,7 +511,8 @@ (singleton o Future.forks) {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)), deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true} - (fold_entries NONE (fn (_, exec) => fn () => force_exec node exec) node)); + (fold_entries NONE + (fn entry as (_, exec) => fn () => SOME (force_exec node exec)) node)); in (versions, commands, execs, execution) end); diff -r 4fdb1009a370 -r 9a04e7502e22 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Aug 25 19:12:58 2011 +0200 +++ b/src/Pure/PIDE/document.scala Fri Aug 26 15:09:54 2011 +0200 @@ -157,7 +157,7 @@ object Change { - val init = Change(Future.value(Version.init), Nil, Future.value(Version.init)) + val init: Change = Change(Future.value(Version.init), Nil, Future.value(Version.init)) } sealed case class Change( @@ -173,7 +173,7 @@ object History { - val init = new History(List(Change.init)) + val init: History = new History(List(Change.init)) } // FIXME pruning, purging of state @@ -205,7 +205,7 @@ } type Assign = - (List[(Document.Command_ID, Document.Exec_ID)], // exec state assignment + (List[(Document.Command_ID, Option[Document.Exec_ID])], // exec state assignment List[(String, Option[Document.Command_ID])]) // last exec val no_assign: Assign = (Nil, Nil) @@ -214,8 +214,13 @@ { class Fail(state: State) extends Exception - val init = - State().define_version(Version.init, Map(), Map()).assign(Version.init.id, no_assign)._2 + val init: State = + State().define_version(Version.init, Assignment.init).assign(Version.init.id, no_assign)._2 + + object Assignment + { + val init: Assignment = Assignment(Map.empty, Map.empty, false) + } case class Assignment( val command_execs: Map[Command_ID, Exec_ID], @@ -223,12 +228,18 @@ val is_finished: Boolean) { def check_finished: Assignment = { require(is_finished); this } - def assign(add_command_execs: List[(Command_ID, Exec_ID)], + def unfinished: Assignment = copy(is_finished = false) + + def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])], add_last_execs: List[(String, Option[Command_ID])]): Assignment = { require(!is_finished) - // FIXME maintain last_commands - Assignment(command_execs ++ add_command_execs, last_execs ++ add_last_execs, true) + val command_execs1 = + (command_execs /: add_command_execs) { + case (res, (command_id, None)) => res - command_id + case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id) + } + Assignment(command_execs1, last_execs ++ add_last_execs, true) } } } @@ -243,14 +254,12 @@ { private def fail[A]: A = throw new State.Fail(this) - def define_version(version: Version, - command_execs: Map[Command_ID, Exec_ID], - last_execs: Map[String, Option[Command_ID]]): State = + def define_version(version: Version, assignment: State.Assignment): State = { val id = version.id if (versions.isDefinedAt(id) || disposed(id)) fail copy(versions = versions + (id -> version), - assignments = assignments + (id -> State.Assignment(command_execs, last_execs, false))) + assignments = assignments + (id -> assignment.unfinished)) } def define_command(command: Command): State = @@ -263,7 +272,7 @@ def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command) def the_version(id: Version_ID): Version = versions.getOrElse(id, fail) - def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) + def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) // FIXME rename def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail) def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail) @@ -287,16 +296,16 @@ val version = the_version(id) val (command_execs, last_execs) = arg - val new_execs = - (execs /: command_execs) { - case (execs1, (cmd_id, exec_id)) => - if (execs1.isDefinedAt(exec_id) || disposed(exec_id)) fail - execs1 + (exec_id -> the_command(cmd_id)) + val (commands, new_execs) = + ((Nil: List[Command], execs) /: command_execs) { + case ((commands1, execs1), (cmd_id, Some(exec_id))) => + val st = the_command(cmd_id) + (st.command :: commands1, execs1 + (exec_id -> st)) + case (res, (_, None)) => res } val new_assignment = the_assignment(version).assign(command_execs, last_execs) val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs) - val commands = command_execs.map(p => the_command(p._1).command) (commands, new_state) } diff -r 4fdb1009a370 -r 9a04e7502e22 src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Thu Aug 25 19:12:58 2011 +0200 +++ b/src/Pure/PIDE/isar_document.ML Fri Aug 26 15:09:54 2011 +0200 @@ -55,7 +55,7 @@ Output.status (Markup.markup (Markup.assign new_id) (assignment |> let open XML.Encode - in pair (list (pair int int)) (list (pair string (option int))) end + in pair (list (pair int (option int))) (list (pair string (option int))) end |> YXML.string_of_body)); val state'' = Document.execute new_id state'; in state'' end)); diff -r 4fdb1009a370 -r 9a04e7502e22 src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Thu Aug 25 19:12:58 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Fri Aug 26 15:09:54 2011 +0200 @@ -18,7 +18,7 @@ case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) => try { import XML.Decode._ - val a = pair(list(pair(long, long)), list(pair(string, option(long))))(body) + val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body) Some(id, a) } catch { diff -r 4fdb1009a370 -r 9a04e7502e22 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Aug 25 19:12:58 2011 +0200 +++ b/src/Pure/System/session.scala Fri Aug 26 15:09:54 2011 +0200 @@ -216,7 +216,7 @@ _.continue_history(Future.value(previous), text_edits, Future.value(version))) val assignment = global_state().the_assignment(previous).check_finished - global_state.change(_.define_version(version, assignment.command_execs, assignment.last_execs)) + global_state.change(_.define_version(version, assignment)) global_state.change_yield(_.assign(version.id, Document.no_assign)) prover.get.update_perspective(previous.id, version.id, name, perspective) @@ -268,15 +268,6 @@ val name = change.name val doc_edits = change.doc_edits - val previous_assignment = global_state().the_assignment(previous).check_finished - - var command_execs = previous_assignment.command_execs - for { - (name, Document.Node.Edits(cmd_edits)) <- doc_edits // FIXME proper coverage!? - (prev, None) <- cmd_edits - removed <- previous.nodes(name).commands.get_after(prev) - } command_execs -= removed.id - def id_command(command: Command) { if (global_state().lookup_command(command.id).isEmpty) { @@ -289,7 +280,8 @@ edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command } } - global_state.change(_.define_version(version, command_execs, previous_assignment.last_execs)) + val assignment = global_state().the_assignment(previous).check_finished + global_state.change(_.define_version(version, assignment)) prover.get.edit_version(previous.id, version.id, doc_edits) } //}}} @@ -388,9 +380,10 @@ reply(()) case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined => - if (text_edits.isEmpty && global_state().tip_stable) - update_perspective(name, perspective) - else +// FIXME +// if (text_edits.isEmpty && global_state().tip_stable) +// update_perspective(name, perspective) +// else handle_edits(name, master_dir, header, List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective))) reply(()) diff -r 4fdb1009a370 -r 9a04e7502e22 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Thu Aug 25 19:12:58 2011 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Fri Aug 26 15:09:54 2011 +0200 @@ -101,7 +101,7 @@ else last_perspective snapshot() match { - case Nil if new_perspective == last_perspective => + case Nil if last_perspective == new_perspective => case edits => pending.clear last_perspective = new_perspective