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