added functor Linear_Set, based on former adhoc structures in document.ML;
Linear_Set.delete_after (ML): actually delete table entries;
Scala Linear_Set: clarified exceptions, according to ML version;
simplified Document.node using Linear_Set;
ML Document.edit: refer to start via NONE instead of no_id, according to Scala version;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/linear_set.ML Tue Aug 17 15:10:49 2010 +0200
@@ -0,0 +1,142 @@
+(* Title: Pure/General/linear_set.ML
+ Author: Makarius
+
+Sets with canonical linear order, or immutable linked-lists.
+*)
+
+signature LINEAR_SET =
+sig
+ type key
+ type 'a T
+ exception DUPLICATE of key
+ exception UNDEFINED of key
+ exception NEXT_UNDEFINED of key option
+ val empty: 'a T
+ val is_empty: 'a T -> bool
+ val defined: 'a T -> key -> bool
+ val lookup: 'a T -> key -> 'a option
+ val update: key * 'a -> 'a T -> 'a T
+ val fold: key option ->
+ ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
+ val get_first: key option ->
+ ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option
+ val get_after: 'a T -> key option -> key option
+ val insert_after: key option -> key * 'a -> 'a T -> 'a T
+ val delete_after: key option -> 'a T -> 'a T
+end;
+
+functor Linear_Set(Key: KEY): LINEAR_SET =
+struct
+
+(* type key *)
+
+type key = Key.key;
+structure Table = Table(Key);
+
+exception DUPLICATE of key;
+exception UNDEFINED of key;
+exception NEXT_UNDEFINED of key option;
+
+
+(* raw entries *)
+
+fun the_entry entries key =
+ (case Table.lookup entries key of
+ NONE => raise UNDEFINED key
+ | SOME entry => entry);
+
+fun next_entry entries key = snd (the_entry entries key);
+
+fun put_entry entry entries = Table.update entry entries;
+
+fun new_entry entry entries = Table.update_new entry entries
+ handle Table.DUP key => raise DUPLICATE key;
+
+fun del_entry key entries = Table.delete_safe key entries;
+
+
+(* set representation and basic operations *)
+
+datatype 'a T = Set of {start: key option, entries: ('a * key option) Table.table};
+
+fun make_set (start, entries) = Set {start = start, entries = entries};
+fun map_set f (Set {start, entries}) = make_set (f (start, entries));
+
+fun start_of (Set {start, ...}) = start;
+fun entries_of (Set {entries, ...}) = entries;
+
+val empty = Set {start = NONE, entries = Table.empty};
+fun is_empty set = is_none (start_of set);
+
+fun defined set key = Table.defined (entries_of set) key;
+
+fun lookup set key = Option.map fst (Table.lookup (entries_of set) key);
+
+fun update (key, x) = map_set (fn (start, entries) =>
+ (start, put_entry (key, (x, next_entry entries key)) entries));
+
+
+(* iterate entries *)
+
+fun optional_start set NONE = start_of set
+ | optional_start _ some = some;
+
+fun fold opt_start f set =
+ let
+ val entries = entries_of set;
+ fun apply _ NONE y = y
+ | apply prev (SOME key) y =
+ let
+ val (x, next) = the_entry entries key;
+ val item = ((prev, key), x);
+ in apply (SOME key) next (f item y) end;
+ in apply NONE (optional_start set opt_start) end;
+
+fun get_first opt_start P set =
+ let
+ val entries = entries_of set;
+ fun first _ NONE = NONE
+ | first prev (SOME key) =
+ let
+ val (x, next) = the_entry entries key;
+ val item = ((prev, key), x);
+ in if P item then SOME item else first (SOME key) next end;
+ in first NONE (optional_start set opt_start) end;
+
+
+(* relative addressing *)
+
+fun get_after set hook =
+ (case hook of
+ NONE => start_of set
+ | SOME key => next_entry (entries_of set) key);
+
+fun insert_after hook (key, x) = map_set (fn (start, entries) =>
+ (case hook of
+ NONE => (SOME key, new_entry (key, (x, start)) entries)
+ | SOME key1 =>
+ let
+ val (x1, next) = the_entry entries key1;
+ val entries' = entries
+ |> put_entry (key1, (x1, SOME key))
+ |> new_entry (key, (x, next));
+ in (start, entries') end));
+
+fun delete_after hook set = set |> map_set (fn (start, entries) =>
+ (case hook of
+ NONE =>
+ (case start of
+ NONE => raise NEXT_UNDEFINED NONE
+ | SOME key1 => (next_entry entries key1, del_entry key1 entries))
+ | SOME key1 =>
+ (case the_entry entries key1 of
+ (_, NONE) => raise NEXT_UNDEFINED (SOME key1)
+ | (x1, SOME key2) =>
+ let
+ val entries' = entries
+ |> put_entry (key1, (x1, next_entry entries key2))
+ |> del_entry key2;
+ in (start, entries') end)));
+
+end;
+
--- a/src/Pure/General/linear_set.scala Mon Aug 16 22:56:28 2010 +0200
+++ b/src/Pure/General/linear_set.scala Tue Aug 17 15:10:49 2010 +0200
@@ -25,8 +25,9 @@
implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
override def empty[A] = new Linear_Set[A]
- class Duplicate(s: String) extends Exception(s)
- class Undefined(s: String) extends Exception(s)
+ class Duplicate[A](x: A) extends Exception
+ class Undefined[A](x: A) extends Exception
+ class Next_Undefined[A](x: Option[A]) extends Exception
}
@@ -43,19 +44,22 @@
protected val rep = Linear_Set.empty_rep[A]
- /* auxiliary operations */
+ /* relative addressing */
+ // FIXME check definedness??
def next(elem: A): Option[A] = rep.nexts.get(elem)
def prev(elem: A): Option[A] = rep.prevs.get(elem)
def get_after(hook: Option[A]): Option[A] =
hook match {
case None => rep.start
- case Some(elem) => next(elem)
+ case Some(elem) =>
+ if (!contains(elem)) throw new Linear_Set.Undefined(elem)
+ next(elem)
}
def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
- if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
+ if (contains(elem)) throw new Linear_Set.Duplicate(elem)
else
hook match {
case None =>
@@ -66,7 +70,7 @@
rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
}
case Some(elem1) =>
- if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
else
rep.nexts.get(elem1) match {
case None =>
@@ -83,7 +87,7 @@
hook match {
case None =>
rep.start match {
- case None => throw new Linear_Set.Undefined("")
+ case None => throw new Linear_Set.Next_Undefined[A](None)
case Some(elem1) =>
rep.nexts.get(elem1) match {
case None => empty
@@ -92,10 +96,10 @@
}
}
case Some(elem1) =>
- if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
else
rep.nexts.get(elem1) match {
- case None => throw new Linear_Set.Undefined("")
+ case None => throw new Linear_Set.Next_Undefined(Some(elem1))
case Some(elem2) =>
rep.nexts.get(elem2) match {
case None =>
@@ -153,15 +157,15 @@
def iterator(elem: A): Iterator[A] =
if (contains(elem)) make_iterator(Some(elem), rep.nexts)
- else throw new Linear_Set.Undefined(elem.toString)
+ else throw new Linear_Set.Undefined(elem)
def reverse_iterator(elem: A): Iterator[A] =
if (contains(elem)) make_iterator(Some(elem), rep.prevs)
- else throw new Linear_Set.Undefined(elem.toString)
+ else throw new Linear_Set.Undefined(elem)
def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
def - (elem: A): Linear_Set[A] =
- if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
+ if (!contains(elem)) throw new Linear_Set.Undefined(elem)
else delete_after(prev(elem))
}
\ No newline at end of file
--- a/src/Pure/IsaMakefile Mon Aug 16 22:56:28 2010 +0200
+++ b/src/Pure/IsaMakefile Tue Aug 17 15:10:49 2010 +0200
@@ -80,6 +80,7 @@
General/graph.ML \
General/heap.ML \
General/integer.ML \
+ General/linear_set.ML \
General/long_name.ML \
General/markup.ML \
General/name_space.ML \
--- a/src/Pure/PIDE/document.ML Mon Aug 16 22:56:28 2010 +0200
+++ b/src/Pure/PIDE/document.ML Tue Aug 17 15:10:49 2010 +0200
@@ -15,7 +15,7 @@
val new_id: unit -> id
val parse_id: string -> id
val print_id: id -> string
- type edit = string * ((command_id * command_id option) list) option
+ type edit = string * ((command_id option * command_id option) list) option
type state
val init_state: state
val define_command: command_id -> string -> state -> state
@@ -55,82 +55,43 @@
(** document structure **)
-abstype entry = Entry of {next: command_id option, exec: exec_id option}
- and node = Node of entry Inttab.table (*unique entries indexed by command_id, start with no_id*)
+structure Entries = Linear_Set(type key = command_id val ord = int_ord);
+
+abstype node = Node of exec_id option Entries.T (*command entries with excecutions*)
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-
-(* command entries *)
-
-fun make_entry next exec = Entry {next = next, exec = exec};
-
-fun the_entry (Node entries) (id: command_id) =
- (case Inttab.lookup entries id of
- NONE => err_undef "command entry" id
- | SOME (Entry entry) => entry);
+val empty_node = Node Entries.empty;
+val empty_version = Version Graph.empty;
-fun put_entry (id: command_id, entry: entry) (Node entries) =
- Node (Inttab.update (id, entry) entries);
-
-fun put_entry_exec (id: command_id) exec node =
- let val {next, ...} = the_entry node id
- in put_entry (id, make_entry next exec) node end;
-
-fun reset_entry_exec id = put_entry_exec id NONE;
-fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
+fun fold_entries start f (Node entries) = Entries.fold start f entries;
+fun first_entry start P (Node entries) = Entries.get_first start P entries;
-(* iterate entries *)
-
-fun fold_entries id0 f (node as Node entries) =
- let
- fun apply NONE x = x
- | apply (SOME id) x =
- let val entry = the_entry node id
- in apply (#next entry) (f (id, entry) x) end;
- in if Inttab.defined entries id0 then apply (SOME id0) else I end;
-
-fun first_entry P node =
- let
- fun first _ NONE = NONE
- | first prev (SOME id) =
- let val entry = the_entry node id
- in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
- in first NONE (SOME no_id) end;
-
-
-(* modify entries *)
-
-fun insert_after (id: command_id) (id2: command_id) node =
- let val {next, exec} = the_entry node id in
- node
- |> put_entry (id, make_entry (SOME id2) exec)
- |> put_entry (id2, make_entry next NONE)
- end;
-
-fun delete_after (id: command_id) node =
- let val {next, exec} = the_entry node id in
- (case next of
- NONE => error ("No next entry to delete: " ^ print_id id)
- | SOME id2 =>
- node |>
- (case #next (the_entry node id2) of
- NONE => put_entry (id, make_entry NONE exec)
- | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
- end;
-
-
-(* node edits *)
+(* node edits and associated executions *)
type edit =
- string * (*node name*)
- ((command_id * command_id option) list) option; (*NONE: remove, SOME: insert/remove commands*)
+ string *
+ (*NONE: remove node, SOME: insert/remove commands*)
+ ((command_id option * command_id option) list) option;
+
+fun the_entry (Node entries) id =
+ (case Entries.lookup entries id of
+ NONE => err_undef "command entry" id
+ | SOME entry => entry);
-val empty_node = Node (Inttab.make [(no_id, make_entry NONE (SOME no_id))]);
+fun update_entry (id, exec_id) (Node entries) =
+ Node (Entries.update (id, SOME exec_id) entries);
-fun edit_node (id, SOME id2) = insert_after id id2
- | edit_node (id, NONE) = delete_after id;
+fun reset_after id entries =
+ (case Entries.get_after entries id of
+ NONE => entries
+ | SOME next => Entries.update (next, NONE) entries);
+
+fun edit_node (hook, SOME id2) (Node entries) =
+ Node (Entries.insert_after hook (id2, NONE) entries)
+ | edit_node (hook, NONE) (Node entries) =
+ Node (entries |> Entries.delete_after hook |> reset_after hook);
(* version operations *)
@@ -138,16 +99,15 @@
fun nodes_of (Version nodes) = nodes;
val node_names_of = Graph.keys o nodes_of;
+fun get_node version name = Graph.get_node (nodes_of version) name
+ handle Graph.UNDEF _ => empty_node;
+
fun edit_nodes (name, SOME edits) (Version nodes) =
Version (nodes
|> Graph.default_node (name, empty_node)
|> Graph.map_node name (fold edit_node edits))
- | edit_nodes (name, NONE) (Version nodes) = Version (Graph.del_node name nodes);
-
-val empty_version = Version Graph.empty;
-
-fun the_node version name =
- Graph.get_node (nodes_of version) name handle Graph.UNDEF _ => empty_node;
+ | edit_nodes (name, NONE) (Version nodes) =
+ Version (Graph.del_node name nodes); (* FIXME Graph.UNDEF !? *)
fun put_node name node (Version nodes) =
Version (Graph.map_node name (K node) nodes); (* FIXME Graph.UNDEF !? *)
@@ -173,8 +133,8 @@
val init_state =
make_state (Inttab.make [(no_id, empty_version)],
- Inttab.make [(no_id, Future.value Toplevel.empty)],
- Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],
+ Inttab.make [(no_id, Future.value Toplevel.empty)], (* FIXME no_id !?? *)
+ Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))], (* FIXME no_id !?? *)
[]);
@@ -238,10 +198,10 @@
local
-fun is_changed node' (id, {next = _, exec}) =
+fun is_changed node' ((_, id), exec) =
(case try (the_entry node') id of
NONE => true
- | SOME {next = _, exec = exec'} => exec' <> exec);
+ | SOME exec' => exec' <> exec);
fun new_exec name (id: command_id) (exec_id, updates, state) =
let
@@ -266,15 +226,18 @@
val new_version = fold edit_nodes edits old_version;
fun update_node name (rev_updates, version, st) =
- let val node = the_node version name in
- (case first_entry (is_changed (the_node old_version name)) node of
+ let val node = get_node version name in
+ (case first_entry NONE (is_changed (get_node old_version name)) node of
NONE => (rev_updates, version, st)
- | SOME (prev, id, _) =>
+ | SOME ((prev, id), _) =>
let
- val prev_exec = the (#exec (the_entry node (the prev)));
+ val prev_exec =
+ (case prev of
+ NONE => no_id
+ | SOME prev_id => the_default no_id (the_entry node prev_id));
val (_, rev_upds, st') =
- fold_entries id (new_exec name o #1) node (prev_exec, [], st);
- val node' = fold set_entry_exec rev_upds node;
+ fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
+ val node' = fold update_entry rev_upds node;
in (rev_upds @ rev_updates, put_node name node' version, st') end)
end;
@@ -306,8 +269,8 @@
node_names_of version |> map (fn name =>
Future.fork_pri 1 (fn () =>
(await_cancellation ();
- fold_entries no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
- (the_node version name) ())));
+ fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
+ (get_node version name) ())));
in (versions, commands, execs, execution') end);
end;
--- a/src/Pure/ROOT.ML Mon Aug 16 22:56:28 2010 +0200
+++ b/src/Pure/ROOT.ML Tue Aug 17 15:10:49 2010 +0200
@@ -42,6 +42,7 @@
use "General/ord_list.ML";
use "General/balanced_tree.ML";
use "General/graph.ML";
+use "General/linear_set.ML";
use "General/long_name.ML";
use "General/binding.ML";
use "General/name_space.ML";
--- a/src/Pure/System/isar_document.ML Mon Aug 16 22:56:28 2010 +0200
+++ b/src/Pure/System/isar_document.ML Tue Aug 17 15:10:49 2010 +0200
@@ -21,10 +21,14 @@
val old_id = Document.parse_id old_id_string;
val new_id = Document.parse_id new_id_string;
val edits =
- XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
- (XML_Data.dest_option (XML_Data.dest_list
- (XML_Data.dest_pair XML_Data.dest_int
- (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
+ XML_Data.dest_list
+ (XML_Data.dest_pair
+ XML_Data.dest_string
+ (XML_Data.dest_option
+ (XML_Data.dest_list
+ (XML_Data.dest_pair
+ (XML_Data.dest_option XML_Data.dest_int)
+ (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
val (updates, state') = Document.edit old_id new_id edits state;
val _ =
--- a/src/Pure/System/isar_document.scala Mon Aug 16 22:56:28 2010 +0200
+++ b/src/Pure/System/isar_document.scala Tue Aug 17 15:10:49 2010 +0200
@@ -51,14 +51,13 @@
def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
edits: List[Document.Edit[Document.Command_ID]])
{
- def make_id1(id1: Option[Document.Command_ID]): XML.Body =
- XML_Data.make_long(id1 getOrElse Document.NO_ID)
-
val arg =
XML_Data.make_list(
XML_Data.make_pair(XML_Data.make_string)(
XML_Data.make_option(XML_Data.make_list(
- XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
+ XML_Data.make_pair(
+ XML_Data.make_option(XML_Data.make_long))(
+ XML_Data.make_option(XML_Data.make_long))))))(edits)
input("Isar_Document.edit_version",
Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))