--- a/src/Pure/General/markup.ML Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/General/markup.ML Mon Aug 16 12:33:52 2010 +0200
@@ -104,13 +104,10 @@
val sendbackN: string val sendback: T
val hiliteN: string val hilite: T
val taskN: string
- val unprocessedN: string val unprocessed: T
- val runningN: string val running: string -> T
val forkedN: string val forked: T
val joinedN: string val joined: T
val failedN: string val failed: T
val finishedN: string val finished: T
- val disposedN: string val disposed: T
val versionN: string
val execN: string
val assignN: string val assign: int -> T
@@ -318,13 +315,11 @@
val taskN = "task";
-val (unprocessedN, unprocessed) = markup_elem "unprocessed";
-val (runningN, running) = markup_string "running" taskN;
val (forkedN, forked) = markup_elem "forked";
val (joinedN, joined) = markup_elem "joined";
+
val (failedN, failed) = markup_elem "failed";
val (finishedN, finished) = markup_elem "finished";
-val (disposedN, disposed) = markup_elem "disposed";
(* interactive documents *)
--- a/src/Pure/General/markup.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/General/markup.scala Mon Aug 16 12:33:52 2010 +0200
@@ -193,13 +193,10 @@
val TASK = "task"
- val UNPROCESSED = "unprocessed"
- val RUNNING = "running"
val FORKED = "forked"
val JOINED = "joined"
val FAILED = "failed"
val FINISHED = "finished"
- val DISPOSED = "disposed"
/* interactive documents */
--- a/src/Pure/Isar/outer_syntax.ML Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Mon Aug 16 12:33:52 2010 +0200
@@ -249,7 +249,7 @@
handle ERROR msg => (Toplevel.malformed range_pos msg, true)
end;
-fun prepare_unit commands init (cmd, proof, proper_proof) =
+fun prepare_atom commands init (cmd, proof, proper_proof) =
let
val (tr, proper_cmd) = prepare_span commands cmd |>> Toplevel.modify_init init;
val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
@@ -278,14 +278,14 @@
val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
val spans = Source.exhaust (Thy_Syntax.span_source toks);
val _ = List.app Thy_Syntax.report_span spans; (* FIXME ?? *)
- val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
- |> Par_List.map (prepare_unit commands init) |> flat;
+ val atoms = Source.exhaust (Thy_Syntax.atom_source (Source.of_list spans))
+ |> Par_List.map (prepare_atom commands init) |> flat;
val _ = Present.theory_source name
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
- val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion units);
+ val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion atoms);
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
fun after_load () =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/toplevel.scala Mon Aug 16 12:33:52 2010 +0200
@@ -0,0 +1,31 @@
+/* Title: Pure/Isar/toplevel.scala
+ Author: Makarius
+
+Isabelle/Isar toplevel transactions.
+*/
+
+package isabelle
+
+
+object Toplevel
+{
+ sealed abstract class Status
+ case class Forked(forks: Int) extends Status
+ case object Unprocessed extends Status
+ case object Finished extends Status
+ case object Failed extends Status
+
+ def command_status(markup: List[Markup]): Status =
+ {
+ val forks = (0 /: markup) {
+ case (i, Markup(Markup.FORKED, _)) => i + 1
+ case (i, Markup(Markup.JOINED, _)) => i - 1
+ case (i, _) => i
+ }
+ if (forks != 0) Forked(forks)
+ else if (markup.exists(_.name == Markup.FAILED)) Failed
+ else if (markup.exists(_.name == Markup.FINISHED)) Finished
+ else Unprocessed
+ }
+}
+
--- a/src/Pure/PIDE/command.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/PIDE/command.scala Mon Aug 16 12:33:52 2010 +0200
@@ -14,14 +14,6 @@
object Command
{
- object Status extends Enumeration
- {
- val UNPROCESSED = Value("UNPROCESSED")
- val FINISHED = Value("FINISHED")
- val FAILED = Value("FAILED")
- val UNDEFINED = Value("UNDEFINED")
- }
-
case class HighlightInfo(kind: String, sub_kind: Option[String]) {
override def toString = kind
}
@@ -35,8 +27,7 @@
case class State(
val command: Command,
- val status: Command.Status.Value,
- val forks: Int,
+ val status: List[Markup],
val reverse_results: List[XML.Tree],
val markup: Markup_Text)
{
@@ -64,12 +55,12 @@
case Command.TypeInfo(_) => true
case _ => false }).flatten
- def type_at(pos: Int): Option[String] =
+ def type_at(pos: Text.Offset): Option[String] =
{
- types.find(t => t.start <= pos && pos < t.stop) match {
+ types.find(_.range.contains(pos)) match {
case Some(t) =>
t.info match {
- case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
+ case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
case _ => None
}
case None => None
@@ -81,8 +72,8 @@
case Command.RefInfo(_, _, _, _) => true
case _ => false }).flatten
- def ref_at(pos: Int): Option[Markup_Node] =
- refs.find(t => t.start <= pos && pos < t.stop)
+ def ref_at(pos: Text.Offset): Option[Markup_Node] =
+ refs.find(_.range.contains(pos))
/* message dispatch */
@@ -90,15 +81,7 @@
def accumulate(message: XML.Tree): Command.State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), elems) =>
- (this /: elems)((state, elem) =>
- elem match {
- case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED)
- case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED)
- case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED)
- case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1)
- case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1)
- case _ => System.err.println("Ignored status message: " + elem); state
- })
+ copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status)
case XML.Elem(Markup(Markup.REPORT, _), elems) =>
(this /: elems)((state, elem) =>
@@ -166,7 +149,7 @@
/* source text */
val source: String = span.map(_.source).mkString
- def source(i: Int, j: Int): String = source.substring(i, j)
+ def source(range: Text.Range): String = source.substring(range.start, range.stop)
def length: Int = source.length
lazy val symbol_index = new Symbol.Index(source)
@@ -178,12 +161,11 @@
{
val start = symbol_index.decode(begin)
val stop = symbol_index.decode(end)
- new Markup_Tree(new Markup_Node(start, stop, info), Nil)
+ new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
}
/* accumulated results */
- val empty_state: Command.State =
- Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source))
+ val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source))
}
--- a/src/Pure/PIDE/document.ML Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/PIDE/document.ML Mon Aug 16 12:33:52 2010 +0200
@@ -2,7 +2,7 @@
Author: Makarius
Document as collection of named nodes, each consisting of an editable
-list of commands.
+list of commands, associated with asynchronous execution process.
*)
signature DOCUMENT =
@@ -12,9 +12,15 @@
type command_id = id
type exec_id = id
val no_id: id
+ 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 state
+ val init_state: state
+ val define_command: command_id -> string -> state -> state
+ val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
+ val execute: version_id -> state -> state
end;
structure Document: DOCUMENT =
@@ -29,15 +35,280 @@
val no_id = 0;
+local
+ val id_count = Synchronized.var "id" 0;
+in
+ fun new_id () =
+ Synchronized.change_result id_count
+ (fn i =>
+ let val i' = i + 1
+ in (i', i') end);
+end;
+
val parse_id = Markup.parse_int;
val print_id = Markup.print_int;
+fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id);
+fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
-(* edits *)
+
+
+(** 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*)
+ 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);
+
+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);
+
+
+(* 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 *)
type edit =
string * (*node name*)
((command_id * command_id option) list) option; (*NONE: remove, SOME: insert/remove commands*)
+val empty_node = Node (Inttab.make [(no_id, make_entry NONE (SOME no_id))]);
+
+fun edit_node (id, SOME id2) = insert_after id id2
+ | edit_node (id, NONE) = delete_after id;
+
+
+(* version operations *)
+
+fun nodes_of (Version nodes) = nodes;
+val node_names_of = Graph.keys o nodes_of;
+
+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;
+
+fun put_node name node (Version nodes) =
+ Version (Graph.map_node name (K node) nodes); (* FIXME Graph.UNDEF !? *)
+
end;
+
+
+(** global state -- document structure and execution process **)
+
+abstype state = State of
+ {versions: version Inttab.table, (*version_id -> document content*)
+ commands: Toplevel.transition future Inttab.table, (*command_id -> transition (future parsing)*)
+ execs: Toplevel.state option lazy Inttab.table, (*exec_id -> execution process*)
+ execution: unit future list} (*global execution process*)
+with
+
+fun make_state (versions, commands, execs, execution) =
+ State {versions = versions, commands = commands, execs = execs, execution = execution};
+
+fun map_state f (State {versions, commands, execs, execution}) =
+ make_state (f (versions, commands, execs, execution));
+
+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))],
+ []);
+
+
+(* document versions *)
+
+fun define_version (id: version_id) version =
+ map_state (fn (versions, commands, execs, execution) =>
+ let val versions' = Inttab.update_new (id, version) versions
+ handle Inttab.DUP dup => err_dup "document version" dup
+ in (versions', commands, execs, execution) end);
+
+fun the_version (State {versions, ...}) (id: version_id) =
+ (case Inttab.lookup versions id of
+ NONE => err_undef "document version" id
+ | SOME version => version);
+
+
+(* commands *)
+
+fun define_command (id: command_id) text =
+ map_state (fn (versions, commands, execs, execution) =>
+ let
+ val id_string = print_id id;
+ val tr = Future.fork_pri 2 (fn () =>
+ Position.setmp_thread_data (Position.id_only id_string)
+ (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
+ val commands' =
+ Inttab.update_new (id, tr) commands
+ handle Inttab.DUP dup => err_dup "command" dup;
+ in (versions, commands', execs, execution) end);
+
+fun the_command (State {commands, ...}) (id: command_id) =
+ (case Inttab.lookup commands id of
+ NONE => err_undef "command" id
+ | SOME tr => tr);
+
+fun join_commands (State {commands, ...}) =
+ Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands ();
+
+
+(* command executions *)
+
+fun define_exec (id: exec_id) exec =
+ map_state (fn (versions, commands, execs, execution) =>
+ let val execs' = Inttab.update_new (id, exec) execs
+ handle Inttab.DUP dup => err_dup "command execution" dup
+ in (versions, commands, execs', execution) end);
+
+fun the_exec (State {execs, ...}) (id: exec_id) =
+ (case Inttab.lookup execs id of
+ NONE => err_undef "command execution" id
+ | SOME exec => exec);
+
+end;
+
+
+
+(** editing **)
+
+(* edit *)
+
+local
+
+fun is_changed node' (id, {next = _, exec}) =
+ (case try (the_entry node') id of
+ NONE => true
+ | SOME {next = _, exec = exec'} => exec' <> exec);
+
+fun new_exec name (id: command_id) (exec_id, updates, state) =
+ let
+ val exec = the_exec state exec_id;
+ val exec_id' = new_id ();
+ val tr = the_command state id;
+ val exec' =
+ Lazy.lazy (fn () =>
+ (case Lazy.force exec of
+ NONE => NONE
+ | SOME st =>
+ let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join tr)
+ in Toplevel.run_command name exec_tr st end));
+ val state' = define_exec exec_id' exec' state;
+ in (exec_id', (id, exec_id') :: updates, state') end;
+
+in
+
+fun edit (old_id: version_id) (new_id: version_id) edits state =
+ let
+ val old_version = the_version state old_id;
+ 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
+ NONE => (rev_updates, version, st)
+ | SOME (prev, id, _) =>
+ let
+ val prev_exec = the (#exec (the_entry node (the prev)));
+ 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;
+ in (rev_upds @ rev_updates, put_node name node' version, st') end)
+ end;
+
+ (* FIXME proper node deps *)
+ val (rev_updates, new_version', state') =
+ fold update_node (node_names_of new_version) ([], new_version, state);
+ val state'' = define_version new_id new_version' state';
+
+ val _ = join_commands state''; (* FIXME async!? *)
+ in (rev rev_updates, state'') end;
+
+end;
+
+
+(* execute *)
+
+fun execute version_id state =
+ state |> map_state (fn (versions, commands, execs, execution) =>
+ let
+ val version = the_version state version_id;
+
+ fun force_exec NONE = ()
+ | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
+
+ val _ = List.app Future.cancel execution;
+ fun await_cancellation () = uninterruptible (fn _ => Future.join_results) execution;
+
+ val execution' = (* FIXME proper node deps *)
+ 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) ())));
+ in (versions, commands, execs, execution') end);
+
+end;
+
--- a/src/Pure/PIDE/document.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/PIDE/document.scala Mon Aug 16 12:33:52 2010 +0200
@@ -2,7 +2,7 @@
Author: Makarius
Document as collection of named nodes, each consisting of an editable
-list of commands.
+list of commands, associated with asynchronous execution process.
*/
package isabelle
@@ -30,13 +30,23 @@
- /** named document nodes **/
+ /** document structure **/
+
+ /* named nodes -- development graph */
+
+ type Node_Text_Edit = (String, List[Text.Edit]) // FIXME None: remove
+
+ type Edit[C] =
+ (String, // node name
+ Option[List[(Option[C], Option[C])]]) // None: remove, Some: insert/remove commands
object Node
{
val empty: Node = new Node(Linear_Set())
- def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
+ // FIXME not scalable
+ def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
+ : Iterator[(Command, Text.Offset)] =
{
var i = offset
for (command <- commands) yield {
@@ -49,27 +59,25 @@
class Node(val commands: Linear_Set[Command])
{
- /* command ranges */
-
- def command_starts: Iterator[(Command, Int)] =
+ def command_starts: Iterator[(Command, Text.Offset)] =
Node.command_starts(commands.iterator)
- def command_start(cmd: Command): Option[Int] =
+ def command_start(cmd: Command): Option[Text.Offset] =
command_starts.find(_._1 == cmd).map(_._2)
- def command_range(i: Int): Iterator[(Command, Int)] =
+ def command_range(i: Text.Offset): Iterator[(Command, Text.Offset)] =
command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
- def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
+ def command_range(i: Text.Offset, j: Text.Offset): Iterator[(Command, Text.Offset)] =
command_range(i) takeWhile { case (_, start) => start < j }
- def command_at(i: Int): Option[(Command, Int)] =
+ def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
{
val range = command_range(i)
if (range.hasNext) Some(range.next) else None
}
- def proper_command_at(i: Int): Option[Command] =
+ def proper_command_at(i: Text.Offset): Option[Command] =
command_at(i) match {
case Some((command, _)) =>
commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
@@ -78,54 +86,102 @@
}
- /* initial document */
+
+ /** versioning **/
+
+ /* particular document versions */
- val init: Document = new Document(NO_ID, Map().withDefaultValue(Node.empty))
+ object Version
+ {
+ val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty))
+ }
+ class Version(val id: Version_ID, val nodes: Map[String, Node])
- /** changes of plain text, eventually resulting in document edits **/
+ /* changes of plain text, eventually resulting in document edits */
- type Node_Text_Edit = (String, List[Text_Edit]) // FIXME None: remove
+ object Change
+ {
+ val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init))
+ }
- type Edit[C] =
- (String, // node name
- Option[List[(Option[C], Option[C])]]) // None: remove, Some: insert/remove commands
+ class Change(
+ val previous: Future[Version],
+ val edits: List[Node_Text_Edit],
+ val result: Future[(List[Edit[Command]], Version)])
+ {
+ val current: Future[Version] = result.map(_._2)
+ def is_finished: Boolean = previous.is_finished && current.is_finished
+ }
+
+
+ /* history navigation and persistent snapshots */
abstract class Snapshot
{
- val document: Document
- val node: Document.Node
+ val version: Version
+ val node: Node
val is_outdated: Boolean
- def convert(offset: Int): Int
- def revert(offset: Int): Int
def lookup_command(id: Command_ID): Option[Command]
def state(command: Command): Command.State
+ def convert(i: Text.Offset): Text.Offset
+ def convert(range: Text.Range): Text.Range = range.map(convert(_))
+ def revert(i: Text.Offset): Text.Offset
+ def revert(range: Text.Range): Text.Range = range.map(revert(_))
+ }
+
+ object History
+ {
+ val init = new History(List(Change.init))
}
- object Change
+ // FIXME pruning, purging of state
+ class History(undo_list: List[Change])
{
- val init = new Change(Future.value(Document.init), Nil, Future.value(Nil, Document.init))
- }
+ require(!undo_list.isEmpty)
+
+ def tip: Change = undo_list.head
+ def +(ch: Change): History = new History(ch :: undo_list)
+
+ def snapshot(name: String, pending_edits: List[Text.Edit], state_snapshot: State): Snapshot =
+ {
+ val found_stable = undo_list.find(change =>
+ change.is_finished && state_snapshot.is_assigned(change.current.join))
+ require(found_stable.isDefined)
+ val stable = found_stable.get
+ val latest = undo_list.head
- class Change(
- val prev: Future[Document],
- val edits: List[Node_Text_Edit],
- val result: Future[(List[Edit[Command]], Document)])
- {
- val document: Future[Document] = result.map(_._2)
- def is_finished: Boolean = prev.is_finished && document.is_finished
+ val edits =
+ (pending_edits /: undo_list.takeWhile(_ != stable))((edits, change) =>
+ (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+ lazy val reverse_edits = edits.reverse
+
+ new Snapshot
+ {
+ val version = stable.current.join
+ val node = version.nodes(name)
+ val is_outdated = !(pending_edits.isEmpty && latest == stable)
+ def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
+ def state(command: Command): Command.State =
+ try { state_snapshot.command_state(version, command) }
+ catch { case _: State.Fail => command.empty_state }
+
+ def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
+ def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+ }
+ }
}
- /** global state -- accumulated prover results **/
+ /** global state -- document structure and execution process **/
object State
{
class Fail(state: State) extends Exception
- val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil)
+ val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)
class Assignment(former_assignment: Map[Command, Exec_ID])
{
@@ -142,20 +198,20 @@
}
case class State(
- val documents: Map[Version_ID, Document] = Map(),
+ val versions: Map[Version_ID, Version] = Map(),
val commands: Map[Command_ID, Command.State] = Map(),
- val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(),
- val assignments: Map[Document, State.Assignment] = Map(),
+ val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
+ val assignments: Map[Version, State.Assignment] = Map(),
val disposed: Set[ID] = Set()) // FIXME unused!?
{
private def fail[A]: A = throw new State.Fail(this)
- def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State =
+ def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State =
{
- val id = document.id
- if (documents.isDefinedAt(id) || disposed(id)) fail
- copy(documents = documents + (id -> document),
- assignments = assignments + (document -> new State.Assignment(former_assignment)))
+ val id = version.id
+ if (versions.isDefinedAt(id) || disposed(id)) fail
+ copy(versions = versions + (id -> version),
+ assignments = assignments + (version -> new State.Assignment(former_assignment)))
}
def define_command(command: Command): State =
@@ -167,16 +223,16 @@
def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
- def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
+ def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
- def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail)
+ def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
execs.get(id) match {
- case Some((st, docs)) =>
+ case Some((st, occs)) =>
val new_st = st.accumulate(message)
- (new_st, copy(execs = execs + (id -> (new_st, docs))))
+ (new_st, copy(execs = execs + (id -> (new_st, occs))))
case None =>
commands.get(id) match {
case Some(st) =>
@@ -188,38 +244,33 @@
def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
{
- val doc = the_document(id)
- val docs = Set(doc) // FIXME unused (!?)
+ val version = the_version(id)
+ val occs = Set(version) // FIXME unused (!?)
var new_execs = execs
val assigned_execs =
for ((cmd_id, exec_id) <- edits) yield {
val st = the_command(cmd_id)
if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
- new_execs += (exec_id -> (st, docs))
+ new_execs += (exec_id -> (st, occs))
(st.command, exec_id)
}
- the_assignment(doc).assign(assigned_execs) // FIXME explicit value instead of promise (!?)
+ the_assignment(version).assign(assigned_execs) // FIXME explicit value instead of promise (!?)
copy(execs = new_execs)
}
- def is_assigned(document: Document): Boolean =
- assignments.get(document) match {
+ def is_assigned(version: Version): Boolean =
+ assignments.get(version) match {
case Some(assgn) => assgn.is_finished
case None => false
}
- def command_state(document: Document, command: Command): Command.State =
+ def command_state(version: Version, command: Command): Command.State =
{
- val assgn = the_assignment(document)
+ val assgn = the_assignment(version)
require(assgn.is_finished)
the_exec_state(assgn.join.getOrElse(command, fail))
}
}
}
-
-class Document(
- val id: Document.Version_ID,
- val nodes: Map[String, Document.Node])
-
--- a/src/Pure/PIDE/event_bus.scala Mon Aug 16 12:11:01 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-/* Title: Pure/PIDE/event_bus.scala
- Author: Makarius
-
-Generic event bus with multiple receiving actors.
-*/
-
-package isabelle
-
-import scala.actors.Actor, Actor._
-import scala.collection.mutable.ListBuffer
-
-
-class Event_Bus[Event]
-{
- /* receivers */
-
- private val receivers = new ListBuffer[Actor]
-
- def += (r: Actor) { synchronized { receivers += r } }
- def + (r: Actor): Event_Bus[Event] = { this += r; this }
-
- def += (f: Event => Unit) {
- this += actor { loop { react { case x: Event => f(x) } } }
- }
-
- def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
-
- def -= (r: Actor) { synchronized { receivers -= r } }
- def - (r: Actor) = { this -= r; this }
-
-
- /* event invocation */
-
- def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
-}
--- a/src/Pure/PIDE/markup_node.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/PIDE/markup_node.scala Mon Aug 16 12:33:52 2010 +0200
@@ -12,17 +12,17 @@
-case class Markup_Node(val start: Int, val stop: Int, val info: Any)
+case class Markup_Node(val range: Text.Range, val info: Any)
{
def fits_into(that: Markup_Node): Boolean =
- that.start <= this.start && this.stop <= that.stop
+ that.range.start <= this.range.start && this.range.stop <= that.range.stop
}
case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
{
private def add(branch: Markup_Tree) = // FIXME avoid sort
- copy(branches = (branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
+ copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start))
private def remove(bs: List[Markup_Tree]) =
copy(branches = branches.filterNot(bs.contains(_)))
@@ -55,21 +55,21 @@
def flatten: List[Markup_Node] =
{
- var next_x = node.start
+ var next_x = node.range.start
if (branches.isEmpty) List(this.node)
else {
val filled_gaps =
for {
child <- branches
markups =
- if (next_x < child.node.start)
- new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
+ if (next_x < child.node.range.start)
+ new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten
else child.flatten
- update = (next_x = child.node.stop)
+ update = (next_x = child.node.range.stop)
markup <- markups
} yield markup
- if (next_x < node.stop)
- filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
+ if (next_x < node.range.stop)
+ filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info))
else filled_gaps
}
}
@@ -78,7 +78,7 @@
case class Markup_Text(val markup: List[Markup_Tree], val content: String)
{
- private val root = new Markup_Tree(new Markup_Node(0, content.length, None), markup) // FIXME !?
+ private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup) // FIXME !?
def + (new_tree: Markup_Tree): Markup_Text =
new Markup_Text((root + new_tree).branches, content)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/text.scala Mon Aug 16 12:33:52 2010 +0200
@@ -0,0 +1,73 @@
+/* Title: Pure/PIDE/text.scala
+ Author: Fabian Immler, TU Munich
+ Author: Makarius
+
+Basic operations on plain text.
+*/
+
+package isabelle
+
+
+object Text
+{
+ /* offset and range */
+
+ type Offset = Int
+
+ sealed case class Range(val start: Offset, val stop: Offset)
+ {
+ def contains(i: Offset): Boolean = start <= i && i < stop
+ def map(f: Offset => Offset): Range = Range(f(start), f(stop))
+ def +(i: Offset): Range = map(_ + i)
+ }
+
+
+ /* editing */
+
+ object Edit
+ {
+ def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
+ def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
+ }
+
+ class Edit(val is_insert: Boolean, val start: Offset, val text: String)
+ {
+ override def toString =
+ (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
+
+
+ /* transform offsets */
+
+ private def transform(do_insert: Boolean, i: Offset): Offset =
+ if (i < start) i
+ else if (is_insert == do_insert) i + text.length
+ else (i - text.length) max start
+
+ def convert(i: Offset): Offset = transform(true, i)
+ def revert(i: Offset): Offset = transform(false, i)
+
+
+ /* edit strings */
+
+ private def insert(i: Offset, string: String): String =
+ string.substring(0, i) + text + string.substring(i)
+
+ private def remove(i: Offset, count: Int, string: String): String =
+ string.substring(0, i) + string.substring(i + count)
+
+ def can_edit(string: String, shift: Int): Boolean =
+ shift <= start && start < shift + string.length
+
+ def edit(string: String, shift: Int): (Option[Edit], String) =
+ if (!can_edit(string, shift)) (Some(this), string)
+ else if (is_insert) (None, insert(start - shift, string))
+ else {
+ val i = start - shift
+ val count = text.length min (string.length - i)
+ val rest =
+ if (count == text.length) None
+ else Some(Edit.remove(start, text.substring(count)))
+ (rest, remove(i, count, string))
+ }
+ }
+}
--- a/src/Pure/PIDE/text_edit.scala Mon Aug 16 12:11:01 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-/* Title: Pure/PIDE/text_edit.scala
- Author: Fabian Immler, TU Munich
- Author: Makarius
-
-Basic edits on plain text.
-*/
-
-package isabelle
-
-
-class Text_Edit(val is_insert: Boolean, val start: Int, val text: String)
-{
- override def toString =
- (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
-
-
- /* transform offsets */
-
- private def transform(do_insert: Boolean, offset: Int): Int =
- if (offset < start) offset
- else if (is_insert == do_insert) offset + text.length
- else (offset - text.length) max start
-
- def convert(offset: Int): Int = transform(true, offset)
- def revert(offset: Int): Int = transform(false, offset)
-
-
- /* edit strings */
-
- private def insert(index: Int, string: String): String =
- string.substring(0, index) + text + string.substring(index)
-
- private def remove(index: Int, count: Int, string: String): String =
- string.substring(0, index) + string.substring(index + count)
-
- def can_edit(string: String, shift: Int): Boolean =
- shift <= start && start < shift + string.length
-
- def edit(string: String, shift: Int): (Option[Text_Edit], String) =
- if (!can_edit(string, shift)) (Some(this), string)
- else if (is_insert) (None, insert(start - shift, string))
- else {
- val index = start - shift
- val count = text.length min (string.length - index)
- val rest =
- if (count == text.length) None
- else Some(new Text_Edit(false, start, text.substring(count)))
- (rest, remove(index, count, string))
- }
-}
-
--- a/src/Pure/ROOT.ML Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/ROOT.ML Mon Aug 16 12:33:52 2010 +0200
@@ -236,9 +236,9 @@
use "Thy/term_style.ML";
use "Thy/thy_output.ML";
use "Thy/thy_syntax.ML";
-use "PIDE/document.ML";
use "old_goals.ML";
use "Isar/outer_syntax.ML";
+use "PIDE/document.ML";
use "Thy/thy_info.ML";
(*theory and proof operations*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/event_bus.scala Mon Aug 16 12:33:52 2010 +0200
@@ -0,0 +1,35 @@
+/* Title: Pure/System/event_bus.scala
+ Author: Makarius
+
+Generic event bus with multiple receiving actors.
+*/
+
+package isabelle
+
+import scala.actors.Actor, Actor._
+import scala.collection.mutable.ListBuffer
+
+
+class Event_Bus[Event]
+{
+ /* receivers */
+
+ private val receivers = new ListBuffer[Actor]
+
+ def += (r: Actor) { synchronized { receivers += r } }
+ def + (r: Actor): Event_Bus[Event] = { this += r; this }
+
+ def += (f: Event => Unit) {
+ this += actor { loop { react { case x: Event => f(x) } } }
+ }
+
+ def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
+
+ def -= (r: Actor) { synchronized { receivers -= r } }
+ def - (r: Actor) = { this -= r; this }
+
+
+ /* event invocation */
+
+ def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
+}
--- a/src/Pure/System/isar_document.ML Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/System/isar_document.ML Mon Aug 16 12:33:52 2010 +0200
@@ -1,295 +1,38 @@
(* Title: Pure/System/isar_document.ML
Author: Makarius
-Interactive Isar documents, which are structured as follows:
-
- - history: tree of documents (i.e. changes without merge)
- - document: graph of nodes (cf. theory files)
- - node: linear set of commands, potentially with proof structure
+Protocol commands for interactive Isar documents.
*)
structure Isar_Document: sig end =
struct
-(* unique identifiers *)
-
-local
- val id_count = Synchronized.var "id" 0;
-in
- fun create_id () =
- Synchronized.change_result id_count
- (fn i =>
- let val i' = i + 1
- in (i', i') end);
-end;
-
-fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id);
-fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
-
-
-(** documents **)
-
-datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
-type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
-type document = node Graph.T; (*development graph via static imports*)
-
-
-(* command entries *)
-
-fun make_entry next exec = Entry {next = next, exec = exec};
+val global_state = Synchronized.var "Isar_Document" Document.init_state;
+val change_state = Synchronized.change global_state;
-fun the_entry (node: node) (id: Document.command_id) =
- (case Inttab.lookup node id of
- NONE => err_undef "command entry" id
- | SOME (Entry entry) => entry);
-
-fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
-
-fun put_entry_exec (id: Document.command_id) exec (node: 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);
-
-
-(* iterate entries *)
-
-fun fold_entries id0 f (node: node) =
- 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 node id0 then apply (SOME id0) else I end;
-
-fun first_entry P (node: 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 Document.no_id) end;
+val _ =
+ Isabelle_Process.add_command "Isar_Document.define_command"
+ (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
-
-(* modify entries *)
-
-fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: 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: Document.command_id) (node: node) =
- let val {next, exec} = the_entry node id in
- (case next of
- NONE => error ("No next entry to delete: " ^ Document.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 operations *)
-
-val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
-
-fun the_node (document: document) name =
- Graph.get_node document name handle Graph.UNDEF _ => empty_node;
+val _ =
+ Isabelle_Process.add_command "Isar_Document.edit_version"
+ (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
+ let
+ 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);
-fun edit_node (id, SOME id2) = insert_after id id2
- | edit_node (id, NONE) = delete_after id;
-
-fun edit_nodes (name, SOME edits) =
- Graph.default_node (name, empty_node) #>
- Graph.map_node name (fold edit_node edits)
- | edit_nodes (name, NONE) = Graph.del_node name;
-
-
-
-(** global configuration **)
-
-(* command executions *)
-
-local
-
-val global_execs =
- Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
-
-in
-
-fun define_exec (id: Document.exec_id) exec =
- NAMED_CRITICAL "Isar" (fn () =>
- Unsynchronized.change global_execs (Inttab.update_new (id, exec))
- handle Inttab.DUP dup => err_dup "exec" dup);
-
-fun the_exec (id: Document.exec_id) =
- (case Inttab.lookup (! global_execs) id of
- NONE => err_undef "exec" id
- | SOME exec => exec);
+ val (updates, state') = Document.edit old_id new_id edits state;
+ val _ =
+ implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
+ |> Markup.markup (Markup.assign new_id)
+ |> Output.status;
+ val state'' = Document.execute new_id state';
+ in state'' end));
end;
-
-(* commands *)
-
-local
-
-val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]);
-
-in
-
-fun define_command (id: Document.command_id) text =
- let
- val id_string = Document.print_id id;
- val tr =
- Position.setmp_thread_data (Position.id_only id_string) (fn () =>
- Outer_Syntax.prepare_command (Position.id id_string) text) ();
- in
- NAMED_CRITICAL "Isar" (fn () =>
- Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr))
- handle Inttab.DUP dup => err_dup "command" dup)
- end;
-
-fun the_command (id: Document.command_id) =
- (case Inttab.lookup (! global_commands) id of
- NONE => err_undef "command" id
- | SOME tr => tr);
-
-end;
-
-
-(* document versions *)
-
-local
-
-val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
-
-in
-
-fun define_document (id: Document.version_id) document =
- NAMED_CRITICAL "Isar" (fn () =>
- Unsynchronized.change global_documents (Inttab.update_new (id, document))
- handle Inttab.DUP dup => err_dup "document" dup);
-
-fun the_document (id: Document.version_id) =
- (case Inttab.lookup (! global_documents) id of
- NONE => err_undef "document" id
- | SOME document => document);
-
-end;
-
-
-
-(** document editing **)
-
-(* execution *)
-
-local
-
-val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
-
-fun force_exec NONE = ()
- | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id));
-
-in
-
-fun execute document =
- NAMED_CRITICAL "Isar" (fn () =>
- let
- val old_execution = ! execution;
- val _ = List.app Future.cancel old_execution;
- fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
- (* FIXME proper node deps *)
- val new_execution = Graph.keys document |> map (fn name =>
- Future.fork_pri 1 (fn () =>
- let
- val _ = await_cancellation ();
- val exec =
- fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
- (the_node document name);
- in exec () end));
- in execution := new_execution end);
-
-end;
-
-
-(* editing *)
-
-local
-
-fun is_changed node' (id, {next = _, exec}) =
- (case try (the_entry node') id of
- NONE => true
- | SOME {next = _, exec = exec'} => exec' <> exec);
-
-fun new_exec name (id: Document.command_id) (exec_id, updates) =
- let
- val exec = the_exec exec_id;
- val exec_id' = create_id ();
- val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id);
- val exec' =
- Lazy.lazy (fn () =>
- (case Lazy.force exec of
- NONE => NONE
- | SOME st => Toplevel.run_command name tr st));
- val _ = define_exec exec_id' exec';
- in (exec_id', (id, exec_id') :: updates) end;
-
-fun updates_status new_id updates =
- implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
- |> Markup.markup (Markup.assign new_id)
- |> Output.status;
-
-in
-
-fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
- NAMED_CRITICAL "Isar" (fn () =>
- let
- val old_document = the_document old_id;
- val new_document = fold edit_nodes edits old_document;
-
- fun update_node name node =
- (case first_entry (is_changed (the_node old_document name)) node of
- NONE => ([], node)
- | SOME (prev, id, _) =>
- let
- val prev_exec_id = the (#exec (the_entry node (the prev)));
- val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []);
- val node' = fold set_entry_exec updates node;
- in (rev updates, node') end);
-
- (* FIXME proper node deps *)
- val (updatess, new_document') =
- (Graph.keys new_document, new_document)
- |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
-
- val _ = define_document new_id new_document';
- val _ = updates_status new_id (flat updatess);
- val _ = execute new_document';
- in () end);
-
-end;
-
-
-
-(** Isabelle process commands **)
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.define_command"
- (fn [id, text] => define_command (Document.parse_id id) text);
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.edit_document"
- (fn [old_id, new_id, edits] =>
- edit_document (Document.parse_id old_id) (Document.parse_id new_id)
- (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)));
-
-end;
-
--- a/src/Pure/System/isar_document.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/System/isar_document.scala Mon Aug 16 12:33:52 2010 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/System/isar_document.scala
Author: Makarius
-Interactive Isar documents.
+Protocol commands for interactive Isar documents.
*/
package isabelle
@@ -46,9 +46,9 @@
input("Isar_Document.define_command", Document.ID(id), text)
- /* documents */
+ /* document versions */
- def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ 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 =
@@ -60,7 +60,7 @@
XML_Data.make_option(XML_Data.make_list(
XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
- input("Isar_Document.edit_document",
+ input("Isar_Document.edit_version",
Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
}
}
--- a/src/Pure/System/session.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/System/session.scala Mon Aug 16 12:33:52 2010 +0200
@@ -40,7 +40,7 @@
/* pervasive event buses */
val global_settings = new Event_Bus[Session.Global_Settings.type]
- val raw_results = new Event_Bus[Isabelle_Process.Result]
+ val raw_protocol = new Event_Bus[Isabelle_Process.Result]
val raw_output = new Event_Bus[Isabelle_Process.Result]
val commands_changed = new Event_Bus[Session.Commands_Changed]
val perspective = new Event_Bus[Session.Perspective.type]
@@ -49,7 +49,7 @@
/* unique ids */
private var id_count: Document.ID = 0
- def create_id(): Document.ID = synchronized {
+ def new_id(): Document.ID = synchronized {
require(id_count > java.lang.Long.MIN_VALUE)
id_count -= 1
id_count
@@ -81,14 +81,14 @@
{
require(change.is_finished)
- val old_doc = change.prev.join
- val (node_edits, doc) = change.result.join
+ val previous = change.previous.join
+ val (node_edits, current) = change.result.join
- var former_assignment = current_state().the_assignment(old_doc).join
+ var former_assignment = current_state().the_assignment(previous).join
for {
(name, Some(cmd_edits)) <- node_edits
(prev, None) <- cmd_edits
- removed <- old_doc.nodes(name).commands.get_after(prev)
+ removed <- previous.nodes(name).commands.get_after(prev)
} former_assignment -= removed
val id_edits =
@@ -113,8 +113,8 @@
}
(name -> Some(ids))
}
- change_state(_.define_document(doc, former_assignment))
- prover.edit_document(old_doc.id, doc.id, id_edits)
+ change_state(_.define_version(current, former_assignment))
+ prover.edit_version(previous.id, current.id, id_edits)
}
//}}}
@@ -129,7 +129,7 @@
def handle_result(result: Isabelle_Process.Result)
//{{{
{
- raw_results.event(result)
+ raw_protocol.event(result)
Position.get_id(result.properties) match {
case Some(state_id) =>
@@ -142,8 +142,8 @@
case None =>
if (result.is_status) {
result.body match {
- case List(Isar_Document.Assign(doc_id, edits)) =>
- try { change_state(_.assign(doc_id, edits)) }
+ case List(Isar_Document.Assign(id, edits)) =>
+ try { change_state(_.assign(id, edits)) }
catch { case _: Document.State.Fail => bad_result(result) }
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
case List(Keyword.Keyword_Decl(name)) => syntax += name
@@ -286,60 +286,30 @@
/** editor history **/
- private case class Edit_Document(edits: List[Document.Node_Text_Edit])
+ private case class Edit_Version(edits: List[Document.Node_Text_Edit])
private val editor_history = new Actor
{
- @volatile private var history = List(Document.Change.init)
-
- def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
- {
- val state_snapshot = current_state()
- val history_snapshot = history
-
- val found_stable = history_snapshot.find(change =>
- change.is_finished && state_snapshot.is_assigned(change.document.join))
- require(found_stable.isDefined)
- val stable = found_stable.get
- val latest = history_snapshot.head
+ @volatile private var history = Document.History.init
- val edits =
- (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
- (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
- lazy val reverse_edits = edits.reverse
-
- new Document.Snapshot {
- val document = stable.document.join
- val node = document.nodes(name)
- val is_outdated = !(pending_edits.isEmpty && latest == stable)
- def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
- def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
- def lookup_command(id: Document.Command_ID): Option[Command] =
- state_snapshot.lookup_command(id)
- def state(command: Command): Command.State =
- try { state_snapshot.command_state(document, command) }
- catch { case _: Document.State.Fail => command.empty_state }
- }
- }
+ def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
+ history.snapshot(name, pending_edits, current_state())
def act
{
loop {
react {
- case Edit_Document(edits) =>
- val history_snapshot = history
- require(!history_snapshot.isEmpty)
-
- val prev = history_snapshot.head.document
- val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
+ case Edit_Version(edits) =>
+ val prev = history.tip.current
+ val result =
isabelle.Future.fork {
- val old_doc = prev.join
- val former_assignment = current_state().the_assignment(old_doc).join // FIXME async!?
- Thy_Syntax.text_edits(Session.this, old_doc, edits)
+ val previous = prev.join
+ val former_assignment = current_state().the_assignment(previous).join // FIXME async!?
+ Thy_Syntax.text_edits(Session.this, previous, edits)
}
- val new_change = new Document.Change(prev, edits, result)
- history ::= new_change
- new_change.document.map(_ => session_actor ! new_change)
+ val change = new Document.Change(prev, edits, result)
+ history += change
+ change.current.map(_ => session_actor ! change)
reply(())
case bad => System.err.println("editor_model: ignoring bad message " + bad)
@@ -358,8 +328,8 @@
def stop() { session_actor ! Stop }
- def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
+ def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
editor_history.snapshot(name, pending_edits)
- def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
+ def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
}
--- a/src/Pure/Thy/thy_syntax.ML Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Mon Aug 16 12:33:52 2010 +0200
@@ -21,7 +21,7 @@
val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
val present_span: span -> output
val report_span: span -> unit
- val unit_source: (span, 'a) Source.source ->
+ val atom_source: (span, 'a) Source.source ->
(span * span list * bool, (span, 'a) Source.source) Source.source
end;
@@ -160,7 +160,7 @@
-(** units: commands with proof **)
+(** specification atoms: commands with optional proof **)
(* scanning spans *)
@@ -174,7 +174,7 @@
val stopper = Scan.stopper (K eof) is_eof;
-(* unit_source *)
+(* atom_source *)
local
@@ -188,13 +188,13 @@
(if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
-val unit =
+val atom =
command_with Keyword.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
Scan.one not_eof >> (fn a => (a, [], true));
in
-fun unit_source src = Source.source stopper (Scan.bulk unit) NONE src;
+fun atom_source src = Source.source stopper (Scan.bulk atom) NONE src;
end;
--- a/src/Pure/Thy/thy_syntax.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Aug 16 12:33:52 2010 +0200
@@ -38,12 +38,12 @@
/** text edits **/
- def text_edits(session: Session, old_doc: Document, edits: List[Document.Node_Text_Edit])
- : (List[Document.Edit[Command]], Document) =
+ def text_edits(session: Session, previous: Document.Version,
+ edits: List[Document.Node_Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
{
/* phase 1: edit individual command source */
- @tailrec def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command])
+ @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
: Linear_Set[Command] =
{
eds match {
@@ -96,7 +96,7 @@
(Some(last), spans1.take(spans1.length - 1))
else (commands.next(last), spans1)
- val inserted = spans2.map(span => new Command(session.create_id(), span))
+ val inserted = spans2.map(span => new Command(session.new_id(), span))
val new_commands =
commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
recover_spans(new_commands)
@@ -110,7 +110,7 @@
{
val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
- var nodes = old_doc.nodes
+ var nodes = previous.nodes
for ((name, text_edits) <- edits) {
val commands0 = nodes(name).commands
@@ -127,7 +127,7 @@
doc_edits += (name -> Some(cmd_edits))
nodes += (name -> new Document.Node(commands2))
}
- (doc_edits.toList, new Document(session.create_id(), nodes))
+ (doc_edits.toList, new Document.Version(session.new_id(), nodes))
}
}
}
--- a/src/Pure/build-jars Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Pure/build-jars Mon Aug 16 12:33:52 2010 +0200
@@ -36,14 +36,15 @@
Isar/keyword.scala
Isar/outer_syntax.scala
Isar/parse.scala
+ Isar/toplevel.scala
Isar/token.scala
PIDE/command.scala
PIDE/document.scala
- PIDE/event_bus.scala
PIDE/markup_node.scala
- PIDE/text_edit.scala
+ PIDE/text.scala
System/cygwin.scala
System/download.scala
+ System/event_bus.scala
System/gui_setup.scala
System/isabelle_process.scala
System/isabelle_syntax.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 16 12:33:52 2010 +0200
@@ -186,7 +186,7 @@
// simplify slightly odd result of TextArea.getLineEndOffset
// NB: jEdit already normalizes \r\n and \r to \n
- def visible_line_end(start: Int, end: Int): Int =
+ def visible_line_end(start: Text.Offset, end: Text.Offset): Text.Offset =
{
val end1 = end - 1
if (start <= end1 && end1 < buffer.getLength &&
@@ -199,14 +199,14 @@
object pending_edits // owned by Swing thread
{
- private val pending = new mutable.ListBuffer[Text_Edit]
- def snapshot(): List[Text_Edit] = pending.toList
+ private val pending = new mutable.ListBuffer[Text.Edit]
+ def snapshot(): List[Text.Edit] = pending.toList
private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
- if (!pending.isEmpty) session.edit_document(List((thy_name, flush())))
+ if (!pending.isEmpty) session.edit_version(List((thy_name, flush())))
}
- def flush(): List[Text_Edit] =
+ def flush(): List[Text.Edit] =
{
Swing_Thread.require()
val edits = snapshot()
@@ -214,7 +214,7 @@
edits
}
- def +=(edit: Text_Edit)
+ def +=(edit: Text.Edit)
{
Swing_Thread.require()
pending += edit
@@ -225,7 +225,8 @@
/* snapshot */
- def snapshot(): Document.Snapshot = {
+ def snapshot(): Document.Snapshot =
+ {
Swing_Thread.require()
session.snapshot(thy_name, pending_edits.snapshot())
}
@@ -238,13 +239,13 @@
override def contentInserted(buffer: JEditBuffer,
start_line: Int, offset: Int, num_lines: Int, length: Int)
{
- pending_edits += new Text_Edit(true, offset, buffer.getText(offset, length))
+ pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
}
override def preContentRemoved(buffer: JEditBuffer,
- start_line: Int, start: Int, num_lines: Int, removed_length: Int)
+ start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
{
- pending_edits += new Text_Edit(false, start, buffer.getText(start, removed_length))
+ pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
}
}
@@ -271,7 +272,7 @@
Document_View(text_area).get.set_styles()
*/
- def handle_token(style: Byte, offset: Int, length: Int) =
+ def handle_token(style: Byte, offset: Text.Offset, length: Int) =
handler.handleToken(line_segment, style, offset, length, context)
var next_x = start
@@ -279,8 +280,7 @@
(command, command_start) <-
snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
markup <- snapshot.state(command).highlight.flatten
- val abs_start = snapshot.convert(command_start + markup.start)
- val abs_stop = snapshot.convert(command_start + markup.stop)
+ val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
if (abs_stop > start)
if (abs_start < stop)
val token_start = (abs_start - start) max 0
@@ -320,7 +320,7 @@
buffer.setTokenMarker(token_marker)
buffer.addBufferListener(buffer_listener)
buffer.propertiesChanged()
- pending_edits += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
+ pending_edits += Text.Edit.insert(0, buffer.getText(0, buffer.getLength))
}
def refresh()
--- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 16 12:33:52 2010 +0200
@@ -28,14 +28,13 @@
{
val state = snapshot.state(command)
if (snapshot.is_outdated) new Color(240, 240, 240)
- else if (state.forks > 0) new Color(255, 228, 225)
- else if (state.forks < 0) Color.red
else
- state.status match {
- case Command.Status.UNPROCESSED => new Color(255, 228, 225)
- case Command.Status.FINISHED => new Color(234, 248, 255)
- case Command.Status.FAILED => new Color(255, 193, 193)
- case Command.Status.UNDEFINED => Color.red
+ Toplevel.command_status(state.status) match {
+ case Toplevel.Forked(i) if i > 0 => new Color(255, 228, 225)
+ case Toplevel.Finished => new Color(234, 248, 255)
+ case Toplevel.Failed => new Color(255, 193, 193)
+ case Toplevel.Unprocessed => new Color(255, 228, 225)
+ case _ => Color.red
}
}
@@ -152,12 +151,12 @@
val snapshot = model.snapshot()
- val command_range: Iterable[(Command, Int)] =
+ val command_range: Iterable[(Command, Text.Offset)] =
{
val range = snapshot.node.command_range(snapshot.revert(start(0)))
if (range.hasNext) {
val (cmd0, start0) = range.next
- new Iterable[(Command, Int)] {
+ new Iterable[(Command, Text.Offset)] {
def iterator =
Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
}
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 16 12:33:52 2010 +0200
@@ -49,9 +49,8 @@
case Some((command, command_start)) =>
snapshot.state(command).ref_at(offset - command_start) match {
case Some(ref) =>
- val begin = snapshot.convert(command_start + ref.start)
+ val Text.Range(begin, end) = snapshot.convert(ref.range + command_start)
val line = buffer.getLineOfOffset(begin)
- val end = snapshot.convert(command_start + ref.stop)
ref.info match {
case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
new External_Hyperlink(begin, end, line, ref_file, ref_line)
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 16 12:33:52 2010 +0200
@@ -95,9 +95,9 @@
import Isabelle_Sidekick.int_to_pos
val root = data.root
- val doc = Swing_Thread.now { model.snapshot().node } // FIXME cover all nodes (!??)
+ val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
for {
- (command, command_start) <- doc.command_range(0)
+ (command, command_start) <- snapshot.node.command_range(0)
if command.is_command && !stopped
}
{
@@ -113,8 +113,7 @@
override def getStart: Position = command_start
override def setEnd(end: Position) = ()
override def getEnd: Position = command_start + command.length
- override def toString = name
- })
+ override def toString = name})
root.add(node)
}
}
@@ -132,7 +131,7 @@
for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
{
- val content = command.source(node.start, node.stop).replace('\n', ' ')
+ val content = command.source(node.range).replace('\n', ' ')
val id = command.id
new DefaultMutableTreeNode(new IAsset {
@@ -142,9 +141,9 @@
override def getName: String = Markup.Long(id)
override def setName(name: String) = ()
override def setStart(start: Position) = ()
- override def getStart: Position = command_start + node.start
+ override def getStart: Position = command_start + node.range.start
override def setEnd(end: Position) = ()
- override def getEnd: Position = command_start + node.stop
+ override def getEnd: Position = command_start + node.range.stop
override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
})
}))
--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Mon Aug 16 12:11:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Mon Aug 16 12:33:52 2010 +0200
@@ -34,6 +34,6 @@
}
}
- override def init() { Isabelle.session.raw_results += main_actor }
- override def exit() { Isabelle.session.raw_results -= main_actor }
+ override def init() { Isabelle.session.raw_protocol += main_actor }
+ override def exit() { Isabelle.session.raw_protocol -= main_actor }
}