src/Pure/PIDE/isar_document.ML
author wenzelm
Wed Aug 24 13:03:39 2011 +0200 (2011-08-24 ago)
changeset 44436 546adfa8a6fc
parent 44384 8f6054a63f96
child 44476 e8a87398f35d
permissions -rw-r--r--
update_perspective without actual edits, bypassing the full state assignment protocol;
edit_nodes/Perspective: do not touch_descendants here;
propagate editor scroll events via update_perspective;
misc tuning;
     1 (*  Title:      Pure/PIDE/isar_document.ML
     2     Author:     Makarius
     3 
     4 Protocol message formats for interactive Isar documents.
     5 *)
     6 
     7 structure Isar_Document: sig end =
     8 struct
     9 
    10 val _ =
    11   Isabelle_Process.add_command "Isar_Document.define_command"
    12     (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
    13 
    14 val _ =
    15   Isabelle_Process.add_command "Isar_Document.update_perspective"
    16     (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
    17       let
    18         val old_id = Document.parse_id old_id_string;
    19         val new_id = Document.parse_id new_id_string;
    20         val ids = YXML.parse_body ids_yxml
    21           |> let open XML.Decode in list int end;
    22 
    23         val _ = Future.join_tasks (Document.cancel_execution state);
    24       in
    25         state
    26         |> Document.update_perspective old_id new_id name ids
    27         |> Document.execute new_id
    28       end));
    29 
    30 val _ =
    31   Isabelle_Process.add_command "Isar_Document.edit_version"
    32     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    33       let
    34         val old_id = Document.parse_id old_id_string;
    35         val new_id = Document.parse_id new_id_string;
    36         val edits =
    37           YXML.parse_body edits_yxml |>
    38             let open XML.Decode in
    39               list (pair string
    40                 (variant
    41                  [fn ([], []) => Document.Clear,
    42                   fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    43                   fn ([], a) =>
    44                     Document.Header
    45                       (Exn.Res (triple string (list string) (list (pair string bool)) a)),
    46                   fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
    47                   fn (a, []) => Document.Perspective (map int_atom a)]))
    48             end;
    49 
    50         val running = Document.cancel_execution state;
    51         val (updates, state') = Document.edit old_id new_id edits state;
    52         val _ = Future.join_tasks running;
    53         val _ = Document.join_commands state';
    54         val _ =
    55           Output.status (Markup.markup (Markup.assign new_id)
    56             (implode (map (Markup.markup_only o Markup.edit) updates)));
    57         val state'' = Document.execute new_id state';
    58       in state'' end));
    59 
    60 val _ =
    61   Isabelle_Process.add_command "Isar_Document.invoke_scala"
    62     (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
    63 
    64 end;
    65