# HG changeset patch # User wenzelm # Date 1392152311 -3600 # Node ID 9c53198dbb1cbed289c61d4377362e156a75b4bf # Parent e0f20a44ff9d33e1ff1967c805c83222d93c2640 maintain multiple command chunks and markup trees: for main chunk and loaded files; document view for all text areas, including auxiliary files; diff -r e0f20a44ff9d -r 9c53198dbb1c src/Pure/PIDE/command.scala --- 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) } diff -r e0f20a44ff9d -r 9c53198dbb1c src/Pure/PIDE/document.scala --- 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]], diff -r e0f20a44ff9d -r 9c53198dbb1c src/Pure/PIDE/protocol.scala --- 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 } } diff -r e0f20a44ff9d -r 9c53198dbb1c src/Tools/jEdit/src/document_model.scala --- 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 { diff -r e0f20a44ff9d -r 9c53198dbb1c src/Tools/jEdit/src/document_view.scala --- 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 = diff -r e0f20a44ff9d -r 9c53198dbb1c src/Tools/jEdit/src/isabelle_sidekick.scala --- 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 } } } diff -r e0f20a44ff9d -r 9c53198dbb1c src/Tools/jEdit/src/jedit_editor.scala --- 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 { diff -r e0f20a44ff9d -r 9c53198dbb1c src/Tools/jEdit/src/plugin.scala --- 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 => } } }