src/Pure/PIDE/protocol.ML
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
parent 63806 c54a53ef1873
child 65300 c262653a3b88
permissions -rw-r--r--
clarified modules;
     1 (*  Title:      Pure/PIDE/protocol.ML
     2     Author:     Makarius
     3 
     4 Protocol message formats for interactive proof documents.
     5 *)
     6 
     7 structure Protocol: sig end =
     8 struct
     9 
    10 val _ =
    11   Isabelle_Process.protocol_command "Prover.echo"
    12     (fn args => List.app writeln args);
    13 
    14 val _ =
    15   Isabelle_Process.protocol_command "Prover.options"
    16     (fn [options_yxml] =>
    17       Isabelle_Process.init_protocol_options (Options.decode (YXML.parse_body options_yxml)));
    18 
    19 val _ =
    20   Isabelle_Process.protocol_command "Document.define_blob"
    21     (fn [digest, content] => Document.change_state (Document.define_blob digest content));
    22 
    23 val _ =
    24   Isabelle_Process.protocol_command "Document.define_command"
    25     (fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
    26       let
    27         val (blobs, blobs_index) =
    28           YXML.parse_body blobs_yxml |>
    29             let
    30               val message =
    31                 YXML.string_of_body o Protocol_Message.command_positions id;
    32               open XML.Decode;
    33             in
    34               pair
    35                 (list (variant
    36                  [fn ([], a) => Exn.Res (pair string (option string) a),
    37                   fn ([], a) => Exn.Exn (ERROR (message a))]))
    38                 int
    39             end;
    40         val toks =
    41           (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
    42       in
    43         Document.change_state
    44           (Document.define_command (Document_ID.parse id) name blobs blobs_index toks)
    45       end);
    46 
    47 val _ =
    48   Isabelle_Process.protocol_command "Document.discontinue_execution"
    49     (fn [] => Execution.discontinue ());
    50 
    51 val _ =
    52   Isabelle_Process.protocol_command "Document.cancel_exec"
    53     (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id));
    54 
    55 val _ =
    56   Isabelle_Process.protocol_command "Document.update"
    57     (Future.task_context "Document.update" (Future.new_group NONE)
    58       (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    59         let
    60           val _ = Execution.discontinue ();
    61 
    62           val old_id = Document_ID.parse old_id_string;
    63           val new_id = Document_ID.parse new_id_string;
    64           val edits =
    65             YXML.parse_body edits_yxml |>
    66               let open XML.Decode in
    67                 list (pair string
    68                   (variant
    69                    [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    70                     fn ([], a) =>
    71                       let
    72                         val (master, (name, (imports, (keywords, errors)))) =
    73                           pair string (pair string (pair (list string)
    74                             (pair (list (pair string
    75                               (pair (pair string (list string)) (list string))))
    76                               (list YXML.string_of_body)))) a;
    77                         val imports' = map (rpair Position.none) imports;
    78                         val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
    79                         val header = Thy_Header.make (name, Position.none) imports' keywords';
    80                       in Document.Deps {master = master, header = header, errors = errors} end,
    81                     fn (a :: b, c) =>
    82                       Document.Perspective (bool_atom a, map int_atom b,
    83                         list (pair int (pair string (list string))) c)]))
    84               end;
    85 
    86           val (removed, assign_update, state') = Document.update old_id new_id edits state;
    87           val _ =
    88             (singleton o Future.forks)
    89              {name = "Document.update/remove", group = NONE,
    90               deps = maps Future.group_snapshot (maps Execution.peek removed),
    91               pri = Task_Queue.urgent_pri + 2, interrupts = false}
    92              (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
    93 
    94           val _ =
    95             Output.protocol_message Markup.assign_update
    96               [(new_id, assign_update) |>
    97                 let open XML.Encode
    98                 in pair int (list (pair int (list int))) end
    99                 |> YXML.string_of_body];
   100         in Document.start_execution state' end)));
   101 
   102 val _ =
   103   Isabelle_Process.protocol_command "Document.remove_versions"
   104     (fn [versions_yxml] => Document.change_state (fn state =>
   105       let
   106         val versions =
   107           YXML.parse_body versions_yxml |>
   108             let open XML.Decode in list int end;
   109         val state1 = Document.remove_versions versions state;
   110         val _ = Output.protocol_message Markup.removed_versions [versions_yxml];
   111       in state1 end));
   112 
   113 val _ =
   114   Isabelle_Process.protocol_command "Document.dialog_result"
   115     (fn [serial, result] =>
   116       Active.dialog_result (Value.parse_int serial) result
   117         handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
   118 
   119 val _ =
   120   Isabelle_Process.protocol_command "ML_Heap.share_common_data"
   121     (fn [] => ML_Heap.share_common_data ());
   122 
   123 end;
   124