# HG changeset patch # User wenzelm # Date 1314283446 -7200 # Node ID e8a87398f35d449f14b44c778b41e51b81289590 # Parent 709e1d67148358301e03684acb4f4c616ffcc18b propagate information about last command with exec state assignment through document model; diff -r 709e1d671483 -r e8a87398f35d src/Pure/General/linear_set.ML --- a/src/Pure/General/linear_set.ML Thu Aug 25 13:24:41 2011 +0200 +++ b/src/Pure/General/linear_set.ML Thu Aug 25 16:44:06 2011 +0200 @@ -14,7 +14,7 @@ val empty: 'a T val is_empty: 'a T -> bool val defined: 'a T -> key -> bool - val lookup: 'a T -> key -> 'a option + 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 @@ -70,7 +70,7 @@ fun defined set key = Table.defined (entries_of set) key; -fun lookup set key = Option.map fst (Table.lookup (entries_of set) key); +fun lookup set key = Table.lookup (entries_of set) key; fun update (key, x) = map_set (fn (start, entries) => (start, put_entry (key, (x, next_entry entries key)) entries)); diff -r 709e1d671483 -r e8a87398f35d src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Thu Aug 25 13:24:41 2011 +0200 +++ b/src/Pure/General/markup.ML Thu Aug 25 16:44:06 2011 +0200 @@ -108,9 +108,7 @@ val failedN: string val failed: T val finishedN: string val finished: T val versionN: string - val execN: string val assignN: string val assign: int -> T - val editN: string val edit: int * int -> T val serialN: string val promptN: string val prompt: T val readyN: string val ready: T @@ -353,12 +351,8 @@ (* interactive documents *) val versionN = "version"; -val execN = "exec"; val (assignN, assign) = markup_int "assign" versionN; -val editN = "edit"; -fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]); - (* messages *) diff -r 709e1d671483 -r e8a87398f35d src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Thu Aug 25 13:24:41 2011 +0200 +++ b/src/Pure/General/markup.scala Thu Aug 25 16:44:06 2011 +0200 @@ -232,9 +232,7 @@ /* interactive documents */ val VERSION = "version" - val EXEC = "exec" val ASSIGN = "assign" - val EDIT = "edit" /* prover process */ diff -r 709e1d671483 -r e8a87398f35d src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Aug 25 13:24:41 2011 +0200 +++ b/src/Pure/PIDE/document.ML Thu Aug 25 16:44:06 2011 +0200 @@ -28,7 +28,8 @@ val join_commands: state -> unit 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 * state + val edit: version_id -> version_id -> edit list -> state -> + ((command_id * exec_id) list * (string * command_id option) list) * state val execute: version_id -> state -> state val state: unit -> state val change_state: (state -> state) -> unit @@ -58,7 +59,7 @@ (** document structure **) type node_header = (string * string list * (string * bool) list) Exn.result; -type perspective = (command_id -> bool) * command_id list; (*visible commands, canonical order*) +type perspective = (command_id -> bool) * command_id option; (*visible commands, last*) structure Entries = Linear_Set(type key = command_id val ord = int_ord); abstype node = Node of @@ -66,58 +67,63 @@ header: node_header, perspective: perspective, entries: exec_id option Entries.T, (*command entries with excecutions*) + last_exec: command_id option, (*last command with exec state assignment*) result: Toplevel.state lazy} and version = Version of node Graph.T (*development graph wrt. static imports*) with -fun make_node (touched, header, perspective, entries, result) = +fun make_node (touched, header, perspective, entries, last_exec, result) = Node {touched = touched, header = header, perspective = perspective, - entries = entries, result = result}; + entries = entries, last_exec = last_exec, result = result}; -fun map_node f (Node {touched, header, perspective, entries, result}) = - make_node (f (touched, header, perspective, entries, result)); +fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) = + make_node (f (touched, header, perspective, entries, last_exec, result)); -fun make_perspective ids : perspective = - (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids); +fun make_perspective command_ids : perspective = + (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids); +val no_header = Exn.Exn (ERROR "Bad theory header"); val no_perspective = make_perspective []; val no_print = Lazy.value (); val no_result = Lazy.value Toplevel.toplevel; -val empty_node = - make_node (false, Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result); - -val clear_node = - map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result)); +val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result); +val clear_node = map_node (fn (_, header, _, _, _, _) => + (false, header, no_perspective, Entries.empty, NONE, no_result)); (* basic components *) fun is_touched (Node {touched, ...}) = touched; fun set_touched touched = - map_node (fn (_, header, perspective, entries, result) => - (touched, header, perspective, entries, result)); + map_node (fn (_, header, perspective, entries, last_exec, result) => + (touched, header, perspective, entries, last_exec, result)); fun get_header (Node {header, ...}) = header; fun set_header header = - map_node (fn (touched, _, perspective, entries, result) => - (touched, header, perspective, entries, result)); + map_node (fn (touched, _, perspective, entries, last_exec, result) => + (touched, header, perspective, entries, last_exec, result)); fun get_perspective (Node {perspective, ...}) = perspective; fun set_perspective ids = - map_node (fn (touched, header, _, entries, result) => - (touched, header, make_perspective ids, entries, result)); + map_node (fn (touched, header, _, entries, last_exec, result) => + (touched, header, make_perspective ids, entries, last_exec, result)); fun map_entries f = - map_node (fn (touched, header, perspective, entries, result) => - (touched, header, perspective, f entries, result)); + map_node (fn (touched, header, perspective, entries, last_exec, result) => + (touched, header, perspective, f entries, last_exec, result)); fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; +fun get_last_exec (Node {last_exec, ...}) = last_exec; +fun set_last_exec last_exec = + map_node (fn (touched, header, perspective, entries, _, result) => + (touched, header, perspective, entries, last_exec, result)); + fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result); fun set_result result = - map_node (fn (touched, header, perspective, entries, _) => - (touched, header, perspective, entries, result)); + map_node (fn (touched, header, perspective, entries, last_exec, _) => + (touched, header, perspective, entries, last_exec, result)); fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; fun default_node name = Graph.default_node (name, empty_node); @@ -137,9 +143,14 @@ fun the_entry (Node {entries, ...}) id = (case Entries.lookup entries id of NONE => err_undef "command entry" id - | SOME entry => entry); + | SOME (exec, _) => exec); -fun update_entry (id, exec_id) = +fun is_last_entry (Node {entries, ...}) id = + (case Entries.lookup entries id of + SOME (_, SOME _) => false + | _ => true); + +fun update_entry id exec_id = map_entries (Entries.update (id, SOME exec_id)); fun reset_after id entries = @@ -382,17 +393,19 @@ (#2 (Future.join (the (AList.lookup (op =) deps import)))))); in Thy_Load.begin_theory dir thy_name imports files parents end; -fun new_exec state init command_id (assigns, execs, exec) = +fun new_exec state init command_id' (execs, exec) = let - val command = the_command state command_id; + val command' = the_command state command_id'; val exec_id' = new_id (); - val exec' = exec |> Lazy.map (fn (st, _) => - let val tr = - Future.join command - |> Toplevel.modify_init init - |> Toplevel.put_id (print_id exec_id'); - in run_command tr st end); - in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end; + val exec' = + snd exec |> Lazy.map (fn (st, _) => + let val tr = + Future.join command' + |> Toplevel.modify_init init + |> Toplevel.put_id (print_id exec_id'); + in run_command tr st end) + |> pair command_id'; + in ((exec_id', exec') :: execs, exec') end; in @@ -402,13 +415,13 @@ val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) val new_version = fold edit_nodes edits old_version; - val updates = + 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) + NONE => Future.value (([], []), set_touched false node) | SOME ((prev, id), _) => let fun init () = init_theory deps name node; @@ -422,22 +435,32 @@ (case prev of NONE => no_id | SOME prev_id => the_default no_id (the_entry node prev_id)); - val (assigns, execs, last_exec) = + val (execs, last_exec as (last_id, _)) = fold_entries (SOME id) (new_exec state init o #2 o #1) - node ([], [], #2 (the_exec state prev_exec)); - val node' = node - |> fold update_entry assigns - |> set_result (Lazy.map #1 last_exec) + node ([], the_exec state prev_exec); + val node' = + fold (fn (exec_id, (command_id, _)) => update_entry command_id exec_id) + execs node; + val result = + if is_last_entry node' last_id + then Lazy.map #1 (#2 last_exec) + else no_result; + val node'' = node' + |> set_last_exec (if last_id = no_id then NONE else SOME last_id) + |> set_result result |> set_touched false; - in ((assigns, execs, [(name, node')]), node') end) + in ((execs, [(name, node'')]), node'') end) end)) - |> Future.joins |> map #1; + |> Future.joins |> map #1 |> rev; (* FIXME why rev? *) + + val updated_nodes = maps #2 updated; + val assignment = map (fn (exec_id, (command_id, _)) => (command_id, exec_id)) (maps #1 updated); + val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes; val state' = state - |> fold (fold define_exec o #2) updates - |> define_version new_id (fold (fold put_node o #3) updates new_version); - - in (maps #1 (rev updates), state') end; + |> fold (fold define_exec o #1) updated + |> define_version new_id (fold put_node updated_nodes new_version); + in ((assignment, last_execs), state') end; end; diff -r 709e1d671483 -r e8a87398f35d src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Aug 25 13:24:41 2011 +0200 +++ b/src/Pure/PIDE/document.scala Thu Aug 25 16:44:06 2011 +0200 @@ -204,20 +204,28 @@ : Stream[Text.Info[Option[A]]] } + type Assign = + (List[(Document.Command_ID, Document.Exec_ID)], // exec state assignment + List[(String, Option[Document.Command_ID])]) // last exec + + val no_assign: Assign = (Nil, Nil) + object State { class Fail(state: State) extends Exception - val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)._2 + val init = State().define_version(Version.init, Map()).assign(Version.init.id, no_assign)._2 case class Assignment( val assignment: Map[Command, Exec_ID], val is_finished: Boolean = false) { def get_finished: Map[Command, Exec_ID] = { require(is_finished); assignment } - def assign(command_execs: List[(Command, Exec_ID)]): Assignment = + def assign(command_execs: List[(Command, Exec_ID)], + last_commands: List[(String, Option[Command])]): Assignment = { require(!is_finished) + // FIXME maintain last_commands Assignment(assignment ++ command_execs, true) } } @@ -270,9 +278,10 @@ } } - def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) = + def assign(id: Version_ID, arg: Assign): (List[Command], State) = { val version = the_version(id) + val (edits, last_ids) = arg var new_execs = execs val assigned_execs = @@ -282,8 +291,14 @@ new_execs += (exec_id -> st) (st.command, exec_id) } - val new_assignment = the_assignment(version).assign(assigned_execs) + + val last_commands = + last_ids map { + case (name, Some(cmd_id)) => (name, Some(the_command(cmd_id).command)) + case (name, None) => (name, None) } + val new_assignment = the_assignment(version).assign(assigned_execs, last_commands) val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs) + (assigned_execs.map(_._1), new_state) } diff -r 709e1d671483 -r e8a87398f35d src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Thu Aug 25 13:24:41 2011 +0200 +++ b/src/Pure/PIDE/isar_document.ML Thu Aug 25 16:44:06 2011 +0200 @@ -48,12 +48,15 @@ end; val running = Document.cancel_execution state; - val (updates, state') = Document.edit old_id new_id edits state; + val (assignment, state') = Document.edit old_id new_id edits state; val _ = Future.join_tasks running; val _ = Document.join_commands state'; val _ = Output.status (Markup.markup (Markup.assign new_id) - (implode (map (Markup.markup_only o Markup.edit) updates))); + (assignment |> + let open XML.Encode + in pair (list (pair int int)) (list (pair string (option int))) end + |> YXML.string_of_body)); val state'' = Document.execute new_id state'; in state'' end)); diff -r 709e1d671483 -r e8a87398f35d src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Thu Aug 25 13:24:41 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Thu Aug 25 16:44:06 2011 +0200 @@ -11,24 +11,20 @@ { /* document editing */ - object Assign { - def unapply(msg: XML.Tree) - : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] = + object Assign + { + def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] = msg match { - case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) => - val id_edits = edits.map(Edit.unapply) - if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get))) - else None - case _ => None - } - } - - object Edit { - def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] = - msg match { - case XML.Elem( - Markup(Markup.EDIT, - List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j)) + 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) + Some(id, a) + } + catch { + case _: XML.XML_Atom => None + case _: XML.XML_Body => None + } case _ => None } } diff -r 709e1d671483 -r e8a87398f35d src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Aug 25 13:24:41 2011 +0200 +++ b/src/Pure/System/session.scala Thu Aug 25 16:44:06 2011 +0200 @@ -217,7 +217,7 @@ val assignment = global_state().the_assignment(previous).get_finished global_state.change(_.define_version(version, assignment)) - global_state.change_yield(_.assign(version.id, Nil)) + global_state.change_yield(_.assign(version.id, Document.no_assign)) prover.get.update_perspective(previous.id, version.id, name, perspective) } @@ -248,10 +248,10 @@ /* exec state assignment */ - def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)]) + def handle_assign(id: Document.Version_ID, assign: Document.Assign) //{{{ { - val cmds = global_state.change_yield(_.assign(id, edits)) + val cmds = global_state.change_yield(_.assign(id, assign)) for (cmd <- cmds) command_change_buffer ! cmd assignments.event(Session.Assignment) } @@ -336,8 +336,8 @@ else if (result.is_stdout) { } else if (result.is_status) { result.body match { - case List(Isar_Document.Assign(id, edits)) => - try { handle_assign(id, edits) } + case List(Isar_Document.Assign(id, assign)) => + try { handle_assign(id, assign) } catch { case _: Document.State.Fail => bad_result(result) } case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) case List(Keyword.Keyword_Decl(name)) => syntax += name