discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;

--- a/src/Pure/PIDE/document.ML	Thu Apr 05 22:33:52 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Apr 06 11:49:08 2012 +0200
@@ -28,7 +28,6 @@
   val discontinue_execution: state -> unit
   val cancel_execution: state -> Future.task list
   val execute: version_id -> state -> state
-  val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
   val update: version_id -> version_id -> edit list -> state ->
     ((command_id * exec_id option) list * (string * command_id option) list) * state
   val remove_versions: version_id list -> state -> state
@@ -348,19 +347,9 @@
 
 
 
-(** update **)
-
-(* perspective *)
+(** edits **)
 
-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;
-
-
-(* edits *)
+(* update *)
 
 local
 

--- a/src/Pure/PIDE/protocol.ML	Thu Apr 05 22:33:52 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Apr 06 11:49:08 2012 +0200
@@ -21,22 +21,6 @@
     (fn [] => ignore (Document.cancel_execution (Document.state ())));
 
 val _ =
-  Isabelle_Process.protocol_command "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.protocol_command "Document.update"
     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
       let

--- a/src/Pure/PIDE/protocol.scala	Thu Apr 05 22:33:52 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Apr 06 11:49:08 2012 +0200
@@ -195,17 +195,6 @@
 
   def cancel_execution() { input("Document.cancel_execution") }
 
-  def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
-    name: Document.Node.Name, perspective: Command.Perspective)
-  {
-    val ids =
-    { import XML.Encode._
-      list(long)(perspective.commands.map(_.id)) }
-
-    input("Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
-      name.node, YXML.string_of_body(ids))
-  }
-
   def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
     edits: List[Document.Edit_Command])
   {

--- a/src/Pure/System/session.scala	Thu Apr 05 22:33:52 2012 +0200
+++ b/src/Pure/System/session.scala	Fri Apr 06 11:49:08 2012 +0200
@@ -267,27 +267,6 @@
     }
 
 
-    /* perspective */
-
-    def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
-    {
-      val previous = global_state().tip_version
-      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 >>>
-          (_.continue_history(Future.value(previous), text_edits, Future.value(version)))
-
-      val assignment = global_state().the_assignment(previous).check_finished
-      global_state >> (_.define_version(version, assignment))
-      global_state >>> (_.assign(version.id))
-
-      prover.get.update_perspective(previous.id, version.id, name, perspective)
-    }
-
-
     /* incoming edits */
 
     def handle_edits(name: Document.Node.Name,
@@ -465,12 +444,8 @@
           reply(())
 
         case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
-          if (text_edits.isEmpty && global_state().tip_stable &&
-              perspective.range.stop <= global_state().last_exec_offset(name))
-            update_perspective(name, perspective)
-          else
-            handle_edits(name, header,
-              List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
+          handle_edits(name, header,
+            List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
           reply(())
 
         case Messages(msgs) =>

--- a/src/Pure/Thy/thy_syntax.scala	Thu Apr 05 22:33:52 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Apr 06 11:49:08 2012 +0200
@@ -118,28 +118,6 @@
     }
   }
 
-  def update_perspective(nodes: Document.Nodes,
-      name: Document.Node.Name, text_perspective: Text.Perspective)
-    : (Command.Perspective, Option[Document.Nodes]) =
-  {
-    val node = nodes(name)
-    val perspective = command_perspective(node, text_perspective)
-    val new_nodes =
-      if (node.perspective same perspective) None
-      else Some(nodes + (name -> node.update_perspective(perspective)))
-    (perspective, new_nodes)
-  }
-
-  def edit_perspective(previous: Document.Version,
-      name: Document.Node.Name, 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.make(previous.syntax, new_nodes getOrElse nodes)
-    (perspective, version)
-  }
-
 
 
   /** header edits: structure and outer syntax **/
@@ -311,11 +289,11 @@
       case (name, Document.Node.Header(_)) =>
 
       case (name, Document.Node.Perspective(text_perspective)) =>
-        update_perspective(nodes, name, text_perspective) match {
-          case (_, None) =>
-          case (perspective, Some(nodes1)) =>
-            doc_edits += (name -> Document.Node.Perspective(perspective))
-            nodes = nodes1
+        val node = nodes(name)
+        val perspective = command_perspective(node, text_perspective)
+        if (!(node.perspective same perspective)) {
+          doc_edits += (name -> Document.Node.Perspective(perspective))
+          nodes += (name -> node.update_perspective(perspective))
         }
     }
     (doc_edits.toList, Document.Version.make(syntax, nodes))