src/Pure/Isar/isar_document.ML
changeset 29490 8f0a481199e7
parent 29489 5dfe03f423c4
child 29499 2819ba5f0c32
equal deleted inserted replaced
29489:5dfe03f423c4 29490:8f0a481199e7
    47 
    47 
    48 fun put_entry_state (id: command_id) state entries =
    48 fun put_entry_state (id: command_id) state entries =
    49   let val {next, ...} = the_entry entries id
    49   let val {next, ...} = the_entry entries id
    50   in put_entry (id, make_entry next state) entries end;
    50   in put_entry (id, make_entry next state) entries end;
    51 
    51 
    52 fun reset_state id = put_entry_state id NONE;
    52 fun reset_entry_state id = put_entry_state id NONE;
    53 fun set_state (id, state_id) = put_entry_state id (SOME state_id);
    53 fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
    54 
    54 
    55 
    55 
    56 
    56 
    57 (* document *)
    57 (* document *)
    58 
    58 
   101       NONE => error ("No next entry to delete: " ^ quote id)
   101       NONE => error ("No next entry to delete: " ^ quote id)
   102     | SOME id2 =>
   102     | SOME id2 =>
   103         entries |>
   103         entries |>
   104           (case #next (the_entry entries id2) of
   104           (case #next (the_entry entries id2) of
   105             NONE => put_entry (id, make_entry NONE state)
   105             NONE => put_entry (id, make_entry NONE state)
   106           | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_state id3))
   106           | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
   107   end);
   107   end);
   108 
   108 
   109 
   109 
   110 
   110 
   111 (** global configuration **)
   111 (** global configuration **)
   209     | SOME (prev, id) =>
   209     | SOME (prev, id) =>
   210         let
   210         let
   211           val _ = fold_entries (SOME id) cancel_state old_document ();
   211           val _ = fold_entries (SOME id) cancel_state old_document ();
   212           val prev_state_id = the (#state (the_entry new_entries (the prev)));
   212           val prev_state_id = the (#state (the_entry new_entries (the prev)));
   213           val (_, updates) = fold_entries (SOME id) new_state new_document (prev_state_id, []);
   213           val (_, updates) = fold_entries (SOME id) new_state new_document (prev_state_id, []);
   214           val new_document' = new_document |> map_entries (fold set_state updates);
   214           val new_document' = new_document |> map_entries (fold set_entry_state updates);
   215         in (updates, new_document') end)
   215         in (updates, new_document') end)
   216   end;
   216   end;
   217 
   217 
   218 fun report_updates _ [] = ()
   218 fun report_updates _ [] = ()
   219   | report_updates (document_id: document_id) updates =
   219   | report_updates (document_id: document_id) updates =