--- a/src/Pure/PIDE/document.scala Mon Aug 12 11:39:29 2013 +0200
+++ b/src/Pure/PIDE/document.scala Mon Aug 12 11:49:58 2013 +0200
@@ -324,17 +324,23 @@
/** global state -- document structure, execution process, editing history **/
+ object Snapshot
+ {
+ val init = State.init.snapshot()
+ }
+
abstract class Snapshot
{
val state: State
val version: Version
- val node_name: Node.Name
- val node: Node
val is_outdated: Boolean
def convert(i: Text.Offset): Text.Offset
def revert(i: Text.Offset): Text.Offset
def convert(range: Text.Range): Text.Range
def revert(range: Text.Range): Text.Range
+
+ val node_name: Node.Name
+ val node: Node
def eq_content(other: Snapshot): Boolean
def cumulate_markup[A](
range: Text.Range,
@@ -555,10 +561,10 @@
new Snapshot
{
+ /* global information */
+
val state = State.this
val version = stable.version.get_finished
- val node_name = name
- val node = version.nodes(name)
val is_outdated = !(pending_edits.isEmpty && latest == stable)
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
@@ -566,6 +572,12 @@
def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
+
+ /* local node content */
+
+ val node_name = name
+ val node = version.nodes(name)
+
def eq_content(other: Snapshot): Boolean =
!is_outdated && !other.is_outdated &&
node.commands.size == other.node.commands.size &&
--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Aug 12 11:39:29 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Aug 12 11:49:58 2013 +0200
@@ -22,7 +22,7 @@
{
/* implicit arguments -- owned by Swing thread */
- private var implicit_snapshot = Document.State.init.snapshot()
+ private var implicit_snapshot = Document.Snapshot.init
private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph"))
private var implicit_graph = no_graph
@@ -36,7 +36,7 @@
}
private def reset_implicit(): Unit =
- set_implicit(Document.State.init.snapshot(), no_graph)
+ set_implicit(Document.Snapshot.init, no_graph)
def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
{
--- a/src/Tools/jEdit/src/info_dockable.scala Mon Aug 12 11:39:29 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Mon Aug 12 11:49:58 2013 +0200
@@ -25,7 +25,7 @@
{
/* implicit arguments -- owned by Swing thread */
- private var implicit_snapshot = Document.State.init.snapshot()
+ private var implicit_snapshot = Document.Snapshot.init
private var implicit_results = Command.Results.empty
private var implicit_info: XML.Body = Nil
@@ -39,7 +39,7 @@
}
private def reset_implicit(): Unit =
- set_implicit(Document.State.init.snapshot(), Command.Results.empty, Nil)
+ set_implicit(Document.Snapshot.init, Command.Results.empty, Nil)
def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
{
--- a/src/Tools/jEdit/src/output_dockable.scala Mon Aug 12 11:39:29 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Mon Aug 12 11:49:58 2013 +0200
@@ -30,7 +30,7 @@
private var zoom_factor = 100
private var do_update = true
- private var current_snapshot = Document.State.init.snapshot()
+ private var current_snapshot = Document.Snapshot.init
private var current_state = Command.empty.init_state
private var current_output: List[XML.Tree] = Nil
@@ -62,7 +62,7 @@
case Some(cmd) =>
(snapshot, snapshot.state.command_state(snapshot.version, cmd))
case None =>
- (Document.State.init.snapshot(), Command.empty.init_state)
+ (Document.Snapshot.init, Command.empty.init_state)
}
}
else (current_snapshot, current_state)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Aug 12 11:39:29 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Aug 12 11:49:58 2013 +0200
@@ -64,7 +64,7 @@
private var current_font_family = "Dialog"
private var current_font_size: Int = 12
private var current_body: XML.Body = Nil
- private var current_base_snapshot = Document.State.init.snapshot()
+ private var current_base_snapshot = Document.Snapshot.init
private var current_base_results = Command.Results.empty
private var current_rendering: Rendering =
Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
--- a/src/Tools/jEdit/src/query_operation.scala Mon Aug 12 11:39:29 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala Mon Aug 12 11:49:58 2013 +0200
@@ -83,7 +83,7 @@
val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
(snapshot, state, removed)
case None =>
- (Document.State.init.snapshot(), Command.empty.init_state, true)
+ (Document.Snapshot.init, Command.empty.init_state, true)
}
val results =
@@ -161,7 +161,7 @@
val snapshot = doc_view.model.snapshot()
remove_overlay()
reset_state()
- consume_output(Document.State.init.snapshot(), Command.Results.empty, Nil)
+ consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
case Some(command) =>
current_location = Some(command)
--- a/src/Tools/jEdit/src/text_overview.scala Mon Aug 12 11:39:29 2013 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala Mon Aug 12 11:49:58 2013 +0200
@@ -53,7 +53,7 @@
private var cached_colors: List[(Color, Int, Int)] = Nil
- private var last_snapshot = Document.State.init.snapshot()
+ private var last_snapshot = Document.Snapshot.init
private var last_options = PIDE.options.value
private var last_relevant_range = Text.Range(0)
private var last_line_count = 0