src/Pure/PIDE/command.scala
author wenzelm
Sun Aug 22 12:54:12 2010 +0200 (2010-08-22 ago)
changeset 38572 0fe2c01ef7da
parent 38564 a6e2715fac5f
child 38574 79cb7b4c908a
permissions -rw-r--r--
Command.State: accumulate markup reports uniformly;
Document_Model.token_marker: select relevant information directly from Markup_Tree, without intermediate HighlightInfo;
tuned;
wenzelm@36676
     1
/*  Title:      Pure/PIDE/command.scala
wenzelm@36676
     2
    Author:     Fabian Immler, TU Munich
wenzelm@36676
     3
    Author:     Makarius
wenzelm@36676
     4
wenzelm@36676
     5
Prover commands with semantic state.
wenzelm@36676
     6
*/
wenzelm@34407
     7
wenzelm@34871
     8
package isabelle
wenzelm@34318
     9
wenzelm@34451
    10
wenzelm@34699
    11
import scala.actors.Actor, Actor._
wenzelm@34497
    12
import scala.collection.mutable
wenzelm@34486
    13
wenzelm@34451
    14
wenzelm@34637
    15
object Command
wenzelm@34637
    16
{
wenzelm@34717
    17
  case class TypeInfo(ty: String)
wenzelm@34707
    18
  case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@38363
    19
    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
wenzelm@38361
    20
wenzelm@38361
    21
wenzelm@38362
    22
wenzelm@38361
    23
  /** accumulated results from prover **/
wenzelm@38361
    24
wenzelm@38362
    25
  case class State(
wenzelm@38361
    26
    val command: Command,
wenzelm@38480
    27
    val status: List[XML.Tree],
wenzelm@38361
    28
    val reverse_results: List[XML.Tree],
wenzelm@38479
    29
    val markup: Markup_Tree)
wenzelm@38361
    30
  {
wenzelm@38361
    31
    /* content */
wenzelm@38361
    32
wenzelm@38362
    33
    lazy val results = reverse_results.reverse
wenzelm@38361
    34
wenzelm@38362
    35
    def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
wenzelm@38361
    36
wenzelm@38564
    37
    def add_markup(node: Markup_Tree.Node[Any]): State = copy(markup = markup + node)
wenzelm@38479
    38
wenzelm@38564
    39
    def markup_root_node: Markup_Tree.Node[Any] =
wenzelm@38480
    40
      new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
wenzelm@38479
    41
    def markup_root: Markup_Tree = markup + markup_root_node
wenzelm@38361
    42
wenzelm@38361
    43
wenzelm@38361
    44
    /* markup */
wenzelm@38361
    45
wenzelm@38564
    46
    private lazy val types: List[Markup_Tree.Node[Any]] =
wenzelm@38362
    47
      markup.filter(_.info match {
wenzelm@38361
    48
        case Command.TypeInfo(_) => true
wenzelm@38479
    49
        case _ => false }).flatten(markup_root_node)
wenzelm@38361
    50
wenzelm@38426
    51
    def type_at(pos: Text.Offset): Option[String] =
wenzelm@38361
    52
    {
wenzelm@38427
    53
      types.find(_.range.contains(pos)) match {
wenzelm@38361
    54
        case Some(t) =>
wenzelm@38361
    55
          t.info match {
wenzelm@38426
    56
            case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
wenzelm@38361
    57
            case _ => None
wenzelm@38361
    58
          }
wenzelm@38361
    59
        case None => None
wenzelm@38361
    60
      }
wenzelm@38361
    61
    }
wenzelm@38361
    62
wenzelm@38564
    63
    private lazy val refs: List[Markup_Tree.Node[Any]] =
wenzelm@38362
    64
      markup.filter(_.info match {
wenzelm@38361
    65
        case Command.RefInfo(_, _, _, _) => true
wenzelm@38479
    66
        case _ => false }).flatten(markup_root_node)
wenzelm@38361
    67
wenzelm@38564
    68
    def ref_at(pos: Text.Offset): Option[Markup_Tree.Node[Any]] =
wenzelm@38427
    69
      refs.find(_.range.contains(pos))
wenzelm@38361
    70
wenzelm@38361
    71
wenzelm@38361
    72
    /* message dispatch */
wenzelm@38361
    73
wenzelm@38361
    74
    def accumulate(message: XML.Tree): Command.State =
wenzelm@38361
    75
      message match {
wenzelm@38480
    76
        case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
wenzelm@38572
    77
        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
wenzelm@38572
    78
          (this /: msgs)((state, msg) =>
wenzelm@38572
    79
            msg match {
wenzelm@38572
    80
              case XML.Elem(Markup(name, atts), args)
wenzelm@38572
    81
              if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
wenzelm@38572
    82
                val range = command.decode_range(Position.get_range(atts).get)
wenzelm@38572
    83
                val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
wenzelm@38572
    84
                val node = Markup_Tree.Node[Any](range, XML.Elem(Markup(name, props), args))
wenzelm@38572
    85
                add_markup(node)
wenzelm@38572
    86
              case _ => System.err.println("Ignored report message: " + msg); state
wenzelm@38361
    87
            })
wenzelm@38361
    88
        case _ => add_result(message)
wenzelm@38361
    89
      }
wenzelm@38361
    90
  }
wenzelm@38367
    91
wenzelm@38367
    92
wenzelm@38367
    93
  /* unparsed dummy commands */
wenzelm@38367
    94
wenzelm@38367
    95
  def unparsed(source: String) =
wenzelm@38367
    96
    new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
wenzelm@34318
    97
}
wenzelm@34318
    98
wenzelm@38361
    99
wenzelm@34697
   100
class Command(
wenzelm@38150
   101
    val id: Document.Command_ID,
wenzelm@38373
   102
    val span: List[Token])
wenzelm@34451
   103
{
wenzelm@34859
   104
  /* classification */
wenzelm@34500
   105
wenzelm@36012
   106
  def is_command: Boolean = !span.isEmpty && span.head.is_command
wenzelm@34865
   107
  def is_ignored: Boolean = span.forall(_.is_ignored)
wenzelm@34859
   108
  def is_malformed: Boolean = !is_command && !is_ignored
wenzelm@34859
   109
wenzelm@38367
   110
  def is_unparsed = id == Document.NO_ID
wenzelm@38367
   111
wenzelm@36012
   112
  def name: String = if (is_command) span.head.content else ""
wenzelm@37129
   113
  override def toString =
wenzelm@37373
   114
    id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
wenzelm@34495
   115
wenzelm@34859
   116
wenzelm@34859
   117
  /* source text */
wenzelm@34451
   118
wenzelm@34859
   119
  val source: String = span.map(_.source).mkString
wenzelm@38426
   120
  def source(range: Text.Range): String = source.substring(range.start, range.stop)
wenzelm@34859
   121
  def length: Int = source.length
wenzelm@38572
   122
wenzelm@38479
   123
  val range: Text.Range = Text.Range(0, length)
wenzelm@34855
   124
wenzelm@34859
   125
  lazy val symbol_index = new Symbol.Index(source)
wenzelm@38572
   126
  def decode_range(r: Text.Range): Text.Range = symbol_index.decode(r)
wenzelm@38370
   127
wenzelm@38370
   128
wenzelm@38370
   129
  /* accumulated results */
wenzelm@38370
   130
wenzelm@38479
   131
  val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
immler@34676
   132
}