src/Pure/PIDE/isar_document.ML
author wenzelm
Sun, 10 Jul 2011 20:59:04 +0200
changeset 43731 70072780e095
parent 43724 4e58485fa320
child 43748 c70bd78ec83c
permissions -rw-r--r--
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38483
3d16bebee1d3 moved Isar_Document to Pure/PIDE;
wenzelm
parents: 38448
diff changeset
     1
(*  Title:      Pure/PIDE/isar_document.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
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
     4
Protocol message formats for interactive Isar 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
43713
1ba5331b4623 moved global state to structure Document (again);
wenzelm
parents: 43668
diff changeset
     7
structure Isar_Document: 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 _ =
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    11
  Isabelle_Process.add_command "Isar_Document.define_command"
43713
1ba5331b4623 moved global state to structure Document (again);
wenzelm
parents: 43668
diff changeset
    12
    (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    13
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    14
val _ =
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    15
  Isabelle_Process.add_command "Isar_Document.edit_version"
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43713
diff changeset
    16
    (fn [old_id_string, new_id_string, edits_yxml, headers_yxml] => Document.change_state (fn state =>
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    17
      let
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    18
        val old_id = Document.parse_id old_id_string;
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    19
        val new_id = Document.parse_id new_id_string;
43724
4e58485fa320 simplified XML_Data;
wenzelm
parents: 43722
diff changeset
    20
        val edits = YXML.parse_body edits_yxml |>
43731
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents: 43724
diff changeset
    21
          let open XML_Data.Decode
43724
4e58485fa320 simplified XML_Data;
wenzelm
parents: 43722
diff changeset
    22
          in list (pair string (option (list (pair (option int) (option int))))) end;
4e58485fa320 simplified XML_Data;
wenzelm
parents: 43722
diff changeset
    23
        val headers = YXML.parse_body headers_yxml |>
43731
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents: 43724
diff changeset
    24
          let open XML_Data.Decode
43724
4e58485fa320 simplified XML_Data;
wenzelm
parents: 43722
diff changeset
    25
          in list (pair string (triple string (list string) (list string))) end;
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    26
43666
7be2e51928cb clarified cancel_execution/await_cancellation;
wenzelm
parents: 43665
diff changeset
    27
      val await_cancellation = Document.cancel_execution state;
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43713
diff changeset
    28
      val (updates, state') = Document.edit old_id new_id edits headers state;
43666
7be2e51928cb clarified cancel_execution/await_cancellation;
wenzelm
parents: 43665
diff changeset
    29
      val _ = await_cancellation ();
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    30
      val _ =
43665
573d1272f36d tuned signature;
wenzelm
parents: 41634
diff changeset
    31
        Output.status (Markup.markup (Markup.assign new_id)
573d1272f36d tuned signature;
wenzelm
parents: 41634
diff changeset
    32
          (implode (map (Markup.markup_only o Markup.edit) updates)));
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    33
      val state'' = Document.execute new_id state';
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    34
    in state'' end));
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    35
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    36
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    37