src/Pure/PIDE/document.ML
changeset 43668 aad4f1956098
parent 43666 7be2e51928cb
child 43713 1ba5331b4623
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Jul 05 19:45:59 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Jul 05 20:36:49 2011 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    type edit = string * ((command_id option * command_id option) list) option
     1.5    type state
     1.6    val init_state: state
     1.7 +  val get_theory: state -> version_id -> Position.T -> string -> theory
     1.8    val cancel_execution: state -> unit -> unit
     1.9    val define_command: command_id -> string -> state -> state
    1.10    val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
    1.11 @@ -49,15 +50,23 @@
    1.12  
    1.13  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.14  
    1.15 -abstype node = Node of exec_id option Entries.T  (*command entries with excecutions*)
    1.16 -  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.17 +abstype node = Node of
    1.18 +  {last: exec_id, entries: exec_id option Entries.T}  (*command entries with excecutions*)
    1.19 +and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.20  with
    1.21  
    1.22 -val empty_node = Node Entries.empty;
    1.23 -val empty_version = Version Graph.empty;
    1.24 +fun make_node (last, entries) =
    1.25 +  Node {last = last, entries = entries};
    1.26 +
    1.27 +fun get_last (Node {last, ...}) = last;
    1.28 +fun set_last last (Node {entries, ...}) = make_node (last, entries);
    1.29  
    1.30 -fun fold_entries start f (Node entries) = Entries.fold start f entries;
    1.31 -fun first_entry start P (Node entries) = Entries.get_first start P entries;
    1.32 +fun map_entries f (Node {last, entries}) = make_node (last, f entries);
    1.33 +fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
    1.34 +fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
    1.35 +
    1.36 +val empty_node = make_node (no_id, Entries.empty);
    1.37 +val empty_version = Version Graph.empty;
    1.38  
    1.39  
    1.40  (* node edits and associated executions *)
    1.41 @@ -67,23 +76,22 @@
    1.42    (*NONE: remove node, SOME: insert/remove commands*)
    1.43    ((command_id option * command_id option) list) option;
    1.44  
    1.45 -fun the_entry (Node entries) id =
    1.46 +fun the_entry (Node {entries, ...}) id =
    1.47    (case Entries.lookup entries id of
    1.48      NONE => err_undef "command entry" id
    1.49    | SOME entry => entry);
    1.50  
    1.51 -fun update_entry (id, exec_id) (Node entries) =
    1.52 -  Node (Entries.update (id, SOME exec_id) entries);
    1.53 +fun update_entry (id, exec_id) =
    1.54 +  map_entries (Entries.update (id, SOME exec_id));
    1.55  
    1.56  fun reset_after id entries =
    1.57    (case Entries.get_after entries id of
    1.58      NONE => entries
    1.59    | SOME next => Entries.update (next, NONE) entries);
    1.60  
    1.61 -fun edit_node (id, SOME id2) (Node entries) =
    1.62 -      Node (Entries.insert_after id (id2, NONE) entries)
    1.63 -  | edit_node (id, NONE) (Node entries) =
    1.64 -      Node (entries |> Entries.delete_after id |> reset_after id);
    1.65 +val edit_node = map_entries o fold
    1.66 +  (fn (id, SOME id2) => Entries.insert_after id (id2, NONE)
    1.67 +    | (id, NONE) => Entries.delete_after id #> reset_after id);
    1.68  
    1.69  
    1.70  (* version operations *)
    1.71 @@ -97,7 +105,7 @@
    1.72  fun edit_nodes (name, SOME edits) (Version nodes) =
    1.73        Version (nodes
    1.74          |> Graph.default_node (name, empty_node)
    1.75 -        |> Graph.map_node name (fold edit_node edits))
    1.76 +        |> Graph.map_node name (edit_node edits))
    1.77    | edit_nodes (name, NONE) (Version nodes) =
    1.78        Version (perhaps (try (Graph.del_node name)) nodes);
    1.79  
    1.80 @@ -182,6 +190,12 @@
    1.81      NONE => err_undef "command execution" id
    1.82    | SOME exec => exec);
    1.83  
    1.84 +fun get_theory state version_id pos name =
    1.85 +  let
    1.86 +    val last = get_last (get_node (the_version state version_id) name);
    1.87 +    val st = #2 (Lazy.force (the_exec state last));
    1.88 +  in Toplevel.end_theory pos st end;
    1.89 +
    1.90  
    1.91  (* document execution *)
    1.92  
    1.93 @@ -309,9 +323,9 @@
    1.94                  (case prev of
    1.95                    NONE => no_id
    1.96                  | SOME prev_id => the_default no_id (the_entry node prev_id));
    1.97 -              val (_, rev_upds, st') =
    1.98 +              val (last, rev_upds, st') =
    1.99                  fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
   1.100 -              val node' = fold update_entry rev_upds node;
   1.101 +              val node' = node |> fold update_entry rev_upds |> set_last last;
   1.102              in (rev_upds @ rev_updates, put_node name node' version, st') end)
   1.103        end;
   1.104