src/Pure/PIDE/protocol.ML
changeset 47346 cd3ab7625519
parent 47343 b8aeab386414
child 47388 fe4b245af74c
     1.1 --- a/src/Pure/PIDE/protocol.ML	Thu Apr 05 22:33:52 2012 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Apr 06 11:49:08 2012 +0200
     1.3 @@ -21,22 +21,6 @@
     1.4      (fn [] => ignore (Document.cancel_execution (Document.state ())));
     1.5  
     1.6  val _ =
     1.7 -  Isabelle_Process.protocol_command "Document.update_perspective"
     1.8 -    (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
     1.9 -      let
    1.10 -        val old_id = Document.parse_id old_id_string;
    1.11 -        val new_id = Document.parse_id new_id_string;
    1.12 -        val ids = YXML.parse_body ids_yxml
    1.13 -          |> let open XML.Decode in list int end;
    1.14 -
    1.15 -        val _ = Future.join_tasks (Document.cancel_execution state);
    1.16 -      in
    1.17 -        state
    1.18 -        |> Document.update_perspective old_id new_id name ids
    1.19 -        |> Document.execute new_id
    1.20 -      end));
    1.21 -
    1.22 -val _ =
    1.23    Isabelle_Process.protocol_command "Document.update"
    1.24      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    1.25        let