src/Pure/PIDE/isar_document.ML
author wenzelm
Tue, 05 Jul 2011 20:36:49 +0200
changeset 43668 aad4f1956098
parent 43666 7be2e51928cb
child 43713 1ba5331b4623
permissions -rw-r--r--
get theory from last executation state; tuned error messages;
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
43668
aad4f1956098 get theory from last executation state;
wenzelm
parents: 43666
diff changeset
     7
signature ISAR_DOCUMENT =
aad4f1956098 get theory from last executation state;
wenzelm
parents: 43666
diff changeset
     8
sig
aad4f1956098 get theory from last executation state;
wenzelm
parents: 43666
diff changeset
     9
  val state: unit -> Document.state
aad4f1956098 get theory from last executation state;
wenzelm
parents: 43666
diff changeset
    10
end
aad4f1956098 get theory from last executation state;
wenzelm
parents: 43666
diff changeset
    11
aad4f1956098 get theory from last executation state;
wenzelm
parents: 43666
diff changeset
    12
structure Isar_Document: ISAR_DOCUMENT =
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    13
struct
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    14
38420
7bdf6c79a2db use Synchronized.var and prevent global CRITICAL sections in this hot spot;
wenzelm
parents: 38418
diff changeset
    15
val global_state = Synchronized.var "Isar_Document" Document.init_state;
7bdf6c79a2db use Synchronized.var and prevent global CRITICAL sections in this hot spot;
wenzelm
parents: 38418
diff changeset
    16
val change_state = Synchronized.change global_state;
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    17
43668
aad4f1956098 get theory from last executation state;
wenzelm
parents: 43666
diff changeset
    18
fun state () = Synchronized.value global_state;
aad4f1956098 get theory from last executation state;
wenzelm
parents: 43666
diff changeset
    19
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    20
val _ =
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    21
  Isabelle_Process.add_command "Isar_Document.define_command"
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    22
    (fn [id, text] => 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
    23
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    24
val _ =
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    25
  Isabelle_Process.add_command "Isar_Document.edit_version"
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    26
    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    27
      let
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    28
        val old_id = Document.parse_id old_id_string;
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    29
        val new_id = Document.parse_id new_id_string;
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    30
        val edits =
38448
62d16c415019 added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents: 38420
diff changeset
    31
          XML_Data.dest_list
62d16c415019 added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents: 38420
diff changeset
    32
            (XML_Data.dest_pair
62d16c415019 added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents: 38420
diff changeset
    33
              XML_Data.dest_string
62d16c415019 added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents: 38420
diff changeset
    34
              (XML_Data.dest_option
62d16c415019 added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents: 38420
diff changeset
    35
                (XML_Data.dest_list
62d16c415019 added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents: 38420
diff changeset
    36
                  (XML_Data.dest_pair
62d16c415019 added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents: 38420
diff changeset
    37
                    (XML_Data.dest_option XML_Data.dest_int)
62d16c415019 added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents: 38420
diff changeset
    38
                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    39
43666
7be2e51928cb clarified cancel_execution/await_cancellation;
wenzelm
parents: 43665
diff changeset
    40
      val await_cancellation = Document.cancel_execution state;
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    41
      val (updates, state') = Document.edit old_id new_id edits state;
43666
7be2e51928cb clarified cancel_execution/await_cancellation;
wenzelm
parents: 43665
diff changeset
    42
      val _ = await_cancellation ();
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    43
      val _ =
43665
573d1272f36d tuned signature;
wenzelm
parents: 41634
diff changeset
    44
        Output.status (Markup.markup (Markup.assign new_id)
573d1272f36d tuned signature;
wenzelm
parents: 41634
diff changeset
    45
          (implode (map (Markup.markup_only o Markup.edit) updates)));
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    46
      val state'' = Document.execute new_id state';
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    47
    in state'' end));
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    48
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    49
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    50