1.1 --- a/src/Pure/PIDE/document.ML	Thu Apr 05 22:33:52 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Apr 06 11:49:08 2012 +0200
     1.3 @@ -28,7 +28,6 @@
     1.4    val discontinue_execution: state -> unit
     1.5    val cancel_execution: state -> Future.task list
     1.6    val execute: version_id -> state -> state
     1.7 -  val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
     1.8    val update: version_id -> version_id -> edit list -> state ->
     1.9      ((command_id * exec_id option) list * (string * command_id option) list) * state
    1.10    val remove_versions: version_id list -> state -> state
    1.11 @@ -348,19 +347,9 @@
    1.12  
    1.13  
    1.14  
    1.15 -(** update **)
    1.16 -
    1.17 -(* perspective *)
    1.18 +(** edits **)
    1.19  
    1.20 -fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state =
    1.21 -  let
    1.22 -    val old_version = the_version state old_id;
    1.23 -    val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *)
    1.24 -    val new_version = edit_nodes (name, Perspective perspective) old_version;
    1.25 -  in define_version new_id new_version state end;
    1.26 -
    1.27 -
    1.28 -(* edits *)
    1.29 +(* update *)
    1.30  
    1.31  local
    1.32