wenzelm@36676: /* Title: Pure/PIDE/command.scala wenzelm@36676: Author: Fabian Immler, TU Munich wenzelm@36676: Author: Makarius wenzelm@36676: wenzelm@36676: Prover commands with semantic state. wenzelm@36676: */ wenzelm@34407: wenzelm@34871: package isabelle wenzelm@34318: wenzelm@43520: import java.lang.System wenzelm@34451: wenzelm@38872: import scala.collection.immutable.SortedMap wenzelm@38872: wenzelm@38872: wenzelm@34637: object Command wenzelm@34637: { wenzelm@38361: /** accumulated results from prover **/ wenzelm@38361: wenzelm@43714: sealed case class State( wenzelm@38361: val command: Command, wenzelm@38872: val status: List[Markup] = Nil, wenzelm@38872: val results: SortedMap[Long, XML.Tree] = SortedMap.empty, wenzelm@38872: val markup: Markup_Tree = Markup_Tree.empty) wenzelm@38361: { wenzelm@38361: /* content */ wenzelm@38361: wenzelm@38714: def add_status(st: Markup): State = copy(status = st :: status) wenzelm@38714: def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info) wenzelm@38872: def add_result(serial: Long, result: XML.Tree): State = wenzelm@38872: copy(results = results + (serial -> result)) wenzelm@38361: wenzelm@38658: def root_info: Text.Info[Any] = wenzelm@38581: new Text.Info(command.range, wenzelm@38658: XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil)))) wenzelm@38658: def root_markup: Markup_Tree = markup + root_info wenzelm@38361: wenzelm@38361: wenzelm@38361: /* message dispatch */ wenzelm@38361: wenzelm@38872: def accumulate(message: XML.Elem): Command.State = wenzelm@38361: message match { wenzelm@38714: case XML.Elem(Markup(Markup.STATUS, _), msgs) => wenzelm@38714: (this /: msgs)((state, msg) => wenzelm@38714: msg match { wenzelm@38714: case XML.Elem(markup, Nil) => state.add_status(markup) wenzelm@38714: case _ => System.err.println("Ignored status message: " + msg); state wenzelm@38714: }) wenzelm@38581: wenzelm@38572: case XML.Elem(Markup(Markup.REPORT, _), msgs) => wenzelm@38572: (this /: msgs)((state, msg) => wenzelm@38572: msg match { wenzelm@39173: case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args) wenzelm@39173: if id == command.id && command.range.contains(command.decode(raw_range)) => wenzelm@39173: val range = command.decode(raw_range) wenzelm@38872: val props = Position.purge(atts) wenzelm@39173: val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args)) wenzelm@38723: state.add_markup(info) wenzelm@40572: case _ => wenzelm@40572: // FIXME System.err.println("Ignored report message: " + msg) wenzelm@40572: state wenzelm@38361: }) wenzelm@38872: case XML.Elem(Markup(name, atts), body) => wenzelm@38872: atts match { wenzelm@38872: case Markup.Serial(i) => wenzelm@38887: val result = XML.Elem(Markup(name, Position.purge(atts)), body) wenzelm@39622: val st0 = add_result(i, result) wenzelm@39441: val st1 = wenzelm@39622: if (Isar_Document.is_tracing(message)) st0 wenzelm@39622: else wenzelm@39622: (st0 /: Isar_Document.message_positions(command, message))( wenzelm@39622: (st, range) => st.add_markup(Text.Info(range, result))) wenzelm@39622: val st2 = (st1 /: Isar_Document.message_reports(message))(_ accumulate _) wenzelm@39622: st2 wenzelm@38872: case _ => System.err.println("Ignored message without serial number: " + message); this wenzelm@38872: } wenzelm@38361: } wenzelm@38361: } wenzelm@38367: wenzelm@38367: wenzelm@40454: /* dummy commands */ wenzelm@38367: wenzelm@40454: def unparsed(source: String): Command = wenzelm@43662: new Command(Document.no_id, List(Token(Token.Kind.UNPARSED, source))) wenzelm@40454: wenzelm@40454: def span(toks: List[Token]): Command = wenzelm@43662: new Command(Document.no_id, toks) wenzelm@44384: wenzelm@44384: wenzelm@44384: /* perspective */ wenzelm@44384: wenzelm@44384: type Perspective = List[Command] // visible commands in canonical order wenzelm@44385: wenzelm@44385: def equal_perspective(p1: Perspective, p2: Perspective): Boolean = wenzelm@44385: { wenzelm@44385: require(p1.forall(_.is_defined)) wenzelm@44385: require(p2.forall(_.is_defined)) wenzelm@44385: p1.length == p2.length && wenzelm@44385: (p1.iterator zip p2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) wenzelm@44385: } wenzelm@34318: } wenzelm@34318: wenzelm@38361: wenzelm@34697: class Command( wenzelm@38150: val id: Document.Command_ID, wenzelm@38373: val span: List[Token]) wenzelm@34451: { wenzelm@34859: /* classification */ wenzelm@34500: wenzelm@44385: def is_defined: Boolean = id != Document.no_id wenzelm@44385: wenzelm@36012: def is_command: Boolean = !span.isEmpty && span.head.is_command wenzelm@34865: def is_ignored: Boolean = span.forall(_.is_ignored) wenzelm@34859: def is_malformed: Boolean = !is_command && !is_ignored wenzelm@34859: wenzelm@36012: def name: String = if (is_command) span.head.content else "" wenzelm@37129: override def toString = wenzelm@37373: id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") wenzelm@34495: wenzelm@34859: wenzelm@34859: /* source text */ wenzelm@34451: wenzelm@34859: val source: String = span.map(_.source).mkString wenzelm@38426: def source(range: Text.Range): String = source.substring(range.start, range.stop) wenzelm@34859: def length: Int = source.length wenzelm@38572: wenzelm@38877: val newlines = wenzelm@38877: (0 /: Symbol.iterator(source)) { wenzelm@38877: case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n } wenzelm@38877: wenzelm@38479: val range: Text.Range = Text.Range(0, length) wenzelm@34855: wenzelm@34859: lazy val symbol_index = new Symbol.Index(source) wenzelm@38579: def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) wenzelm@38579: def decode(r: Text.Range): Text.Range = symbol_index.decode(r) wenzelm@38370: wenzelm@38370: wenzelm@38370: /* accumulated results */ wenzelm@38370: wenzelm@38872: val empty_state: Command.State = Command.State(this) immler@34676: }