# HG changeset patch # User wenzelm # Date 1376300998 -7200 # Node ID 8fd8e1c149886b399187bd91377f251a38d2b7c4 # Parent 31926d2c04eee78d650e236f597090935819033f tuned signature; diff -r 31926d2c04ee -r 8fd8e1c14988 src/Pure/PIDE/document.scala --- 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 && diff -r 31926d2c04ee -r 8fd8e1c14988 src/Tools/jEdit/src/graphview_dockable.scala --- 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]) { diff -r 31926d2c04ee -r 8fd8e1c14988 src/Tools/jEdit/src/info_dockable.scala --- 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) { diff -r 31926d2c04ee -r 8fd8e1c14988 src/Tools/jEdit/src/output_dockable.scala --- 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) diff -r 31926d2c04ee -r 8fd8e1c14988 src/Tools/jEdit/src/pretty_text_area.scala --- 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 diff -r 31926d2c04ee -r 8fd8e1c14988 src/Tools/jEdit/src/query_operation.scala --- 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) diff -r 31926d2c04ee -r 8fd8e1c14988 src/Tools/jEdit/src/text_overview.scala --- 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