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@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@51496:     def make(es: Iterable[Results.Entry]): Results = (empty /: es.iterator)(_ + _)
wenzelm@50507:     def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
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@51496:     def entries: 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@50508:       else (this /: other.entries)(_ + _)
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@50540:     override def toString: String = entries.mkString("Results(", ", ", ")")
wenzelm@50507:   }
wenzelm@50507: 
wenzelm@50507: 
wenzelm@50507:   /* state */
wenzelm@50501: 
wenzelm@43714:   sealed case class State(
wenzelm@50501:     command: Command,
wenzelm@50501:     status: List[Markup] = Nil,
wenzelm@50507:     results: Results = Results.empty,
wenzelm@50501:     markup: Markup_Tree = Markup_Tree.empty)
wenzelm@38361:   {
wenzelm@49645:     def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
wenzelm@49645:       markup.to_XML(command.range, command.source, filter)
wenzelm@49614: 
wenzelm@49614: 
wenzelm@51494:     /* content */
wenzelm@51494: 
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@51494:       markup == other.markup
wenzelm@38361: 
wenzelm@46152:     private def add_status(st: Markup): State = copy(status = st :: status)
wenzelm@46152:     private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
wenzelm@38361: 
wenzelm@52531:     def + (alt_id: Document_ID.Generic, 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@50499:                 state.add_status(markup)
wenzelm@50499:                   .add_markup(Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
wenzelm@46152: 
wenzelm@52536:               case _ =>
wenzelm@52536:                 java.lang.System.err.println("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@38572:             msg match {
wenzelm@39173:               case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
wenzelm@49527:               if (id == command.id || id == alt_id) &&
wenzelm@49527:                   command.range.contains(command.decode(raw_range)) =>
wenzelm@39173:                 val range = command.decode(raw_range)
wenzelm@38872:                 val props = Position.purge(atts)
wenzelm@45455:                 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
wenzelm@38723:                 state.add_markup(info)
wenzelm@49526:               case XML.Elem(Markup(name, atts), args)
wenzelm@50201:               if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
wenzelm@49037:                 val range = command.proper_range
wenzelm@49037:                 val props = Position.purge(atts)
wenzelm@49037:                 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
wenzelm@49037:                 state.add_markup(info)
wenzelm@40572:               case _ =>
wenzelm@52536:                 // FIXME java.lang.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@50201:             case Markup.Serial(i) =>
wenzelm@50163:               val props = Position.purge(atts)
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@50163:               val st0 = copy(results = results + (i -> message1))
wenzelm@39441:               val st1 =
wenzelm@50500:                 if (Protocol.is_inlined(message))
wenzelm@45709:                   (st0 /: Protocol.message_positions(command, message))(
wenzelm@50163:                     (st, range) => st.add_markup(Text.Info(range, message2)))
wenzelm@50500:                 else st0
wenzelm@49445: 
wenzelm@49445:               st1
wenzelm@52536:             case _ =>
wenzelm@52536:               java.lang.System.err.println("Ignored message without serial number: " + message)
wenzelm@52536:               this
wenzelm@38872:           }
wenzelm@38361:       }
wenzelm@52527: 
wenzelm@52527:     def ++ (other: State): State =
wenzelm@52527:       copy(results = results ++ other.results)  // FIXME merge more content!?
wenzelm@38361:   }
wenzelm@38367: 
wenzelm@38367: 
wenzelm@45644:   /* make commands */
wenzelm@45644: 
wenzelm@48745:   type Span = List[Token]
wenzelm@48745: 
wenzelm@52524:   def apply(
wenzelm@52530:     id: Document_ID.Command,
wenzelm@52524:     node_name: Document.Node.Name,
wenzelm@52524:     span: Span,
wenzelm@52524:     results: Results = Results.empty,
wenzelm@52524:     markup: Markup_Tree = Markup_Tree.empty): Command =
wenzelm@45644:   {
wenzelm@45644:     val source: String =
wenzelm@48745:       span match {
wenzelm@45644:         case List(tok) => tok.source
wenzelm@48745:         case _ => span.map(_.source).mkString
wenzelm@45644:       }
wenzelm@45644: 
wenzelm@48745:     val span1 = new mutable.ListBuffer[Token]
wenzelm@45644:     var i = 0
wenzelm@48745:     for (Token(kind, s) <- span) {
wenzelm@45644:       val n = s.length
wenzelm@45644:       val s1 = source.substring(i, i + n)
wenzelm@48745:       span1 += Token(kind, s1)
wenzelm@45644:       i += n
wenzelm@45644:     }
wenzelm@45644: 
wenzelm@50501:     new Command(id, node_name, span1.toList, source, results, markup)
wenzelm@45644:   }
wenzelm@45644: 
wenzelm@52530:   val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil)
wenzelm@49414: 
wenzelm@52530:   def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
wenzelm@50501:       : Command =
wenzelm@50501:     Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
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@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@52535:     val span: List[Token],
wenzelm@49414:     val source: String,
wenzelm@50501:     val init_results: Command.Results,
wenzelm@49414:     val init_markup: Markup_Tree)
wenzelm@34451: {
wenzelm@34859:   /* classification */
wenzelm@34500: 
wenzelm@52530:   def is_undefined: Boolean = id == Document_ID.none
wenzelm@48754:   val is_unparsed: Boolean = span.exists(_.is_unparsed)
wenzelm@48754:   val is_unfinished: Boolean = span.exists(_.is_unfinished)
wenzelm@44385: 
wenzelm@48599:   val is_ignored: Boolean = !span.exists(_.is_proper)
wenzelm@48754:   val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error))
wenzelm@47012:   def is_command: Boolean = !is_ignored && !is_malformed
wenzelm@34859: 
wenzelm@47012:   def name: String =
wenzelm@48718:     span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
wenzelm@47012: 
wenzelm@37129:   override def toString =
wenzelm@37373:     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
wenzelm@34495: 
wenzelm@34859: 
wenzelm@52509:   /* source */
wenzelm@34451: 
wenzelm@46813:   def length: Int = source.length
wenzelm@46813:   val range: Text.Range = Text.Range(0, length)
wenzelm@46813: 
wenzelm@46813:   val proper_range: Text.Range =
wenzelm@51048:     Text.Range(0, (length /: span.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@52507:   lazy val symbol_index = 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@50501:   val init_state: Command.State =
wenzelm@50501:     Command.State(this, results = init_results, markup = init_markup)
wenzelm@52527: 
wenzelm@52527:   val empty_state: Command.State = Command.State(this)
immler@34676: }