src/Pure/PIDE/protocol.ML
changeset 47346 cd3ab7625519
parent 47343 b8aeab386414
child 47388 fe4b245af74c
--- 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