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@34451: 
wenzelm@34699: import scala.actors.Actor, Actor._
wenzelm@34497: import scala.collection.mutable
wenzelm@34486: 
wenzelm@34451: 
wenzelm@34637: object Command
wenzelm@34637: {
wenzelm@34637:   object Status extends Enumeration
wenzelm@34637:   {
wenzelm@34318:     val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318:     val FINISHED = Value("FINISHED")
wenzelm@34318:     val FAILED = Value("FAILED")
wenzelm@36990:     val UNDEFINED = Value("UNDEFINED")
wenzelm@34318:   }
wenzelm@34707: 
wenzelm@37197:   case class HighlightInfo(kind: String, sub_kind: Option[String]) {
wenzelm@37197:     override def toString = kind
wenzelm@37197:   }
wenzelm@34717:   case class TypeInfo(ty: String)
wenzelm@34707:   case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@38355:     command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
wenzelm@38361: 
wenzelm@38361: 
wenzelm@38361:   /** accumulated results from prover **/
wenzelm@38361: 
wenzelm@38361:   class State(
wenzelm@38361:     val command: Command,
wenzelm@38361:     val status: Command.Status.Value,
wenzelm@38361:     val forks: Int,
wenzelm@38361:     val reverse_results: List[XML.Tree],
wenzelm@38361:     val markup_root: Markup_Text)
wenzelm@38361:   {
wenzelm@38361:     def this(command: Command) =
wenzelm@38361:       this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
wenzelm@38361: 
wenzelm@38361: 
wenzelm@38361:     /* content */
wenzelm@38361: 
wenzelm@38361:     private def set_status(st: Command.Status.Value): State =
wenzelm@38361:       new State(command, st, forks, reverse_results, markup_root)
wenzelm@38361: 
wenzelm@38361:     private def add_forks(i: Int): State =
wenzelm@38361:       new State(command, status, forks + i, reverse_results, markup_root)
wenzelm@38361: 
wenzelm@38361:     private def add_result(res: XML.Tree): State =
wenzelm@38361:       new State(command, status, forks, res :: reverse_results, markup_root)
wenzelm@38361: 
wenzelm@38361:     private def add_markup(node: Markup_Tree): State =
wenzelm@38361:       new State(command, status, forks, reverse_results, markup_root + node)
wenzelm@38361: 
wenzelm@38361:     lazy val results = reverse_results.reverse
wenzelm@38361: 
wenzelm@38361: 
wenzelm@38361:     /* markup */
wenzelm@38361: 
wenzelm@38361:     lazy val highlight: Markup_Text =
wenzelm@38361:     {
wenzelm@38361:       markup_root.filter(_.info match {
wenzelm@38361:         case Command.HighlightInfo(_, _) => true
wenzelm@38361:         case _ => false
wenzelm@38361:       })
wenzelm@38361:     }
wenzelm@38361: 
wenzelm@38361:     private lazy val types: List[Markup_Node] =
wenzelm@38361:       markup_root.filter(_.info match {
wenzelm@38361:         case Command.TypeInfo(_) => true
wenzelm@38361:         case _ => false }).flatten
wenzelm@38361: 
wenzelm@38361:     def type_at(pos: Int): Option[String] =
wenzelm@38361:     {
wenzelm@38361:       types.find(t => t.start <= pos && pos < t.stop) match {
wenzelm@38361:         case Some(t) =>
wenzelm@38361:           t.info match {
wenzelm@38361:             case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
wenzelm@38361:             case _ => None
wenzelm@38361:           }
wenzelm@38361:         case None => None
wenzelm@38361:       }
wenzelm@38361:     }
wenzelm@38361: 
wenzelm@38361:     private lazy val refs: List[Markup_Node] =
wenzelm@38361:       markup_root.filter(_.info match {
wenzelm@38361:         case Command.RefInfo(_, _, _, _) => true
wenzelm@38361:         case _ => false }).flatten
wenzelm@38361: 
wenzelm@38361:     def ref_at(pos: Int): Option[Markup_Node] =
wenzelm@38361:       refs.find(t => t.start <= pos && pos < t.stop)
wenzelm@38361: 
wenzelm@38361: 
wenzelm@38361:     /* message dispatch */
wenzelm@38361: 
wenzelm@38361:     def accumulate(message: XML.Tree): Command.State =
wenzelm@38361:       message match {
wenzelm@38361:         case XML.Elem(Markup(Markup.STATUS, _), elems) =>
wenzelm@38361:           (this /: elems)((state, elem) =>
wenzelm@38361:             elem match {
wenzelm@38361:               case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
wenzelm@38361:               case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
wenzelm@38361:               case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
wenzelm@38361:               case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
wenzelm@38361:               case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
wenzelm@38361:               case _ => System.err.println("Ignored status message: " + elem); state
wenzelm@38361:             })
wenzelm@38361: 
wenzelm@38361:         case XML.Elem(Markup(Markup.REPORT, _), elems) =>
wenzelm@38361:           (this /: elems)((state, elem) =>
wenzelm@38361:             elem match {
wenzelm@38361:               case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
wenzelm@38361:                 atts match {
wenzelm@38361:                   case Position.Range(begin, end) =>
wenzelm@38361:                     if (kind == Markup.ML_TYPING) {
wenzelm@38361:                       val info = Pretty.string_of(body, margin = 40)
wenzelm@38361:                       state.add_markup(
wenzelm@38361:                         command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
wenzelm@38361:                     }
wenzelm@38361:                     else if (kind == Markup.ML_REF) {
wenzelm@38361:                       body match {
wenzelm@38361:                         case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
wenzelm@38361:                           state.add_markup(command.markup_node(
wenzelm@38361:                             begin - 1, end - 1,
wenzelm@38361:                             Command.RefInfo(
wenzelm@38361:                               Position.get_file(props),
wenzelm@38361:                               Position.get_line(props),
wenzelm@38361:                               Position.get_id(props),
wenzelm@38361:                               Position.get_offset(props))))
wenzelm@38361:                         case _ => state
wenzelm@38361:                       }
wenzelm@38361:                     }
wenzelm@38361:                     else {
wenzelm@38361:                       state.add_markup(
wenzelm@38361:                         command.markup_node(begin - 1, end - 1,
wenzelm@38361:                           Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
wenzelm@38361:                     }
wenzelm@38361:                   case _ => state
wenzelm@38361:                 }
wenzelm@38361:               case _ => System.err.println("Ignored report message: " + elem); state
wenzelm@38361:             })
wenzelm@38361:         case _ => add_result(message)
wenzelm@38361:       }
wenzelm@38361:   }
wenzelm@34318: }
wenzelm@34318: 
wenzelm@38361: 
wenzelm@34697: class Command(
wenzelm@38150:     val id: Document.Command_ID,
wenzelm@37129:     val span: Thy_Syntax.Span,
wenzelm@38220:     val static_parent: Option[Command] = None)  // FIXME !?
wenzelm@34815:   extends Session.Entity
wenzelm@34451: {
wenzelm@34859:   /* classification */
wenzelm@34500: 
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@34859:   def source(i: Int, j: Int): String = source.substring(i, j)
wenzelm@34859:   def length: Int = source.length
wenzelm@34855: 
wenzelm@34859:   lazy val symbol_index = new Symbol.Index(source)
immler@34593: 
wenzelm@34815: 
wenzelm@34815:   /* accumulated messages */
wenzelm@34815: 
wenzelm@38361:   @volatile protected var state = new Command.State(this)
wenzelm@38361:   def current_state: Command.State = state
wenzelm@34815: 
wenzelm@37129:   private case class Consume(message: XML.Tree, forward: Command => Unit)
wenzelm@34832:   private case object Assign
wenzelm@34815: 
wenzelm@34815:   private val accumulator = actor {
wenzelm@34832:     var assigned = false
wenzelm@34815:     loop {
wenzelm@34815:       react {
wenzelm@37129:         case Consume(message, forward) if !assigned =>
wenzelm@37129:           val old_state = state
wenzelm@37178:           state = old_state.accumulate(message)
wenzelm@37129:           if (!(state eq old_state)) forward(static_parent getOrElse this)
wenzelm@34815: 
wenzelm@34832:         case Assign =>
wenzelm@34835:           assigned = true  // single assignment
wenzelm@34832:           reply(())
wenzelm@34815: 
wenzelm@37189:         case bad => System.err.println("Command accumulator: ignoring bad message " + bad)
wenzelm@34815:       }
wenzelm@34815:     }
wenzelm@34815:   }
wenzelm@34815: 
wenzelm@37129:   def consume(message: XML.Tree, forward: Command => Unit)
wenzelm@37129:   {
wenzelm@37129:     accumulator ! Consume(message, forward)
wenzelm@37129:   }
wenzelm@34815: 
wenzelm@38150:   def assign_state(state_id: Document.State_ID): Command =
wenzelm@34815:   {
wenzelm@37129:     val cmd = new Command(state_id, span, Some(this))
wenzelm@34832:     accumulator !? Assign
wenzelm@34815:     cmd.state = current_state
wenzelm@34815:     cmd
wenzelm@34815:   }
immler@34676: 
immler@34676: 
immler@34676:   /* markup */
wenzelm@34508: 
wenzelm@34859:   lazy val empty_markup = new Markup_Text(Nil, source)
immler@34676: 
wenzelm@34717:   def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
wenzelm@34699:   {
wenzelm@34703:     val start = symbol_index.decode(begin)
wenzelm@34703:     val stop = symbol_index.decode(end)
wenzelm@34717:     new Markup_Tree(new Markup_Node(start, stop, info), Nil)
wenzelm@34500:   }
immler@34676: }