src/Pure/PIDE/isar_document.ML
author wenzelm
Fri, 26 Aug 2011 15:09:54 +0200
changeset 44479 9a04e7502e22
parent 44476 e8a87398f35d
child 44481 bb42bc831570
permissions -rw-r--r--
refined document state assignment: observe perspective, more explicit assignment message; misc tuning and clarification;
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 _ =
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    15
  Isabelle_Process.add_command "Isar_Document.update_perspective"
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    16
    (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    17
      let
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    18
        val old_id = Document.parse_id old_id_string;
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    19
        val new_id = Document.parse_id new_id_string;
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    20
        val ids = YXML.parse_body ids_yxml
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    21
          |> let open XML.Decode in list int end;
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    22
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    23
        val _ = Future.join_tasks (Document.cancel_execution state);
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    24
      in
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    25
        state
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    26
        |> Document.update_perspective old_id new_id name ids
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    27
        |> Document.execute new_id
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    28
      end));
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    29
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    30
val _ =
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    31
  Isabelle_Process.add_command "Isar_Document.edit_version"
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    32
    (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
    33
      let
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    34
        val old_id = Document.parse_id old_id_string;
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
    35
        val new_id = Document.parse_id new_id_string;
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    36
        val edits =
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    37
          YXML.parse_body edits_yxml |>
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    38
            let open XML.Decode in
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    39
              list (pair string
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    40
                (variant
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44182
diff changeset
    41
                 [fn ([], []) => Document.Clear,
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    42
                  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
    43
                  fn ([], a) =>
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44182
diff changeset
    44
                    Document.Header
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44182
diff changeset
    45
                      (Exn.Res (triple string (list string) (list (pair string bool)) a)),
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 44301
diff changeset
    46
                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 44301
diff changeset
    47
                  fn (a, []) => Document.Perspective (map int_atom a)]))
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
    48
            end;
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    49
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    50
        val running = Document.cancel_execution state;
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44436
diff changeset
    51
        val (assignment, state') = Document.edit 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 _ = Future.join_tasks running;
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    53
        val _ = Document.join_commands state';
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    54
        val _ =
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    55
          Output.status (Markup.markup (Markup.assign new_id)
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44436
diff changeset
    56
            (assignment |>
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44436
diff changeset
    57
              let open XML.Encode
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44476
diff changeset
    58
              in pair (list (pair int (option int))) (list (pair string (option int))) end
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44436
diff changeset
    59
              |> YXML.string_of_body));
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    60
        val state'' = Document.execute new_id state';
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
    61
      in state'' end));
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    62
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
    63
val _ =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
    64
  Isabelle_Process.add_command "Isar_Document.invoke_scala"
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
    65
    (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
    66
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    67
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    68