--- a/src/Tools/jEdit/src/jedit/document_model.scala Thu Dec 31 23:48:18 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Fri Jan 01 14:41:25 2010 +0100
@@ -8,7 +8,7 @@
package isabelle.jedit
-import isabelle.proofdocument.{Change, Command, Edit, Insert, Remove, Proof_Document, Session}
+import isabelle.proofdocument.{Change, Command, Edit, Insert, Remove, Document, Session}
import scala.actors.Actor, Actor._
import scala.collection.mutable
@@ -100,7 +100,7 @@
/* history of changes */
- private def doc_or_pred(c: Change): Proof_Document =
+ private def doc_or_pred(c: Change): Document =
session.document(c.id).getOrElse(doc_or_pred(c.parent.get))
def current_document() = doc_or_pred(current_change)
@@ -108,14 +108,14 @@
/* transforming offsets */
- private def changes_from(doc: Proof_Document): List[Edit] =
+ private def changes_from(doc: Document): List[Edit] =
List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
edits.toList
- def from_current(doc: Proof_Document, offset: Int): Int =
+ def from_current(doc: Document, offset: Int): Int =
(offset /: changes_from(doc).reverse) ((i, change) => change before i)
- def to_current(doc: Proof_Document, offset: Int): Int =
+ def to_current(doc: Document, offset: Int): Int =
(offset /: changes_from(doc)) ((i, change) => change after i)
def lines_of_command(cmd: Command): (Int, Int) =
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Dec 31 23:48:18 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Fri Jan 01 14:41:25 2010 +0100
@@ -8,7 +8,7 @@
package isabelle.jedit
-import isabelle.proofdocument.{Command, Proof_Document, Session}
+import isabelle.proofdocument.{Command, Document, Session}
import scala.actors.Actor._
@@ -23,7 +23,7 @@
object Document_View
{
- def choose_color(command: Command, doc: Proof_Document): Color =
+ def choose_color(command: Command, doc: Document): Color =
{
command.status(doc) match {
case Command.Status.UNPROCESSED => new Color(255, 228, 225)
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Dec 31 23:48:18 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Fri Jan 01 14:41:25 2010 +0100
@@ -19,7 +19,7 @@
import errorlist.DefaultErrorSource
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
-import isabelle.proofdocument.{Command, Markup_Node, Proof_Document}
+import isabelle.proofdocument.{Command, Markup_Node, Document}
class Isabelle_Sidekick extends SideKickParser("isabelle")
--- a/src/Tools/jEdit/src/proofdocument/command.scala Thu Dec 31 23:48:18 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala Fri Jan 01 14:41:25 2010 +0100
@@ -51,8 +51,8 @@
def content(i: Int, j: Int): String = content.substring(i, j)
val symbol_index = new Symbol.Index(content)
- def start(doc: Proof_Document) = doc.token_start(tokens.first)
- def stop(doc: Proof_Document) = doc.token_start(tokens.last) + tokens.last.length
+ def start(doc: Document) = doc.token_start(tokens.first)
+ def stop(doc: Document) = doc.token_start(tokens.last) + tokens.last.length
def contains(p: Token) = tokens.contains(p)
@@ -111,13 +111,13 @@
def highlight: Markup_Text = current_state.highlight
- private def cmd_state(doc: Proof_Document): State = // FIXME clarify
+ private def cmd_state(doc: Document): State = // FIXME clarify
doc.states.getOrElse(this, this).current_state
- def status(doc: Proof_Document) = cmd_state(doc).status
- def results(doc: Proof_Document) = cmd_state(doc).results
- def markup_root(doc: Proof_Document) = cmd_state(doc).markup_root
- def highlight(doc: Proof_Document) = cmd_state(doc).highlight
- def type_at(doc: Proof_Document, offset: Int) = cmd_state(doc).type_at(offset)
- def ref_at(doc: Proof_Document, offset: Int) = cmd_state(doc).ref_at(offset)
+ def status(doc: Document) = cmd_state(doc).status
+ def results(doc: Document) = cmd_state(doc).results
+ def markup_root(doc: Document) = cmd_state(doc).markup_root
+ def highlight(doc: Document) = cmd_state(doc).highlight
+ def type_at(doc: Document, offset: Int) = cmd_state(doc).type_at(offset)
+ def ref_at(doc: Document, offset: Int) = cmd_state(doc).ref_at(offset)
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/document.scala Fri Jan 01 14:41:25 2010 +0100
@@ -0,0 +1,305 @@
+/*
+ * Document as list of commands, consisting of lists of tokens
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.proofdocument
+
+
+import scala.actors.Actor._
+
+import java.util.regex.Pattern
+
+
+object Document
+{
+ // Be careful when changing this regex. Not only must it handle the
+ // spurious end of a token but also:
+ // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
+ // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
+
+ val token_pattern =
+ Pattern.compile(
+ "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
+ "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
+ "(\\?'?|')[A-Za-z_0-9.]*|" +
+ "[A-Za-z_0-9.]+|" +
+ "[!#$%&*+-/<=>?@^_|~]+|" +
+ "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
+ "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
+ "[()\\[\\]{}:;]", Pattern.MULTILINE)
+
+ def empty(id: Isar_Document.Document_ID): Document =
+ new Document(id, Linear_Set(), Map(), Linear_Set(), Map())
+
+ type StructureChange = List[(Option[Command], Option[Command])]
+}
+
+
+class Document(
+ val id: Isar_Document.Document_ID,
+ val tokens: Linear_Set[Token], // FIXME plain List, inside Command
+ val token_start: Map[Token, Int], // FIXME eliminate
+ val commands: Linear_Set[Command],
+ var states: Map[Command, Command]) // FIXME immutable, eliminate!?
+ extends Session.Entity
+{
+ import Document.StructureChange
+
+ def content = Token.string_from_tokens(Nil ++ tokens, token_start)
+
+
+ /* accumulated messages */
+
+ private val accumulator = actor {
+ loop {
+ react {
+ case (session: Session, message: XML.Tree) =>
+ message match {
+ case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
+ for {
+ XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
+ <- elems
+ } {
+ session.lookup_entity(cmd_id) match {
+ case Some(cmd: Command) =>
+ val state = cmd.finish_static(state_id)
+ session.register_entity(state)
+ states += (cmd -> state) // FIXME !?
+ session.command_change.event(cmd) // FIXME really!?
+ case _ =>
+ }
+ }
+ case _ =>
+ }
+
+ case bad => System.err.println("document accumulator: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ def consume(session: Session, message: XML.Tree) { accumulator ! (session, message) }
+
+
+
+ /** token view **/
+
+ def text_changed(session: Session, change: Change): (Document, StructureChange) =
+ {
+ def edit_doc(doc_chgs: (Document, StructureChange), edit: Edit) = {
+ val (doc, chgs) = doc_chgs
+ val (new_doc, chg) = doc.text_edit(session, edit, change.id)
+ (new_doc, chgs ++ chg)
+ }
+ ((this, Nil: StructureChange) /: change.edits)(edit_doc)
+ }
+
+ def text_edit(session: Session, e: Edit, id: String): (Document, StructureChange) =
+ {
+ case class TextChange(start: Int, added: String, removed: String)
+ val change = e match {
+ case Insert(s, a) => TextChange(s, a, "")
+ case Remove(s, r) => TextChange(s, "", r)
+ }
+ //indices of tokens
+ var start: Map[Token, Int] = token_start
+ def stop(t: Token) = start(t) + t.length
+ // split old token lists
+ val tokens = Nil ++ this.tokens
+ val (begin, remaining) = tokens.span(stop(_) < change.start)
+ val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length)
+ // update indices
+ start = end.foldLeft(start)((s, t) =>
+ s + (t -> (s(t) + change.added.length - change.removed.length)))
+
+ val split_begin = removed.takeWhile(start(_) < change.start).
+ map (t => {
+ val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
+ start += (split_tok -> start(t))
+ split_tok
+ })
+
+ val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length).
+ map (t => {
+ val split_tok =
+ new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind)
+ start += (split_tok -> start(t))
+ split_tok
+ })
+ // update indices
+ start = removed.foldLeft (start) ((s, t) => s - t)
+ start = split_end.foldLeft (start) ((s, t) =>
+ s + (t -> (change.start + change.added.length)))
+
+ val ins = new Token(change.added, Token.Kind.OTHER)
+ start += (ins -> change.start)
+
+ var invalid_tokens = split_begin ::: ins :: split_end ::: end
+ var new_tokens: List[Token] = Nil
+ var old_suffix: List[Token] = Nil
+
+ val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
+ val matcher =
+ Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
+
+ while (matcher.find() && invalid_tokens != Nil) {
+ val kind =
+ if (session.current_syntax.is_command(matcher.group))
+ Token.Kind.COMMAND_START
+ else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
+ Token.Kind.COMMENT
+ else
+ Token.Kind.OTHER
+ val new_token = new Token(matcher.group, kind)
+ start += (new_token -> (match_start + matcher.start))
+ new_tokens ::= new_token
+
+ invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
+ invalid_tokens match {
+ case t :: ts =>
+ if (start(t) == start(new_token) &&
+ start(t) > change.start + change.added.length) {
+ old_suffix = t :: ts
+ new_tokens = new_tokens.tail
+ invalid_tokens = Nil
+ }
+ case _ =>
+ }
+ }
+ val insert = new_tokens.reverse
+ val new_token_list = begin ::: insert ::: old_suffix
+ token_changed(session, id, begin.lastOption, insert,
+ old_suffix.firstOption, new_token_list, start)
+ }
+
+
+ /** command view **/
+
+ private def token_changed(
+ session: Session,
+ new_id: String,
+ before_change: Option[Token],
+ inserted_tokens: List[Token],
+ after_change: Option[Token],
+ new_tokens: List[Token],
+ new_token_start: Map[Token, Int]):
+ (Document, StructureChange) =
+ {
+ val new_tokenset = Linear_Set[Token]() ++ new_tokens
+ val cmd_before_change = before_change match {
+ case None => None
+ case Some(bc) =>
+ val cmd_with_bc = commands.find(_.contains(bc)).get
+ if (cmd_with_bc.tokens.last == bc) {
+ if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
+ Some(cmd_with_bc)
+ else commands.prev(cmd_with_bc)
+ }
+ else commands.prev(cmd_with_bc)
+ }
+
+ val cmd_after_change = after_change match {
+ case None => None
+ case Some(ac) =>
+ val cmd_with_ac = commands.find(_.contains(ac)).get
+ if (ac.is_start)
+ Some(cmd_with_ac)
+ else
+ commands.next(cmd_with_ac)
+ }
+
+ val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
+ takeWhile(Some(_) != cmd_after_change)
+
+ // calculate inserted commands
+ def tokens_to_commands(tokens: List[Token]): List[Command]= {
+ tokens match {
+ case Nil => Nil
+ case t :: ts =>
+ val (cmd, rest) =
+ ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
+ new Command(session.create_id(), t :: cmd, new_token_start) :: tokens_to_commands(rest)
+ }
+ }
+
+ val split_begin =
+ if (before_change.isDefined) {
+ val changed =
+ if (cmd_before_change.isDefined)
+ new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
+ else new_tokenset
+ if (changed.exists(_ == before_change.get))
+ changed.takeWhile(_ != before_change.get).toList :::
+ List(before_change.get)
+ else Nil
+ } else Nil
+
+ val split_end =
+ if (after_change.isDefined) {
+ val unchanged = new_tokens.dropWhile(_ != after_change.get)
+ if(cmd_after_change.isDefined) {
+ if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
+ unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
+ else Nil
+ } else {
+ unchanged
+ }
+ } else Nil
+
+ val rescan_begin =
+ split_begin :::
+ before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
+ val rescanning_tokens =
+ after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
+ split_end
+ val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
+
+ // build new document
+ val new_commandset = commands.
+ delete_between(cmd_before_change, cmd_after_change).
+ append_after(cmd_before_change, inserted_commands)
+
+
+ val doc =
+ new Document(new_id, new_tokenset, new_token_start, new_commandset,
+ states -- removed_commands)
+
+ val removes =
+ for (cmd <- removed_commands) yield (cmd_before_change -> None)
+ val inserts =
+ for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
+
+ return (doc, removes.toList ++ inserts)
+ }
+
+ val commands_offsets = {
+ var last_stop = 0
+ (for (c <- commands) yield {
+ val r = c -> (last_stop,c.stop(this))
+ last_stop = c.stop(this)
+ r
+ }).toArray
+ }
+
+ def command_at(pos: Int): Option[Command] =
+ find_command(pos, 0, commands_offsets.length)
+
+ // use a binary search to find commands for a given offset
+ private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
+ {
+ val middle_index = (array_start + array_stop) / 2
+ if (middle_index >= commands_offsets.length) return None
+ val (middle, (start, stop)) = commands_offsets(middle_index)
+ // does middle contain pos?
+ if (start <= pos && pos < stop)
+ Some(middle)
+ else if (start > pos)
+ find_command(pos, array_start, middle_index)
+ else if (stop <= pos)
+ find_command(pos, middle_index + 1, array_stop)
+ else error("impossible")
+ }
+}
--- a/src/Tools/jEdit/src/proofdocument/html_panel.scala Thu Dec 31 23:48:18 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/html_panel.scala Fri Jan 01 14:41:25 2010 +0100
@@ -14,7 +14,6 @@
import javax.swing.{JButton, JPanel, JScrollPane}
import java.util.logging.{Logger, Level}
-import org.w3c.dom.Document
import org.w3c.dom.html2.HTMLElement
import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
@@ -102,8 +101,8 @@
private val main_actor = actor {
// crude double buffering
- var doc1: Document = null
- var doc2: Document = null
+ var doc1: org.w3c.dom.Document = null
+ var doc2: org.w3c.dom.Document = null
loop {
react {
--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala Thu Dec 31 23:48:18 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,305 +0,0 @@
-/*
- * Document as list of commands, consisting of lists of tokens
- *
- * @author Johannes Hölzl, TU Munich
- * @author Fabian Immler, TU Munich
- * @author Makarius
- */
-
-package isabelle.proofdocument
-
-
-import scala.actors.Actor._
-
-import java.util.regex.Pattern
-
-
-object Proof_Document
-{
- // Be careful when changing this regex. Not only must it handle the
- // spurious end of a token but also:
- // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
- // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
-
- val token_pattern =
- Pattern.compile(
- "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
- "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
- "(\\?'?|')[A-Za-z_0-9.]*|" +
- "[A-Za-z_0-9.]+|" +
- "[!#$%&*+-/<=>?@^_|~]+|" +
- "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
- "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
- "[()\\[\\]{}:;]", Pattern.MULTILINE)
-
- def empty(id: Isar_Document.Document_ID): Proof_Document =
- new Proof_Document(id, Linear_Set(), Map(), Linear_Set(), Map())
-
- type StructureChange = List[(Option[Command], Option[Command])]
-}
-
-
-class Proof_Document(
- val id: Isar_Document.Document_ID,
- val tokens: Linear_Set[Token], // FIXME plain List, inside Command
- val token_start: Map[Token, Int], // FIXME eliminate
- val commands: Linear_Set[Command],
- var states: Map[Command, Command]) // FIXME immutable, eliminate!?
- extends Session.Entity
-{
- import Proof_Document.StructureChange
-
- def content = Token.string_from_tokens(Nil ++ tokens, token_start)
-
-
- /* accumulated messages */
-
- private val accumulator = actor {
- loop {
- react {
- case (session: Session, message: XML.Tree) =>
- message match {
- case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
- for {
- XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
- <- elems
- } {
- session.lookup_entity(cmd_id) match {
- case Some(cmd: Command) =>
- val state = cmd.finish_static(state_id)
- session.register_entity(state)
- states += (cmd -> state) // FIXME !?
- session.command_change.event(cmd) // FIXME really!?
- case _ =>
- }
- }
- case _ =>
- }
-
- case bad => System.err.println("document accumulator: ignoring bad message " + bad)
- }
- }
- }
-
- def consume(session: Session, message: XML.Tree) { accumulator ! (session, message) }
-
-
-
- /** token view **/
-
- def text_changed(session: Session, change: Change): (Proof_Document, StructureChange) =
- {
- def edit_doc(doc_chgs: (Proof_Document, StructureChange), edit: Edit) = {
- val (doc, chgs) = doc_chgs
- val (new_doc, chg) = doc.text_edit(session, edit, change.id)
- (new_doc, chgs ++ chg)
- }
- ((this, Nil: StructureChange) /: change.edits)(edit_doc)
- }
-
- def text_edit(session: Session, e: Edit, id: String): (Proof_Document, StructureChange) =
- {
- case class TextChange(start: Int, added: String, removed: String)
- val change = e match {
- case Insert(s, a) => TextChange(s, a, "")
- case Remove(s, r) => TextChange(s, "", r)
- }
- //indices of tokens
- var start: Map[Token, Int] = token_start
- def stop(t: Token) = start(t) + t.length
- // split old token lists
- val tokens = Nil ++ this.tokens
- val (begin, remaining) = tokens.span(stop(_) < change.start)
- val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length)
- // update indices
- start = end.foldLeft(start)((s, t) =>
- s + (t -> (s(t) + change.added.length - change.removed.length)))
-
- val split_begin = removed.takeWhile(start(_) < change.start).
- map (t => {
- val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
- start += (split_tok -> start(t))
- split_tok
- })
-
- val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length).
- map (t => {
- val split_tok =
- new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind)
- start += (split_tok -> start(t))
- split_tok
- })
- // update indices
- start = removed.foldLeft (start) ((s, t) => s - t)
- start = split_end.foldLeft (start) ((s, t) =>
- s + (t -> (change.start + change.added.length)))
-
- val ins = new Token(change.added, Token.Kind.OTHER)
- start += (ins -> change.start)
-
- var invalid_tokens = split_begin ::: ins :: split_end ::: end
- var new_tokens: List[Token] = Nil
- var old_suffix: List[Token] = Nil
-
- val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
- val matcher =
- Proof_Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
-
- while (matcher.find() && invalid_tokens != Nil) {
- val kind =
- if (session.current_syntax.is_command(matcher.group))
- Token.Kind.COMMAND_START
- else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
- Token.Kind.COMMENT
- else
- Token.Kind.OTHER
- val new_token = new Token(matcher.group, kind)
- start += (new_token -> (match_start + matcher.start))
- new_tokens ::= new_token
-
- invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
- invalid_tokens match {
- case t :: ts =>
- if (start(t) == start(new_token) &&
- start(t) > change.start + change.added.length) {
- old_suffix = t :: ts
- new_tokens = new_tokens.tail
- invalid_tokens = Nil
- }
- case _ =>
- }
- }
- val insert = new_tokens.reverse
- val new_token_list = begin ::: insert ::: old_suffix
- token_changed(session, id, begin.lastOption, insert,
- old_suffix.firstOption, new_token_list, start)
- }
-
-
- /** command view **/
-
- private def token_changed(
- session: Session,
- new_id: String,
- before_change: Option[Token],
- inserted_tokens: List[Token],
- after_change: Option[Token],
- new_tokens: List[Token],
- new_token_start: Map[Token, Int]):
- (Proof_Document, StructureChange) =
- {
- val new_tokenset = Linear_Set[Token]() ++ new_tokens
- val cmd_before_change = before_change match {
- case None => None
- case Some(bc) =>
- val cmd_with_bc = commands.find(_.contains(bc)).get
- if (cmd_with_bc.tokens.last == bc) {
- if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
- Some(cmd_with_bc)
- else commands.prev(cmd_with_bc)
- }
- else commands.prev(cmd_with_bc)
- }
-
- val cmd_after_change = after_change match {
- case None => None
- case Some(ac) =>
- val cmd_with_ac = commands.find(_.contains(ac)).get
- if (ac.is_start)
- Some(cmd_with_ac)
- else
- commands.next(cmd_with_ac)
- }
-
- val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
- takeWhile(Some(_) != cmd_after_change)
-
- // calculate inserted commands
- def tokens_to_commands(tokens: List[Token]): List[Command]= {
- tokens match {
- case Nil => Nil
- case t :: ts =>
- val (cmd, rest) =
- ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
- new Command(session.create_id(), t :: cmd, new_token_start) :: tokens_to_commands(rest)
- }
- }
-
- val split_begin =
- if (before_change.isDefined) {
- val changed =
- if (cmd_before_change.isDefined)
- new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
- else new_tokenset
- if (changed.exists(_ == before_change.get))
- changed.takeWhile(_ != before_change.get).toList :::
- List(before_change.get)
- else Nil
- } else Nil
-
- val split_end =
- if (after_change.isDefined) {
- val unchanged = new_tokens.dropWhile(_ != after_change.get)
- if(cmd_after_change.isDefined) {
- if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
- unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
- else Nil
- } else {
- unchanged
- }
- } else Nil
-
- val rescan_begin =
- split_begin :::
- before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
- val rescanning_tokens =
- after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
- split_end
- val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
-
- // build new document
- val new_commandset = commands.
- delete_between(cmd_before_change, cmd_after_change).
- append_after(cmd_before_change, inserted_commands)
-
-
- val doc =
- new Proof_Document(new_id, new_tokenset, new_token_start, new_commandset,
- states -- removed_commands)
-
- val removes =
- for (cmd <- removed_commands) yield (cmd_before_change -> None)
- val inserts =
- for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
-
- return (doc, removes.toList ++ inserts)
- }
-
- val commands_offsets = {
- var last_stop = 0
- (for (c <- commands) yield {
- val r = c -> (last_stop,c.stop(this))
- last_stop = c.stop(this)
- r
- }).toArray
- }
-
- def command_at(pos: Int): Option[Command] =
- find_command(pos, 0, commands_offsets.length)
-
- // use a binary search to find commands for a given offset
- private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
- {
- val middle_index = (array_start + array_stop) / 2
- if (middle_index >= commands_offsets.length) return None
- val (middle, (start, stop)) = commands_offsets(middle_index)
- // does middle contain pos?
- if (start <= pos && pos < stop)
- Some(middle)
- else if (start > pos)
- find_command(pos, array_start, middle_index)
- else if (stop <= pos)
- find_command(pos, middle_index + 1, array_stop)
- else error("impossible")
- }
-}
--- a/src/Tools/jEdit/src/proofdocument/session.scala Thu Dec 31 23:48:18 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala Fri Jan 01 14:41:25 2010 +0100
@@ -39,7 +39,7 @@
val results = new Event_Bus[Command]
val command_change = new Event_Bus[Command]
- val document_change = new Event_Bus[Proof_Document]
+ val document_change = new Event_Bus[Document]
/* unique ids */
@@ -57,8 +57,8 @@
def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
// FIXME eliminate
- @volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]()
- def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id)
+ @volatile private var documents = Map[Isar_Document.Document_ID, Document]()
+ def document(id: Isar_Document.Document_ID): Option[Document] = documents.get(id)
@@ -200,7 +200,7 @@
case Begin_Document(path: String) if prover != null =>
val id = create_id()
- val doc = Proof_Document.empty(id)
+ val doc = Document.empty(id)
register(doc)
documents += (id -> doc)
prover.begin_document(id, path)
@@ -229,6 +229,6 @@
def stop() { session_actor ! Stop }
def input(change: Change) { session_actor ! change }
- def begin_document(path: String): Proof_Document =
- (session_actor !? Begin_Document(path)).asInstanceOf[Proof_Document]
+ def begin_document(path: String): Document =
+ (session_actor !? Begin_Document(path)).asInstanceOf[Document]
}