wenzelm@36676: /* Title: Pure/PIDE/command.scala wenzelm@36676: Author: Fabian Immler, TU Munich wenzelm@36676: Author: Makarius wenzelm@36676: wenzelm@52536: Prover commands with accumulated results from execution. wenzelm@36676: */ wenzelm@34407: wenzelm@34871: package isabelle wenzelm@34318: wenzelm@34451: wenzelm@45644: import scala.collection.mutable wenzelm@38872: import scala.collection.immutable.SortedMap wenzelm@38872: wenzelm@38872: wenzelm@34637: object Command wenzelm@34637: { wenzelm@52849: type Edit = (Option[Command], Option[Command]) wenzelm@56746: type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])] wenzelm@55648: wenzelm@52849: wenzelm@52849: wenzelm@38361: /** accumulated results from prover **/ wenzelm@38361: wenzelm@50507: /* results */ wenzelm@50507: wenzelm@50507: object Results wenzelm@50507: { wenzelm@51496: type Entry = (Long, XML.Tree) wenzelm@50507: val empty = new Results(SortedMap.empty) wenzelm@56299: def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _) wenzelm@56299: def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _) wenzelm@50507: } wenzelm@50507: wenzelm@51494: final class Results private(private val rep: SortedMap[Long, XML.Tree]) wenzelm@50507: { wenzelm@50507: def defined(serial: Long): Boolean = rep.isDefinedAt(serial) wenzelm@50507: def get(serial: Long): Option[XML.Tree] = rep.get(serial) wenzelm@56372: def iterator: Iterator[Results.Entry] = rep.iterator wenzelm@50508: wenzelm@51496: def + (entry: Results.Entry): Results = wenzelm@50508: if (defined(entry._1)) this wenzelm@50508: else new Results(rep + entry) wenzelm@50508: wenzelm@50508: def ++ (other: Results): Results = wenzelm@50508: if (this eq other) this wenzelm@50508: else if (rep.isEmpty) other wenzelm@56372: else (this /: other.iterator)(_ + _) wenzelm@50540: wenzelm@51494: override def hashCode: Int = rep.hashCode wenzelm@51494: override def equals(that: Any): Boolean = wenzelm@51494: that match { wenzelm@51494: case other: Results => rep == other.rep wenzelm@51494: case _ => false wenzelm@51494: } wenzelm@56372: override def toString: String = iterator.mkString("Results(", ", ", ")") wenzelm@50507: } wenzelm@50507: wenzelm@50507: wenzelm@55649: /* markup */ wenzelm@55649: wenzelm@55649: object Markup_Index wenzelm@55649: { wenzelm@56746: val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) wenzelm@55649: } wenzelm@55649: wenzelm@56746: sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) wenzelm@55649: wenzelm@55649: object Markups wenzelm@55649: { wenzelm@55649: val empty: Markups = new Markups(Map.empty) wenzelm@55649: wenzelm@55649: def init(markup: Markup_Tree): Markups = wenzelm@55649: new Markups(Map(Markup_Index.markup -> markup)) wenzelm@55649: } wenzelm@55649: wenzelm@55649: final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) wenzelm@55649: { wenzelm@56489: def is_empty: Boolean = rep.isEmpty wenzelm@56489: wenzelm@55649: def apply(index: Markup_Index): Markup_Tree = wenzelm@55649: rep.getOrElse(index, Markup_Tree.empty) wenzelm@55649: wenzelm@55649: def add(index: Markup_Index, markup: Text.Markup): Markups = wenzelm@55649: new Markups(rep + (index -> (this(index) + markup))) wenzelm@55649: wenzelm@56475: def redirection_iterator: Iterator[Document_ID.Generic] = wenzelm@56746: for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) wenzelm@56475: yield id wenzelm@56470: wenzelm@56475: def redirect(other_id: Document_ID.Generic): Markups = wenzelm@56489: { wenzelm@56489: val rep1 = wenzelm@56470: (for { wenzelm@56746: (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator wenzelm@56470: if other_id == id wenzelm@56746: } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap wenzelm@56489: if (rep1.isEmpty) Markups.empty else new Markups(rep1) wenzelm@56489: } wenzelm@56470: wenzelm@55649: override def hashCode: Int = rep.hashCode wenzelm@55649: override def equals(that: Any): Boolean = wenzelm@55649: that match { wenzelm@55649: case other: Markups => rep == other.rep wenzelm@55649: case _ => false wenzelm@55649: } wenzelm@55649: override def toString: String = rep.iterator.mkString("Markups(", ", ", ")") wenzelm@55649: } wenzelm@55649: wenzelm@55649: wenzelm@50507: /* state */ wenzelm@50501: wenzelm@56299: object State wenzelm@56299: { wenzelm@56299: def merge_results(states: List[State]): Command.Results = wenzelm@56299: Results.merge(states.map(_.results)) wenzelm@56299: wenzelm@56301: def merge_markup(states: List[State], index: Markup_Index, wenzelm@56743: range: Text.Range, elements: Markup.Elements): Markup_Tree = wenzelm@56301: Markup_Tree.merge(states.map(_.markup(index)), range, elements) wenzelm@56299: } wenzelm@56299: wenzelm@43714: sealed case class State( wenzelm@50501: command: Command, wenzelm@50501: status: List[Markup] = Nil, wenzelm@50507: results: Results = Results.empty, wenzelm@55649: markups: Markups = Markups.empty) wenzelm@38361: { wenzelm@56395: lazy val protocol_status: Protocol.Status = wenzelm@56395: { wenzelm@56395: val warnings = wenzelm@56395: if (results.iterator.exists(p => Protocol.is_warning(p._2))) wenzelm@56395: List(Markup(Markup.WARNING, Nil)) wenzelm@56395: else Nil wenzelm@56395: val errors = wenzelm@56395: if (results.iterator.exists(p => Protocol.is_error(p._2))) wenzelm@56395: List(Markup(Markup.ERROR, Nil)) wenzelm@56395: else Nil wenzelm@56395: Protocol.Status.make((warnings ::: errors ::: status).iterator) wenzelm@56395: } wenzelm@55432: wenzelm@55650: def markup(index: Markup_Index): Markup_Tree = markups(index) wenzelm@55432: wenzelm@56489: def redirect(other_command: Command): Option[State] = wenzelm@56489: { wenzelm@56489: val markups1 = markups.redirect(other_command.id) wenzelm@56489: if (markups1.is_empty) None wenzelm@56489: else Some(new State(other_command, Nil, Results.empty, markups1)) wenzelm@56489: } wenzelm@49614: wenzelm@51494: def eq_content(other: State): Boolean = wenzelm@51494: command.source == other.command.source && wenzelm@51494: status == other.status && wenzelm@51494: results == other.results && wenzelm@55434: markups == other.markups wenzelm@38361: wenzelm@55649: private def add_status(st: Markup): State = wenzelm@55649: copy(status = st :: status) wenzelm@55432: wenzelm@56746: private def add_markup( wenzelm@56746: status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = wenzelm@55649: { wenzelm@55649: val markups1 = wenzelm@56395: if (status || Protocol.liberal_status_elements(m.info.name)) wenzelm@56462: markups.add(Markup_Index(true, chunk_name), m) wenzelm@55649: else markups wenzelm@56462: copy(markups = markups1.add(Markup_Index(false, chunk_name), m)) wenzelm@55649: } wenzelm@38361: wenzelm@56470: def accumulate( wenzelm@56470: self_id: Document_ID.Generic => Boolean, wenzelm@56746: other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], wenzelm@56470: message: XML.Elem): State = wenzelm@38361: message match { wenzelm@50201: case XML.Elem(Markup(Markup.STATUS, _), msgs) => wenzelm@38714: (this /: msgs)((state, msg) => wenzelm@38714: msg match { wenzelm@46152: case elem @ XML.Elem(markup, Nil) => wenzelm@55649: state. wenzelm@55649: add_status(markup). wenzelm@56746: add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem)) wenzelm@52536: case _ => wenzelm@56782: Output.warning("Ignored status message: " + msg) wenzelm@52536: state wenzelm@38714: }) wenzelm@38581: wenzelm@50201: case XML.Elem(Markup(Markup.REPORT, _), msgs) => wenzelm@38572: (this /: msgs)((state, msg) => wenzelm@55432: { wenzelm@56782: def bad(): Unit = Output.warning("Ignored report message: " + msg) wenzelm@55432: wenzelm@55432: msg match { wenzelm@57911: case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) => wenzelm@56470: wenzelm@56470: val target = wenzelm@56470: if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) wenzelm@56470: Some((chunk_name, command.chunks(chunk_name))) wenzelm@56746: else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id) wenzelm@56470: else None wenzelm@56470: wenzelm@57911: (target, atts) match { wenzelm@57911: case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => wenzelm@56470: target_chunk.incorporate(symbol_range) match { wenzelm@55548: case Some(range) => wenzelm@55822: val props = Position.purge(atts) wenzelm@55822: val info = Text.Info(range, XML.Elem(Markup(name, props), args)) wenzelm@56470: state.add_markup(false, target_name, info) wenzelm@55548: case None => bad(); state wenzelm@55432: } wenzelm@57911: case _ => wenzelm@56514: // silently ignore excessive reports wenzelm@56476: state wenzelm@55432: } wenzelm@55432: wenzelm@55432: case XML.Elem(Markup(name, atts), args) wenzelm@55432: if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => wenzelm@55432: val range = command.proper_range wenzelm@55432: val props = Position.purge(atts) wenzelm@55432: val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) wenzelm@56746: state.add_markup(false, Symbol.Text_Chunk.Default, info) wenzelm@55432: wenzelm@56470: case _ => bad(); state wenzelm@55432: } wenzelm@38361: }) wenzelm@52930: case XML.Elem(Markup(name, props), body) => wenzelm@52930: props match { wenzelm@50201: case Markup.Serial(i) => wenzelm@50201: val message1 = XML.Elem(Markup(Markup.message(name), props), body) wenzelm@50163: val message2 = XML.Elem(Markup(name, props), body) wenzelm@50163: wenzelm@55433: var st = copy(results = results + (i -> message1)) wenzelm@55433: if (Protocol.is_inlined(message)) { wenzelm@55433: for { wenzelm@56469: (chunk_name, chunk) <- command.chunks.iterator wenzelm@57911: range <- Protocol.message_positions( wenzelm@57911: self_id, command.position, chunk_name, chunk, message) wenzelm@56462: } st = st.add_markup(false, chunk_name, Text.Info(range, message2)) wenzelm@55433: } wenzelm@55433: st wenzelm@55432: wenzelm@52536: case _ => wenzelm@56782: Output.warning("Ignored message without serial number: " + message) wenzelm@52536: this wenzelm@38872: } wenzelm@56295: } wenzelm@38361: } wenzelm@38367: wenzelm@38367: wenzelm@55431: wenzelm@55431: /** static content **/ wenzelm@55431: wenzelm@45644: /* make commands */ wenzelm@45644: wenzelm@55648: def apply( wenzelm@55648: id: Document_ID.Command, wenzelm@55648: node_name: Document.Node.Name, wenzelm@55648: blobs: List[Blob], wenzelm@57905: span: Command_Span.Span): Command = wenzelm@55648: { wenzelm@57901: val (source, span1) = span.compact_source wenzelm@55648: new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty) wenzelm@55648: } wenzelm@49414: wenzelm@57901: val empty: Command = wenzelm@57905: Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty) wenzelm@55648: wenzelm@55648: def unparsed( wenzelm@55648: id: Document_ID.Command, wenzelm@55648: source: String, wenzelm@55648: results: Results, wenzelm@55648: markup: Markup_Tree): Command = wenzelm@55648: { wenzelm@57905: val (source1, span1) = Command_Span.unparsed(source).compact_source wenzelm@57901: new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup) wenzelm@55648: } wenzelm@49414: wenzelm@50501: def unparsed(source: String): Command = wenzelm@52530: unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty) wenzelm@44384: wenzelm@52530: def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = wenzelm@49414: { wenzelm@49466: val text = XML.content(body) wenzelm@49466: val markup = Markup_Tree.from_XML(body) wenzelm@50501: unparsed(id, text, results, markup) wenzelm@49414: } wenzelm@49359: wenzelm@44384: wenzelm@44384: /* perspective */ wenzelm@44384: wenzelm@44474: object Perspective wenzelm@44474: { wenzelm@44474: val empty: Perspective = Perspective(Nil) wenzelm@44474: } wenzelm@44385: wenzelm@44474: sealed case class Perspective(commands: List[Command]) // visible commands in canonical order wenzelm@44385: { wenzelm@57615: def is_empty: Boolean = commands.isEmpty wenzelm@57615: wenzelm@44474: def same(that: Perspective): Boolean = wenzelm@44474: { wenzelm@44474: val cmds1 = this.commands wenzelm@44474: val cmds2 = that.commands wenzelm@48754: require(!cmds1.exists(_.is_undefined)) wenzelm@48754: require(!cmds2.exists(_.is_undefined)) wenzelm@44474: cmds1.length == cmds2.length && wenzelm@44474: (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) wenzelm@44474: } wenzelm@44385: } wenzelm@34318: } wenzelm@34318: wenzelm@38361: wenzelm@46712: final class Command private( wenzelm@52530: val id: Document_ID.Command, wenzelm@44615: val node_name: Document.Node.Name, wenzelm@54519: val blobs: List[Command.Blob], wenzelm@57905: val span: Command_Span.Span, wenzelm@49414: val source: String, wenzelm@50501: val init_results: Command.Results, wenzelm@49414: val init_markup: Markup_Tree) wenzelm@34451: { wenzelm@57910: /* name */ wenzelm@34859: wenzelm@57901: def name: String = wenzelm@57910: span.kind match { case Command_Span.Command_Span(name, _) => name case _ => "" } wenzelm@57910: wenzelm@57910: def position: Position.T = wenzelm@57910: span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none } wenzelm@47012: wenzelm@57912: override def toString: String = id + "/" + span.kind.toString wenzelm@34495: wenzelm@57910: wenzelm@57910: /* classification */ wenzelm@57910: wenzelm@57905: def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span] wenzelm@57905: def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span wenzelm@57904: wenzelm@57904: def is_undefined: Boolean = id == Document_ID.none wenzelm@57904: val is_unparsed: Boolean = span.content.exists(_.is_unparsed) wenzelm@57904: val is_unfinished: Boolean = span.content.exists(_.is_unfinished) wenzelm@57904: wenzelm@34859: wenzelm@54519: /* blobs */ wenzelm@54519: wenzelm@54530: def blobs_names: List[Document.Node.Name] = wenzelm@54530: for (Exn.Res((name, _)) <- blobs) yield name wenzelm@54530: wenzelm@57842: def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] = wenzelm@57842: for (Exn.Res((name, Some((digest, _)))) <- blobs) yield (name, digest) wenzelm@57842: wenzelm@57842: def blobs_changed(doc_blobs: Document.Blobs): Boolean = wenzelm@57842: blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false }) wenzelm@54519: wenzelm@55432: wenzelm@56462: /* source chunks */ wenzelm@55431: wenzelm@56746: val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) wenzelm@56473: wenzelm@56746: val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = wenzelm@56746: ((Symbol.Text_Chunk.Default -> chunk) :: wenzelm@56473: (for (Exn.Res((name, Some((_, file)))) <- blobs) wenzelm@56746: yield (Symbol.Text_Chunk.File(name.node) -> file))).toMap wenzelm@56473: wenzelm@46813: def length: Int = source.length wenzelm@56473: def range: Text.Range = chunk.range wenzelm@46813: wenzelm@46813: val proper_range: Text.Range = wenzelm@57901: Text.Range(0, wenzelm@57901: (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length)) wenzelm@46813: wenzelm@38426: def source(range: Text.Range): String = source.substring(range.start, range.stop) wenzelm@38572: wenzelm@38370: wenzelm@38370: /* accumulated results */ wenzelm@38370: wenzelm@50501: val init_state: Command.State = wenzelm@55649: Command.State(this, results = init_results, markups = Command.Markups.init(init_markup)) wenzelm@52527: wenzelm@52527: val empty_state: Command.State = Command.State(this) immler@34676: }