src/Pure/PIDE/protocol.ML
author wenzelm
Mon Apr 06 16:00:19 2015 +0200 (2015-04-06 ago)
changeset 59934 b65c4370f831
parent 59715 4f0d0e4ad68d
child 60074 38a64cc17403
permissions -rw-r--r--
more position information and PIDE markup for command keywords;
     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       let val options = Options.decode (YXML.parse_body options_yxml) in
    18         Options.set_default options;
    19         Future.ML_statistics := true;
    20         Multithreading.trace := Options.int options "threads_trace";
    21         Multithreading.max_threads_update (Options.int options "threads");
    22         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
    23       end);
    24 
    25 val _ =
    26   Isabelle_Process.protocol_command "Document.define_blob"
    27     (fn [digest, content] => Document.change_state (Document.define_blob digest content));
    28 
    29 val _ =
    30   Isabelle_Process.protocol_command "Document.define_command"
    31     (fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
    32       let
    33         val (blobs, blobs_index) =
    34           YXML.parse_body blobs_yxml |>
    35             let
    36               val message =
    37                 YXML.string_of_body o Protocol_Message.command_positions id;
    38               open XML.Decode;
    39             in
    40               pair
    41                 (list (variant
    42                  [fn ([], a) => Exn.Res (pair string (option string) a),
    43                   fn ([], a) => Exn.Exn (ERROR (message a))]))
    44                 int
    45             end;
    46         val toks =
    47           (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
    48       in
    49         Document.change_state
    50           (Document.define_command (Document_ID.parse id) name blobs blobs_index toks)
    51       end);
    52 
    53 val _ =
    54   Isabelle_Process.protocol_command "Document.discontinue_execution"
    55     (fn [] => Execution.discontinue ());
    56 
    57 val _ =
    58   Isabelle_Process.protocol_command "Document.cancel_exec"
    59     (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id));
    60 
    61 val _ =
    62   Isabelle_Process.protocol_command "Document.update"
    63     (Future.task_context "Document.update" (Future.new_group NONE)
    64       (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    65         let
    66           val _ = Execution.discontinue ();
    67 
    68           val old_id = Document_ID.parse old_id_string;
    69           val new_id = Document_ID.parse new_id_string;
    70           val edits =
    71             YXML.parse_body edits_yxml |>
    72               let open XML.Decode in
    73                 list (pair string
    74                   (variant
    75                    [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    76                     fn ([], a) =>
    77                       let
    78                         val (master, (name, (imports, (keywords, errors)))) =
    79                           pair string (pair string (pair (list string)
    80                             (pair (list (pair string
    81                               (option (pair (pair string (list string)) (list string)))))
    82                               (list YXML.string_of_body)))) a;
    83                         val imports' = map (rpair Position.none) imports;
    84                         val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
    85                         val header = Thy_Header.make (name, Position.none) imports' keywords';
    86                       in Document.Deps {master = master, header = header, errors = errors} end,
    87                     fn (a :: b, c) =>
    88                       Document.Perspective (bool_atom a, map int_atom b,
    89                         list (pair int (pair string (list string))) c)]))
    90               end;
    91 
    92           val (removed, assign_update, state') = Document.update old_id new_id edits state;
    93           val _ =
    94             (singleton o Future.forks)
    95              {name = "Document.update/remove", group = NONE,
    96               deps = maps Future.group_snapshot (maps Execution.peek removed),
    97               pri = 1, interrupts = false}
    98              (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
    99 
   100           val _ =
   101             Output.protocol_message Markup.assign_update
   102               [(new_id, assign_update) |>
   103                 let open XML.Encode
   104                 in pair int (list (pair int (list int))) end
   105                 |> YXML.string_of_body];
   106         in Document.start_execution state' end)));
   107 
   108 val _ =
   109   Isabelle_Process.protocol_command "Document.remove_versions"
   110     (fn [versions_yxml] => Document.change_state (fn state =>
   111       let
   112         val versions =
   113           YXML.parse_body versions_yxml |>
   114             let open XML.Decode in list int end;
   115         val state1 = Document.remove_versions versions state;
   116         val _ = Output.protocol_message Markup.removed_versions [versions_yxml];
   117       in state1 end));
   118 
   119 val _ =
   120   Isabelle_Process.protocol_command "Document.dialog_result"
   121     (fn [serial, result] =>
   122       Active.dialog_result (Markup.parse_int serial) result
   123         handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
   124 
   125 val _ =
   126   Isabelle_Process.protocol_command "ML_System.share_common_data"
   127     (fn [] => ML_System.share_common_data ());
   128 
   129 end;
   130