maintain multiple command chunks and markup trees: for main chunk and loaded files;
document view for all text areas, including auxiliary files;
--- a/src/Pure/PIDE/command.scala Tue Feb 11 17:44:29 2014 +0100
+++ b/src/Pure/PIDE/command.scala Tue Feb 11 21:58:31 2014 +0100
@@ -60,8 +60,13 @@
command: Command,
status: List[Markup] = Nil,
results: Results = Results.empty,
- markup: Markup_Tree = Markup_Tree.empty)
+ markups: Map[String, Markup_Tree] = Map.empty)
{
+ def get_markup(file_name: String): Markup_Tree =
+ markups.getOrElse(file_name, Markup_Tree.empty)
+
+ def markup: Markup_Tree = get_markup("")
+
def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
markup.to_XML(command.range, command.source, filter)
@@ -75,7 +80,9 @@
markup == other.markup
private def add_status(st: Markup): State = copy(status = st :: status)
- private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
+
+ private def add_markup(file_name: String, m: Text.Markup): State =
+ copy(markups = markups + (file_name -> (get_markup(file_name) + m)))
def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
message match {
@@ -84,7 +91,7 @@
msg match {
case elem @ XML.Elem(markup, Nil) =>
state.add_status(markup)
- .add_markup(Text.Info(command.proper_range, elem)) // FIXME cumulation order!?
+ .add_markup("", Text.Info(command.proper_range, elem)) // FIXME cumulation order!?
case _ =>
java.lang.System.err.println("Ignored status message: " + msg)
@@ -93,23 +100,40 @@
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
- msg match {
- case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
- if (id == command.id || id == alt_id) && file_name == "" &&
- command.range.contains(command.decode(raw_range)) =>
- val range = command.decode(raw_range)
- val props = Position.purge(atts)
- val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
- state.add_markup(info)
- case XML.Elem(Markup(name, atts), args)
- if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
- val range = command.proper_range
- val props = Position.purge(atts)
- val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
- state.add_markup(info)
- case _ =>
- // FIXME java.lang.System.err.println("Ignored report message: " + msg)
- state
+ {
+ def bad(): Unit = java.lang.System.err.println("Ignored report message: " + msg)
+
+ msg match {
+ case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
+ if id == command.id || id == alt_id =>
+ command.chunks.get(file_name) match {
+ case Some(chunk) =>
+ val range = chunk.decode(raw_range)
+ if (chunk.range.contains(range)) {
+ val props = Position.purge(atts)
+ val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
+ state.add_markup(file_name, info)
+ }
+ else {
+ bad()
+ state
+ }
+ case None =>
+ bad()
+ state
+ }
+
+ case XML.Elem(Markup(name, atts), args)
+ if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
+ val range = command.proper_range
+ val props = Position.purge(atts)
+ val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
+ state.add_markup("", info)
+
+ case _ =>
+ // FIXME bad()
+ state
+ }
})
case XML.Elem(Markup(name, props), body) =>
props match {
@@ -119,12 +143,18 @@
val st0 = copy(results = results + (i -> message1))
val st1 =
- if (Protocol.is_inlined(message))
- (st0 /: Protocol.message_positions(command.id, command, message))(
- (st, range) => st.add_markup(Text.Info(range, message2)))
+ if (Protocol.is_inlined(message)) {
+ var st1 = st0
+ for {
+ (file_name, chunk) <- command.chunks
+ range <- Protocol.message_positions(command.id, chunk, message)
+ } st1 = st1.add_markup(file_name, Text.Info(range, message2))
+ st1
+ }
else st0
st1
+
case _ =>
java.lang.System.err.println("Ignored message without serial number: " + message)
this
@@ -135,7 +165,10 @@
copy(
status = other.status ::: status,
results = results ++ other.results,
- markup = markup ++ other.markup)
+ markups =
+ (markups.keySet ++ other.markups.keySet)
+ .map(a => a -> (get_markup(a) ++ other.get_markup(a))).toMap
+ )
}
@@ -268,6 +301,10 @@
def blobs_digests: List[SHA1.Digest] =
for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
+ val chunks: Map[String, Command.Chunk] =
+ (("" -> this) ::
+ (for (Exn.Res((name, Some((_, file)))) <- blobs) yield (name.node -> file))).toMap
+
/* source */
@@ -289,7 +326,7 @@
/* accumulated results */
val init_state: Command.State =
- Command.State(this, results = init_results, markup = init_markup)
+ Command.State(this, results = init_results, markups = Map("" -> init_markup))
val empty_state: Command.State = Command.State(this)
}
--- a/src/Pure/PIDE/document.scala Tue Feb 11 17:44:29 2014 +0100
+++ b/src/Pure/PIDE/document.scala Tue Feb 11 21:58:31 2014 +0100
@@ -361,6 +361,7 @@
val node_name: Node.Name
val node: Node
+ val thy_load_commands: List[Command]
def eq_content(other: Snapshot): Boolean
def cumulate_markup[A](
range: Text.Range,
@@ -608,6 +609,10 @@
val node_name = name
val node = version.nodes(name)
+ val thy_load_commands: List[Command] =
+ if (node_name.is_theory) Nil
+ else version.nodes.thy_load_commands(node_name)
+
def eq_content(other: Snapshot): Boolean =
!is_outdated && !other.is_outdated &&
node.commands.size == other.node.commands.size &&
@@ -621,15 +626,30 @@
result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
{
val former_range = revert(range)
- (for {
- (command, command_start) <- node.command_range(former_range)
- st = state.command_state(version, command)
- res = result(st)
- Text.Info(r0, a) <- st.markup.cumulate[A](
- (former_range - command_start).restrict(command.range), info, elements,
- { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
- ).iterator
- } yield Text.Info(convert(r0 + command_start), a)).toList
+ thy_load_commands match {
+ case thy_load_command :: _ =>
+ val file_name = node_name.node
+ (for {
+ chunk <- thy_load_command.chunks.get(file_name).iterator
+ st = state.command_state(version, thy_load_command)
+ res = result(st)
+ Text.Info(r0, a) <- st.get_markup(file_name).cumulate[A](
+ former_range.restrict(chunk.range), info, elements,
+ { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
+ ).iterator
+ } yield Text.Info(convert(r0), a)).toList
+
+ case _ =>
+ (for {
+ (command, command_start) <- node.command_range(former_range)
+ st = state.command_state(version, command)
+ res = result(st)
+ Text.Info(r0, a) <- st.markup.cumulate[A](
+ (former_range - command_start).restrict(command.range), info, elements,
+ { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
+ ).iterator
+ } yield Text.Info(convert(r0 + command_start), a)).toList
+ }
}
def select_markup[A](range: Text.Range, elements: Option[Set[String]],
--- a/src/Pure/PIDE/protocol.scala Tue Feb 11 17:44:29 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala Tue Feb 11 21:58:31 2014 +0100
@@ -302,8 +302,14 @@
}
val set = positions(Set.empty, message)
- if (set.isEmpty)
- set ++ Position.Range.unapply(message.markup.properties).map(chunk.decode(_))
+ if (set.isEmpty) {
+ message.markup.properties match {
+ case Position.Reported(id, file_name, range)
+ if id == command_id && file_name == chunk.file_name =>
+ set + chunk.decode(range)
+ case _ => set
+ }
+ }
else set
}
}
--- a/src/Tools/jEdit/src/document_model.scala Tue Feb 11 17:44:29 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Feb 11 21:58:31 2014 +0100
@@ -106,10 +106,13 @@
val snapshot = this.snapshot()
val document_view_ranges =
- for {
- doc_view <- PIDE.document_views(buffer)
- range <- doc_view.perspective(snapshot).ranges
- } yield range
+ if (is_theory) {
+ for {
+ doc_view <- PIDE.document_views(buffer)
+ range <- doc_view.perspective(snapshot).ranges
+ } yield range
+ }
+ else Nil
val thy_load_ranges =
for {
--- a/src/Tools/jEdit/src/document_view.scala Tue Feb 11 17:44:29 2014 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Tue Feb 11 21:58:31 2014 +0100
@@ -210,14 +210,18 @@
if (model.buffer == text_area.getBuffer) {
val snapshot = model.snapshot()
- if (changed.assignment ||
+ val thy_load_changed =
+ snapshot.thy_load_commands.exists(changed.commands.contains)
+
+ if (changed.assignment || thy_load_changed ||
(changed.nodes.contains(model.node_name) &&
changed.commands.exists(snapshot.node.commands.contains)))
Swing_Thread.later { overview.delay_repaint.invoke() }
val visible_lines = text_area.getVisibleLines
if (visible_lines > 0) {
- if (changed.assignment) text_area.invalidateScreenLineRange(0, visible_lines)
+ if (changed.assignment || thy_load_changed)
+ text_area.invalidateScreenLineRange(0, visible_lines)
else {
val visible_range = JEdit_Lib.visible_range(text_area).get
val visible_cmds =
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Feb 11 17:44:29 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Feb 11 21:58:31 2014 +0100
@@ -148,8 +148,9 @@
{
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
- Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
- case Some(snapshot) =>
+ Swing_Thread.now { Document_Model(buffer) } match {
+ case Some(model) if model.is_theory =>
+ val snapshot = model.snapshot
val root = data.root
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
Isabelle_Sidekick.swing_markup_tree(
@@ -171,7 +172,7 @@
})
}
true
- case None => false
+ case _ => false
}
}
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Feb 11 17:44:29 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Feb 11 21:58:31 2014 +0100
@@ -69,7 +69,7 @@
val buffer = view.getBuffer
PIDE.document_view(text_area) match {
- case Some(doc_view) =>
+ case Some(doc_view) if doc_view.model.is_theory =>
val node = snapshot.version.nodes(doc_view.model.node_name)
val caret = snapshot.revert(text_area.getCaretPosition)
if (caret < buffer.getLength) {
@@ -81,7 +81,7 @@
else None
}
else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
- case None =>
+ case _ =>
PIDE.document_model(buffer) match {
case Some(model) if !model.is_theory =>
snapshot.version.nodes.thy_load_commands(model.node_name) match {
--- a/src/Tools/jEdit/src/plugin.scala Tue Feb 11 17:44:29 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Feb 11 21:58:31 2014 +0100
@@ -114,12 +114,10 @@
val model = Document_Model.init(session, buffer, node_name)
(model.init_edits(), model)
}
- if (model.is_theory) {
- for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
- if (document_view(text_area).map(_.model) != Some(model))
- Document_View.init(model, text_area)
- }
- }
+ for {
+ text_area <- JEdit_Lib.jedit_text_areas(buffer)
+ if document_view(text_area).map(_.model) != Some(model)
+ } Document_View.init(model, text_area)
model_edits ::: edits
}
}
@@ -132,8 +130,8 @@
{
JEdit_Lib.swing_buffer_lock(buffer) {
document_model(buffer) match {
- case Some(model) if model.is_theory => Document_View.init(model, text_area)
- case _ =>
+ case Some(model) => Document_View.init(model, text_area)
+ case None =>
}
}
}