wenzelm@38483: /*  Title:      Pure/PIDE/isar_document.scala
wenzelm@38412:     Author:     Makarius
wenzelm@38412: 
wenzelm@38567: Protocol message formats for interactive Isar documents.
wenzelm@38412: */
wenzelm@38412: 
wenzelm@38412: package isabelle
wenzelm@38412: 
wenzelm@38412: 
wenzelm@38412: object Isar_Document
wenzelm@38412: {
wenzelm@38567:   /* document editing */
wenzelm@38412: 
wenzelm@38412:   object Assign {
wenzelm@38414:     def unapply(msg: XML.Tree)
wenzelm@38414:         : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
wenzelm@38412:       msg match {
wenzelm@38414:         case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
wenzelm@38412:           val id_edits = edits.map(Edit.unapply)
wenzelm@38414:           if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
wenzelm@38412:           else None
wenzelm@38412:         case _ => None
wenzelm@38412:       }
wenzelm@38412:   }
wenzelm@38412: 
wenzelm@38412:   object Edit {
wenzelm@38412:     def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
wenzelm@38412:       msg match {
wenzelm@38414:         case XML.Elem(
wenzelm@38414:           Markup(Markup.EDIT,
wenzelm@38414:             List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
wenzelm@38412:         case _ => None
wenzelm@38412:       }
wenzelm@38412:   }
wenzelm@38567: 
wenzelm@38567: 
wenzelm@38567:   /* toplevel transactions */
wenzelm@38567: 
wenzelm@38567:   sealed abstract class Status
wenzelm@38567:   case class Forked(forks: Int) extends Status
wenzelm@38567:   case object Unprocessed extends Status
wenzelm@38567:   case object Finished extends Status
wenzelm@38567:   case object Failed extends Status
wenzelm@38567: 
wenzelm@38581:   def command_status(markup: List[Markup]): Status =
wenzelm@38567:   {
wenzelm@38567:     val forks = (0 /: markup) {
wenzelm@38581:       case (i, Markup(Markup.FORKED, _)) => i + 1
wenzelm@38581:       case (i, Markup(Markup.JOINED, _)) => i - 1
wenzelm@38567:       case (i, _) => i
wenzelm@38567:     }
wenzelm@38567:     if (forks != 0) Forked(forks)
wenzelm@38581:     else if (markup.exists(_.name == Markup.FAILED)) Failed
wenzelm@38581:     else if (markup.exists(_.name == Markup.FINISHED)) Finished
wenzelm@38567:     else Unprocessed
wenzelm@38567:   }
wenzelm@38887: 
wenzelm@38887: 
wenzelm@39441:   /* result messages */
wenzelm@39439: 
wenzelm@39439:   def clean_message(body: XML.Body): XML.Body =
wenzelm@39439:     body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
wenzelm@39439:       { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
wenzelm@39439: 
wenzelm@39441:   def message_reports(msg: XML.Tree): List[XML.Elem] =
wenzelm@39441:     msg match {
wenzelm@39441:       case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
wenzelm@39441:       case XML.Elem(_, body) => body.flatMap(message_reports)
wenzelm@39441:       case XML.Text(_) => Nil
wenzelm@39441:     }
wenzelm@39441: 
wenzelm@39439: 
wenzelm@39511:   /* specific messages */
wenzelm@39511: 
wenzelm@39625:   def is_ready(msg: XML.Tree): Boolean =
wenzelm@39625:     msg match {
wenzelm@39625:       case XML.Elem(Markup(Markup.STATUS, _),
wenzelm@39625:         List(XML.Elem(Markup(Markup.READY, _), _))) => true
wenzelm@39625:       case _ => false
wenzelm@39625:     }
wenzelm@39625: 
wenzelm@39625:  def is_tracing(msg: XML.Tree): Boolean =
wenzelm@39622:     msg match {
wenzelm@39622:       case XML.Elem(Markup(Markup.TRACING, _), _) => true
wenzelm@39622:       case _ => false
wenzelm@39622:     }
wenzelm@39622: 
wenzelm@39511:   def is_warning(msg: XML.Tree): Boolean =
wenzelm@39511:     msg match {
wenzelm@39511:       case XML.Elem(Markup(Markup.WARNING, _), _) => true
wenzelm@39511:       case _ => false
wenzelm@39511:     }
wenzelm@39511: 
wenzelm@39511:   def is_error(msg: XML.Tree): Boolean =
wenzelm@39511:     msg match {
wenzelm@39511:       case XML.Elem(Markup(Markup.ERROR, _), _) => true
wenzelm@39511:       case _ => false
wenzelm@39511:     }
wenzelm@38887: 
wenzelm@39441:   def is_state(msg: XML.Tree): Boolean =
wenzelm@39170:     msg match {
wenzelm@39627:       case XML.Elem(Markup(Markup.WRITELN, _),
wenzelm@39627:         List(XML.Elem(Markup(Markup.STATE, _), _))) => true
wenzelm@39170:       case _ => false
wenzelm@39170:     }
wenzelm@39170: 
wenzelm@39511: 
wenzelm@39511:   /* reported positions */
wenzelm@39511: 
wenzelm@39627:   private val include_pos =
wenzelm@39627:     Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
wenzelm@39441: 
wenzelm@39441:   def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
wenzelm@38887:   {
wenzelm@39441:     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
wenzelm@38887:       tree match {
wenzelm@39172:         case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
wenzelm@39172:         if include_pos(name) && id == command.id =>
wenzelm@39172:           val range = command.decode(raw_range).restrict(command.range)
wenzelm@39441:           body.foldLeft(if (range.is_singularity) set else set + range)(positions)
wenzelm@39441:         case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
wenzelm@39042:         case _ => set
wenzelm@38887:       }
wenzelm@39441:     val set = positions(Set.empty, message)
wenzelm@39170:     if (set.isEmpty && !is_state(message))
wenzelm@39172:       set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
wenzelm@39042:     else set
wenzelm@38887:   }
wenzelm@38412: }
wenzelm@38412: 
wenzelm@38412: 
wenzelm@38412: trait Isar_Document extends Isabelle_Process
wenzelm@38412: {
wenzelm@38412:   /* commands */
wenzelm@38412: 
wenzelm@38412:   def define_command(id: Document.Command_ID, text: String): Unit =
wenzelm@38414:     input("Isar_Document.define_command", Document.ID(id), text)
wenzelm@38412: 
wenzelm@38412: 
wenzelm@38417:   /* document versions */
wenzelm@38412: 
wenzelm@38417:   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
wenzelm@44157:     edits: List[Document.Edit_Command_ID])
wenzelm@38412:   {
wenzelm@44157:     val edits_yxml =
wenzelm@43767:     { import XML.Encode._
wenzelm@44156:       def encode: T[List[Document.Edit_Command_ID]] =
wenzelm@44156:         list(pair(string,
wenzelm@44156:           variant(List(
wenzelm@44156:             { case Document.Node.Remove() => (Nil, Nil) },
wenzelm@44157:             { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
wenzelm@44182:             { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
wenzelm@44157:                 (Nil, triple(string, list(string), list(string))(a, b, c)) },
wenzelm@44182:             { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
wenzelm@44157:       YXML.string_of_body(encode(edits)) }
wenzelm@38412: 
wenzelm@44157:     input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
wenzelm@38412:   }
wenzelm@43748: 
wenzelm@43748: 
wenzelm@43748:   /* method invocation service */
wenzelm@43748: 
wenzelm@43748:   def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
wenzelm@43748:   {
wenzelm@43748:     input("Isar_Document.invoke_scala", id, tag.toString, res)
wenzelm@43748:   }
wenzelm@38412: }