src/Pure/PIDE/document.ML
changeset 47346 cd3ab7625519
parent 47345 193251980a73
child 47347 af937661e4a1
--- 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