# HG changeset patch # User wenzelm # Date 1314183819 -7200 # Node ID 546adfa8a6fc38cc12ef0ea260efd4f10c1018e3 # Parent d4c69d0bbd27e8c264b006a81a2dabbb9bfe565f update_perspective without actual edits, bypassing the full state assignment protocol; edit_nodes/Perspective: do not touch_descendants here; propagate editor scroll events via update_perspective; misc tuning; diff -r d4c69d0bbd27 -r 546adfa8a6fc src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Aug 23 21:19:24 2011 +0200 +++ b/src/Pure/PIDE/document.ML Wed Aug 24 13:03:39 2011 +0200 @@ -27,6 +27,7 @@ val join_commands: state -> unit val cancel_execution: state -> Future.task list val define_command: command_id -> string -> state -> state + 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 execute: version_id -> state -> state val state: unit -> state @@ -154,27 +155,31 @@ fun edit_nodes (name, node_edit) (Version nodes) = Version - (touch_descendants name - (case node_edit of - Clear => update_node name clear_node nodes - | Edits edits => - nodes - |> update_node name (edit_node edits) - | Header header => - let - val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []); - val nodes1 = nodes - |> default_node name - |> fold default_node parents; - val nodes2 = nodes1 - |> Graph.Keys.fold - (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); - val (header', nodes3) = - (header, Graph.add_deps_acyclic (name, parents) nodes2) - handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); - in Graph.map_node name (set_header header') nodes3 end - | Perspective perspective => - update_node name (set_perspective perspective) nodes)); + (case node_edit of + Clear => + nodes + |> update_node name clear_node + |> touch_descendants name + | Edits edits => + nodes + |> update_node name (edit_node edits) + |> touch_descendants name + | Header header => + let + val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []); + val nodes1 = nodes + |> default_node name + |> fold default_node parents; + val nodes2 = nodes1 + |> Graph.Keys.fold + (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); + val (header', nodes3) = + (header, Graph.add_deps_acyclic (name, parents) nodes2) + handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); + in Graph.map_node name (set_header header') nodes3 end + |> touch_descendants name + | Perspective perspective => + update_node name (set_perspective perspective) nodes); fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes); @@ -320,6 +325,16 @@ (** editing **) +(* perspective *) + +fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state = + let + val old_version = the_version state old_id; + val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *) + val new_version = edit_nodes (name, Perspective perspective) old_version; + in define_version new_id new_version state end; + + (* edit *) local @@ -346,7 +361,6 @@ (#2 (Future.join (the (AList.lookup (op =) deps import)))))); in Thy_Load.begin_theory dir thy_name imports files parents end; - fun new_exec (command_id, command) (assigns, execs, exec) = let val exec_id' = new_id (); diff -r d4c69d0bbd27 -r 546adfa8a6fc src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Aug 23 21:19:24 2011 +0200 +++ b/src/Pure/PIDE/document.scala Wed Aug 24 13:03:39 2011 +0200 @@ -146,7 +146,8 @@ val init: Version = Version(no_id, Map().withDefaultValue(Node.empty)) } - sealed case class Version(val id: Version_ID, val nodes: Map[String, Node]) + type Nodes = Map[String, Node] + sealed case class Version(val id: Version_ID, val nodes: Nodes) /* changes of plain text, eventually resulting in document edits */ @@ -290,6 +291,12 @@ case None => false } + def is_stable(change: Change): Boolean = + change.is_finished && is_assigned(change.version.get_finished) + + def tip_stable: Boolean = is_stable(history.tip) + def recent_stable: Option[Change] = history.undo_list.find(is_stable) + def extend_history(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): (Change, State) = @@ -302,11 +309,8 @@ // persistent user-view def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot = { - val found_stable = history.undo_list.find(change => - change.is_finished && is_assigned(change.version.get_finished)) - require(found_stable.isDefined) - val stable = found_stable.get - val latest = history.undo_list.head + val stable = recent_stable.get + val latest = history.tip // FIXME proper treatment of removed nodes val edits = diff -r d4c69d0bbd27 -r 546adfa8a6fc src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Tue Aug 23 21:19:24 2011 +0200 +++ b/src/Pure/PIDE/isar_document.ML Wed Aug 24 13:03:39 2011 +0200 @@ -12,6 +12,22 @@ (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text)); val _ = + Isabelle_Process.add_command "Isar_Document.update_perspective" + (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state => + let + val old_id = Document.parse_id old_id_string; + val new_id = Document.parse_id new_id_string; + val ids = YXML.parse_body ids_yxml + |> let open XML.Decode in list int end; + + val _ = Future.join_tasks (Document.cancel_execution state); + in + state + |> Document.update_perspective old_id new_id name ids + |> Document.execute new_id + end)); + +val _ = Isabelle_Process.add_command "Isar_Document.edit_version" (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => let @@ -31,15 +47,15 @@ fn (a, []) => Document.Perspective (map int_atom a)])) end; - val running = Document.cancel_execution state; - val (updates, 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))); - val state'' = Document.execute new_id state'; - in state'' end)); + val running = Document.cancel_execution state; + val (updates, 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))); + val state'' = Document.execute new_id state'; + in state'' end)); val _ = Isabelle_Process.add_command "Isar_Document.invoke_scala" diff -r d4c69d0bbd27 -r 546adfa8a6fc src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Tue Aug 23 21:19:24 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Wed Aug 24 13:03:39 2011 +0200 @@ -139,6 +139,17 @@ /* document versions */ + def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID, + name: String, perspective: Command.Perspective) + { + val ids = + { import XML.Encode._ + list(long)(perspective.map(_.id)) } + + input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name, + YXML.string_of_body(ids)) + } + def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, edits: List[Document.Edit_Command]) { diff -r d4c69d0bbd27 -r 546adfa8a6fc src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Aug 23 21:19:24 2011 +0200 +++ b/src/Pure/System/session.scala Wed Aug 24 13:03:39 2011 +0200 @@ -180,6 +180,27 @@ var prover: Option[Isabelle_Process with Isar_Document] = None + /* perspective */ + + def update_perspective(name: String, text_perspective: Text.Perspective) + { + val previous = global_state().history.tip.version.get_finished + val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective) + + val text_edits: List[Document.Edit_Text] = + List((name, Document.Node.Perspective(text_perspective))) + val change = + global_state.change_yield( + _.extend_history(Future.value(previous), text_edits, Future.value(version))) + + val assignment = global_state().the_assignment(previous).get_finished + global_state.change(_.define_version(version, assignment)) + global_state.change_yield(_.assign(version.id, Nil)) + + prover.get.update_perspective(previous.id, version.id, name, perspective) + } + + /* incoming edits */ def handle_edits(name: String, master_dir: String, @@ -213,6 +234,18 @@ //}}} + /* exec state assignment */ + + def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)]) + //{{{ + { + val cmds = global_state.change_yield(_.assign(id, edits)) + for (cmd <- cmds) command_change_buffer ! cmd + assignments.event(Session.Assignment) + } + //}}} + + /* resulting changes */ def handle_change(change: Change_Node) @@ -292,11 +325,7 @@ else if (result.is_status) { result.body match { case List(Isar_Document.Assign(id, edits)) => - try { - val cmds: List[Command] = global_state.change_yield(_.assign(id, edits)) - for (cmd <- cmds) command_change_buffer ! cmd - assignments.event(Session.Assignment) - } + try { handle_assign(id, edits) } 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 @@ -345,9 +374,11 @@ reply(()) case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined => - handle_edits(name, master_dir, header, - List(Document.Node.Edits(text_edits), - Document.Node.Perspective(perspective))) + 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(()) case change: Change_Node if prover.isDefined => diff -r d4c69d0bbd27 -r 546adfa8a6fc src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Tue Aug 23 21:19:24 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Wed Aug 24 13:03:39 2011 +0200 @@ -97,7 +97,7 @@ - /** command perspective **/ + /** perspective **/ def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective = { @@ -126,6 +126,26 @@ } } + def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective) + : (Command.Perspective, Option[Document.Nodes]) = + { + val node = nodes(name) + val perspective = command_perspective(node, text_perspective) + val new_nodes = + if (Command.equal_perspective(node.perspective, perspective)) None + else Some(nodes + (name -> node.copy(perspective = perspective))) + (perspective, new_nodes) + } + + def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective) + : (Command.Perspective, Document.Version) = + { + val nodes = previous.nodes + val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective) + val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes) + (perspective, version) + } + /** text edits **/ @@ -243,11 +263,11 @@ } case (name, Document.Node.Perspective(text_perspective)) => - val node = nodes(name) - val perspective = command_perspective(node, text_perspective) - if (!Command.equal_perspective(node.perspective, perspective)) { - doc_edits += (name -> Document.Node.Perspective(perspective)) - nodes += (name -> node.copy(perspective = perspective)) + update_perspective(nodes, name, text_perspective) match { + case (_, None) => + case (perspective, Some(nodes1)) => + doc_edits += (name -> Document.Node.Perspective(perspective)) + nodes = nodes1 } } (doc_edits.toList, Document.Version(Document.new_id(), nodes)) diff -r d4c69d0bbd27 -r 546adfa8a6fc src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Aug 23 21:19:24 2011 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Wed Aug 24 13:03:39 2011 +0200 @@ -87,15 +87,17 @@ private object pending_edits // owned by Swing thread { private val pending = new mutable.ListBuffer[Text.Edit] + private var pending_perspective = false def snapshot(): List[Text.Edit] = pending.toList def flush() { Swing_Thread.require() snapshot() match { - case Nil => + case Nil if !pending_perspective => case edits => pending.clear + pending_perspective = false session.edit_node(node_name, master_dir, node_header(), perspective(), edits) } } @@ -116,6 +118,18 @@ pending += edit delay_flush() } + + def update_perspective() + { + pending_perspective = true + delay_flush() + } + } + + def update_perspective() + { + Swing_Thread.require() + pending_edits.update_perspective() } diff -r d4c69d0bbd27 -r 546adfa8a6fc src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Tue Aug 23 21:19:24 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Wed Aug 24 13:03:39 2011 +0200 @@ -25,7 +25,8 @@ import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug} import org.gjt.sp.jedit.gui.RolloverButton import org.gjt.sp.jedit.options.GutterOptionPane -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter} +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter, + ScrollListener} import org.gjt.sp.jedit.syntax.{SyntaxStyle} @@ -354,6 +355,15 @@ } + /* scrolling */ + + private val scroll_listener = new ScrollListener + { + def scrolledVertically(arg: TextArea) { model.update_perspective() } + def scrolledHorizontally(arg: TextArea) { } + } + + /* overview of command status left of scrollbar */ private val overview = new JPanel(new BorderLayout) @@ -474,6 +484,7 @@ text_area.getView.addWindowListener(window_listener) painter.addMouseMotionListener(mouse_motion_listener) text_area.addCaretListener(caret_listener) + text_area.addScrollListener(scroll_listener) text_area.addLeftOfScrollBar(overview) session.commands_changed += main_actor session.global_settings += main_actor @@ -488,6 +499,7 @@ text_area.getView.removeWindowListener(window_listener) painter.removeMouseMotionListener(mouse_motion_listener) text_area.removeCaretListener(caret_listener) + text_area.removeScrollListener(scroll_listener) text_area.removeLeftOfScrollBar(overview) text_area.getGutter.removeExtension(gutter_painter) text_area_painter.deactivate()