src/Pure/PIDE/command.scala
author wenzelm
Wed Aug 18 23:44:50 2010 +0200 (2010-08-18 ago)
changeset 38479 e628da370072
parent 38476 d72479a07882
child 38480 e5eed57913d0
permissions -rw-r--r--
more efficient Markup_Tree, based on branches sorted by quasi-order;
renamed markup_node.scala to markup_tree.scala and classes/objects accordingly;
Position.Range: produce actual Text.Range;
Symbol.Index.decode: convert 1-based Isabelle offsets here;
added static Command.range;
simplified Command.markup;
Document_Model.token_marker: flatten markup at most once;
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@37197
    17
  case class HighlightInfo(kind: String, sub_kind: Option[String]) {
wenzelm@37197
    18
    override def toString = kind
wenzelm@37197
    19
  }
wenzelm@34717
    20
  case class TypeInfo(ty: String)
wenzelm@34707
    21
  case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@38363
    22
    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
wenzelm@38361
    23
wenzelm@38361
    24
wenzelm@38362
    25
wenzelm@38361
    26
  /** accumulated results from prover **/
wenzelm@38361
    27
wenzelm@38362
    28
  case class State(
wenzelm@38361
    29
    val command: Command,
wenzelm@38429
    30
    val status: List[Markup],
wenzelm@38361
    31
    val reverse_results: List[XML.Tree],
wenzelm@38479
    32
    val markup: Markup_Tree)
wenzelm@38361
    33
  {
wenzelm@38361
    34
    /* content */
wenzelm@38361
    35
wenzelm@38362
    36
    lazy val results = reverse_results.reverse
wenzelm@38361
    37
wenzelm@38362
    38
    def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
wenzelm@38361
    39
wenzelm@38479
    40
    def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node)
wenzelm@38479
    41
wenzelm@38479
    42
    def markup_root_node: Markup_Tree.Node = new Markup_Tree.Node(command.range, status)
wenzelm@38479
    43
    def markup_root: Markup_Tree = markup + markup_root_node
wenzelm@38361
    44
wenzelm@38361
    45
wenzelm@38361
    46
    /* markup */
wenzelm@38361
    47
wenzelm@38479
    48
    lazy val highlight: List[Markup_Tree.Node] =
wenzelm@38361
    49
    {
wenzelm@38362
    50
      markup.filter(_.info match {
wenzelm@38361
    51
        case Command.HighlightInfo(_, _) => true
wenzelm@38361
    52
        case _ => false
wenzelm@38479
    53
      }).flatten(markup_root_node)
wenzelm@38361
    54
    }
wenzelm@38361
    55
wenzelm@38479
    56
    private lazy val types: List[Markup_Tree.Node] =
wenzelm@38362
    57
      markup.filter(_.info match {
wenzelm@38361
    58
        case Command.TypeInfo(_) => true
wenzelm@38479
    59
        case _ => false }).flatten(markup_root_node)
wenzelm@38361
    60
wenzelm@38426
    61
    def type_at(pos: Text.Offset): Option[String] =
wenzelm@38361
    62
    {
wenzelm@38427
    63
      types.find(_.range.contains(pos)) match {
wenzelm@38361
    64
        case Some(t) =>
wenzelm@38361
    65
          t.info match {
wenzelm@38426
    66
            case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
wenzelm@38361
    67
            case _ => None
wenzelm@38361
    68
          }
wenzelm@38361
    69
        case None => None
wenzelm@38361
    70
      }
wenzelm@38361
    71
    }
wenzelm@38361
    72
wenzelm@38479
    73
    private lazy val refs: List[Markup_Tree.Node] =
wenzelm@38362
    74
      markup.filter(_.info match {
wenzelm@38361
    75
        case Command.RefInfo(_, _, _, _) => true
wenzelm@38479
    76
        case _ => false }).flatten(markup_root_node)
wenzelm@38361
    77
wenzelm@38479
    78
    def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] =
wenzelm@38427
    79
      refs.find(_.range.contains(pos))
wenzelm@38361
    80
wenzelm@38361
    81
wenzelm@38361
    82
    /* message dispatch */
wenzelm@38361
    83
wenzelm@38361
    84
    def accumulate(message: XML.Tree): Command.State =
wenzelm@38361
    85
      message match {
wenzelm@38361
    86
        case XML.Elem(Markup(Markup.STATUS, _), elems) =>
wenzelm@38429
    87
          copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status)
wenzelm@38361
    88
wenzelm@38361
    89
        case XML.Elem(Markup(Markup.REPORT, _), elems) =>
wenzelm@38361
    90
          (this /: elems)((state, elem) =>
wenzelm@38361
    91
            elem match {
wenzelm@38361
    92
              case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
wenzelm@38361
    93
                atts match {
wenzelm@38479
    94
                  case Position.Range(range) =>
wenzelm@38361
    95
                    if (kind == Markup.ML_TYPING) {
wenzelm@38361
    96
                      val info = Pretty.string_of(body, margin = 40)
wenzelm@38479
    97
                      state.add_markup(command.decode_range(range, Command.TypeInfo(info)))
wenzelm@38361
    98
                    }
wenzelm@38361
    99
                    else if (kind == Markup.ML_REF) {
wenzelm@38361
   100
                      body match {
wenzelm@38361
   101
                        case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
wenzelm@38362
   102
                          state.add_markup(
wenzelm@38479
   103
                            command.decode_range(range,
wenzelm@38362
   104
                              Command.RefInfo(
wenzelm@38362
   105
                                Position.get_file(props),
wenzelm@38362
   106
                                Position.get_line(props),
wenzelm@38362
   107
                                Position.get_id(props),
wenzelm@38362
   108
                                Position.get_offset(props))))
wenzelm@38361
   109
                        case _ => state
wenzelm@38361
   110
                      }
wenzelm@38361
   111
                    }
wenzelm@38361
   112
                    else {
wenzelm@38361
   113
                      state.add_markup(
wenzelm@38479
   114
                        command.decode_range(range,
wenzelm@38361
   115
                          Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
wenzelm@38361
   116
                    }
wenzelm@38361
   117
                  case _ => state
wenzelm@38361
   118
                }
wenzelm@38361
   119
              case _ => System.err.println("Ignored report message: " + elem); state
wenzelm@38361
   120
            })
wenzelm@38361
   121
        case _ => add_result(message)
wenzelm@38361
   122
      }
wenzelm@38361
   123
  }
wenzelm@38367
   124
wenzelm@38367
   125
wenzelm@38367
   126
  /* unparsed dummy commands */
wenzelm@38367
   127
wenzelm@38367
   128
  def unparsed(source: String) =
wenzelm@38367
   129
    new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
wenzelm@34318
   130
}
wenzelm@34318
   131
wenzelm@38361
   132
wenzelm@34697
   133
class Command(
wenzelm@38150
   134
    val id: Document.Command_ID,
wenzelm@38373
   135
    val span: List[Token])
wenzelm@34451
   136
{
wenzelm@34859
   137
  /* classification */
wenzelm@34500
   138
wenzelm@36012
   139
  def is_command: Boolean = !span.isEmpty && span.head.is_command
wenzelm@34865
   140
  def is_ignored: Boolean = span.forall(_.is_ignored)
wenzelm@34859
   141
  def is_malformed: Boolean = !is_command && !is_ignored
wenzelm@34859
   142
wenzelm@38367
   143
  def is_unparsed = id == Document.NO_ID
wenzelm@38367
   144
wenzelm@36012
   145
  def name: String = if (is_command) span.head.content else ""
wenzelm@37129
   146
  override def toString =
wenzelm@37373
   147
    id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
wenzelm@34495
   148
wenzelm@34859
   149
wenzelm@34859
   150
  /* source text */
wenzelm@34451
   151
wenzelm@34859
   152
  val source: String = span.map(_.source).mkString
wenzelm@38426
   153
  def source(range: Text.Range): String = source.substring(range.start, range.stop)
wenzelm@34859
   154
  def length: Int = source.length
wenzelm@38479
   155
  val range: Text.Range = Text.Range(0, length)
wenzelm@34855
   156
wenzelm@34859
   157
  lazy val symbol_index = new Symbol.Index(source)
immler@34593
   158
wenzelm@34815
   159
immler@34676
   160
  /* markup */
wenzelm@34508
   161
wenzelm@38479
   162
  def decode_range(range: Text.Range, info: Any): Markup_Tree.Node =
wenzelm@38479
   163
    new Markup_Tree.Node(symbol_index.decode(range), info)
wenzelm@38370
   164
wenzelm@38370
   165
wenzelm@38370
   166
  /* accumulated results */
wenzelm@38370
   167
wenzelm@38479
   168
  val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
immler@34676
   169
}