src/Pure/PIDE/isar_document.ML
author wenzelm
Thu Aug 25 16:44:06 2011 +0200 (2011-08-25 ago)
changeset 44476 e8a87398f35d
parent 44436 546adfa8a6fc
child 44479 9a04e7502e22
permissions -rw-r--r--
propagate information about last command with exec state assignment through document model;
     1 (*  Title:      Pure/PIDE/isar_document.ML
     2     Author:     Makarius
     3 
     4 Protocol message formats for interactive Isar documents.
     5 *)
     6 
     7 structure Isar_Document: sig end =
     8 struct
     9 
    10 val _ =
    11   Isabelle_Process.add_command "Isar_Document.define_command"
    12     (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
    13 
    14 val _ =
    15   Isabelle_Process.add_command "Isar_Document.update_perspective"
    16     (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
    17       let
    18         val old_id = Document.parse_id old_id_string;
    19         val new_id = Document.parse_id new_id_string;
    20         val ids = YXML.parse_body ids_yxml
    21           |> let open XML.Decode in list int end;
    22 
    23         val _ = Future.join_tasks (Document.cancel_execution state);
    24       in
    25         state
    26         |> Document.update_perspective old_id new_id name ids
    27         |> Document.execute new_id
    28       end));
    29 
    30 val _ =
    31   Isabelle_Process.add_command "Isar_Document.edit_version"
    32     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    33       let
    34         val old_id = Document.parse_id old_id_string;
    35         val new_id = Document.parse_id new_id_string;
    36         val edits =
    37           YXML.parse_body edits_yxml |>
    38             let open XML.Decode in
    39               list (pair string
    40                 (variant
    41                  [fn ([], []) => Document.Clear,
    42                   fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    43                   fn ([], a) =>
    44                     Document.Header
    45                       (Exn.Res (triple string (list string) (list (pair string bool)) a)),
    46                   fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
    47                   fn (a, []) => Document.Perspective (map int_atom a)]))
    48             end;
    49 
    50         val running = Document.cancel_execution state;
    51         val (assignment, state') = Document.edit old_id new_id edits state;
    52         val _ = Future.join_tasks running;
    53         val _ = Document.join_commands state';
    54         val _ =
    55           Output.status (Markup.markup (Markup.assign new_id)
    56             (assignment |>
    57               let open XML.Encode
    58               in pair (list (pair int int)) (list (pair string (option int))) end
    59               |> YXML.string_of_body));
    60         val state'' = Document.execute new_id state';
    61       in state'' end));
    62 
    63 val _ =
    64   Isabelle_Process.add_command "Isar_Document.invoke_scala"
    65     (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
    66 
    67 end;
    68