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;

--- 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 ();

--- 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 =

--- 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"

--- 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])
   {

--- 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 =>

--- 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))

--- 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()
   }
 
 

--- 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()