# HG changeset patch # User wenzelm # Date 1281954832 -7200 # Node ID be39c9e5ac39ef1a2def9529b121720e32881b64 # Parent 644b346027126b443410ae8a8f1bdb168c099c74# Parent 9951852fae91dc6487360c133d769fb1226b0611 merged diff -r 644b34602712 -r be39c9e5ac39 src/Pure/General/markup.ML --- 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 *) diff -r 644b34602712 -r be39c9e5ac39 src/Pure/General/markup.scala --- 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 */ diff -r 644b34602712 -r be39c9e5ac39 src/Pure/Isar/outer_syntax.ML --- 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 () = diff -r 644b34602712 -r be39c9e5ac39 src/Pure/Isar/toplevel.scala --- /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 + } +} + diff -r 644b34602712 -r be39c9e5ac39 src/Pure/PIDE/command.scala --- 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)) } diff -r 644b34602712 -r be39c9e5ac39 src/Pure/PIDE/document.ML --- 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; + diff -r 644b34602712 -r be39c9e5ac39 src/Pure/PIDE/document.scala --- 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]) - diff -r 644b34602712 -r be39c9e5ac39 src/Pure/PIDE/event_bus.scala --- 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) } } -} diff -r 644b34602712 -r be39c9e5ac39 src/Pure/PIDE/markup_node.scala --- 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) diff -r 644b34602712 -r be39c9e5ac39 src/Pure/PIDE/text.scala --- /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)) + } + } +} diff -r 644b34602712 -r be39c9e5ac39 src/Pure/PIDE/text_edit.scala --- 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)) - } -} - diff -r 644b34602712 -r be39c9e5ac39 src/Pure/ROOT.ML --- 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*) diff -r 644b34602712 -r be39c9e5ac39 src/Pure/System/event_bus.scala --- /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) } } +} diff -r 644b34602712 -r be39c9e5ac39 src/Pure/System/isar_document.ML --- 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; - diff -r 644b34602712 -r be39c9e5ac39 src/Pure/System/isar_document.scala --- 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)) } } diff -r 644b34602712 -r be39c9e5ac39 src/Pure/System/session.scala --- 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) } } diff -r 644b34602712 -r be39c9e5ac39 src/Pure/Thy/thy_syntax.ML --- 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; diff -r 644b34602712 -r be39c9e5ac39 src/Pure/Thy/thy_syntax.scala --- 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)) } } } diff -r 644b34602712 -r be39c9e5ac39 src/Pure/build-jars --- 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 diff -r 644b34602712 -r be39c9e5ac39 src/Tools/jEdit/src/jedit/document_model.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() diff -r 644b34602712 -r be39c9e5ac39 src/Tools/jEdit/src/jedit/document_view.scala --- 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) } diff -r 644b34602712 -r be39c9e5ac39 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- 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) diff -r 644b34602712 -r be39c9e5ac39 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- 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 + "]" }) })) diff -r 644b34602712 -r be39c9e5ac39 src/Tools/jEdit/src/jedit/protocol_dockable.scala --- 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 } }