src/Pure/PIDE/protocol.ML
author wenzelm
Mon, 29 Apr 2013 15:47:42 +0200
changeset 51818 517f232e867d
parent 51294 0850d43cb355
child 52111 1fd184eaa310
permissions -rw-r--r--
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
     1
(*  Title:      Pure/PIDE/protocol.ML
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     3
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
     4
Protocol message formats for interactive proof documents.
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     5
*)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     6
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
     7
structure Protocol: sig end =
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     8
struct
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     9
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    10
val _ =
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45709
diff changeset
    11
  Isabelle_Process.protocol_command "Document.define_command"
44644
317e4962dd0f clarified define_command: store name as structural information;
wenzelm
parents: 44612
diff changeset
    12
    (fn [id, name, text] =>
317e4962dd0f clarified define_command: store name as structural information;
wenzelm
parents: 44612
diff changeset
    13
      Document.change_state (Document.define_command (Document.parse_id id) name text));
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    14
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    15
val _ =
47343
b8aeab386414 less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents: 46938
diff changeset
    16
  Isabelle_Process.protocol_command "Document.discontinue_execution"
b8aeab386414 less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents: 46938
diff changeset
    17
    (fn [] => Document.discontinue_execution (Document.state ()));
b8aeab386414 less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents: 46938
diff changeset
    18
b8aeab386414 less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents: 46938
diff changeset
    19
val _ =
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45709
diff changeset
    20
  Isabelle_Process.protocol_command "Document.cancel_execution"
47404
e6e5750f1311 simplified Future.cancel/cancel_group (again) -- running threads only;
wenzelm
parents: 47388
diff changeset
    21
    (fn [] => Document.cancel_execution (Document.state ()));
44612
990ac978854c explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents: 44610
diff changeset
    22
990ac978854c explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents: 44610
diff changeset
    23
val _ =
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45709
diff changeset
    24
  Isabelle_Process.protocol_command "Document.update"
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    25
    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    26
      let
47404
e6e5750f1311 simplified Future.cancel/cancel_group (again) -- running threads only;
wenzelm
parents: 47388
diff changeset
    27
        val _ = Document.cancel_execution state;
e6e5750f1311 simplified Future.cancel/cancel_group (again) -- running threads only;
wenzelm
parents: 47388
diff changeset
    28
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    29
        val old_id = Document.parse_id old_id_string;
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    30
        val new_id = Document.parse_id new_id_string;
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    31
        val edits =
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    32
          YXML.parse_body edits_yxml |>
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    33
            let open XML.Decode in
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    34
              list (pair string
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    35
                (variant
48755
393a37003851 apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
wenzelm
parents: 48707
diff changeset
    36
                 [fn ([], []) => Document.Clear,  (* FIXME unused !? *)
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    37
                  fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    38
                  fn ([], a) =>
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46774
diff changeset
    39
                    let
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
    40
                      val (master, (name, (imports, (keywords, errors)))) =
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 47420
diff changeset
    41
                        pair string (pair string (pair (list string)
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48755
diff changeset
    42
                          (pair (list (pair string
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48755
diff changeset
    43
                            (option (pair (pair string (list string)) (list string)))))
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
    44
                            (list string)))) a;
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48864
diff changeset
    45
                      val imports' = map (rpair Position.none) imports;
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
    46
                      val header = Thy_Header.make (name, Position.none) imports' keywords;
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
    47
                    in Document.Deps (master, header, errors) end,
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 44301
diff changeset
    48
                  fn (a, []) => Document.Perspective (map int_atom a)]))
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    49
            end;
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    50
47420
0dbe6c69eda2 just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents: 47404
diff changeset
    51
        val (assignment, state') = Document.update old_id new_id edits state;
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    52
        val _ =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49931
diff changeset
    53
          Output.protocol_message Markup.assign_execs
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44660
diff changeset
    54
            ((new_id, assignment) |>
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44436
diff changeset
    55
              let open XML.Encode
47388
fe4b245af74c discontinued obsolete last_execs (cf. cd3ab7625519);
wenzelm
parents: 47346
diff changeset
    56
              in pair int (list (pair int (option int))) end
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44660
diff changeset
    57
              |> YXML.string_of_body);
47420
0dbe6c69eda2 just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents: 47404
diff changeset
    58
49931
85780e6f8fd2 more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents: 49647
diff changeset
    59
        val _ = List.app Future.cancel_group (Goal.reset_futures ());
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50500
diff changeset
    60
        val _ = Isabelle_Process.reset_tracing ();
47420
0dbe6c69eda2 just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents: 47404
diff changeset
    61
        val _ = Document.start_execution state';
0dbe6c69eda2 just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents: 47404
diff changeset
    62
      in state' end));
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    63
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
    64
val _ =
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45709
diff changeset
    65
  Isabelle_Process.protocol_command "Document.remove_versions"
44673
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
    66
    (fn [versions_yxml] => Document.change_state (fn state =>
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
    67
      let
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
    68
        val versions =
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
    69
          YXML.parse_body versions_yxml |>
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
    70
            let open XML.Decode in list int end;
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    71
        val state1 = Document.remove_versions versions state;
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49931
diff changeset
    72
        val _ = Output.protocol_message Markup.removed_versions versions_yxml;
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    73
      in state1 end));
44673
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
    74
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
    75
val _ =
50498
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50201
diff changeset
    76
  Isabelle_Process.protocol_command "Document.dialog_result"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
    77
    (fn [serial, result] =>
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
    78
      Active.dialog_result (Markup.parse_int serial) result
50498
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50201
diff changeset
    79
        handle exn => if Exn.is_interrupt exn then () else reraise exn);
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50201
diff changeset
    80
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50201
diff changeset
    81
val _ =
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45709
diff changeset
    82
  Isabelle_Process.protocol_command "Document.invoke_scala"
49470
ee564db2649b more management of Invoke_Scala tasks;
wenzelm
parents: 49061
diff changeset
    83
    (fn [id, tag, res] =>
ee564db2649b more management of Invoke_Scala tasks;
wenzelm
parents: 49061
diff changeset
    84
      Invoke_Scala.fulfill_method id tag res
ee564db2649b more management of Invoke_Scala tasks;
wenzelm
parents: 49061
diff changeset
    85
        handle exn => if Exn.is_interrupt exn then () else reraise exn);
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
    86
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    87
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    88