src/Pure/PIDE/command.scala
author wenzelm
Thu Aug 12 13:59:18 2010 +0200 (2010-08-12)
changeset 38361 b609d0b271fa
parent 38360 53224a4d2f0e
child 38362 754ad6340055
permissions -rw-r--r--
specific command state;
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@34637
    17
  object Status extends Enumeration
wenzelm@34637
    18
  {
wenzelm@34318
    19
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    20
    val FINISHED = Value("FINISHED")
wenzelm@34318
    21
    val FAILED = Value("FAILED")
wenzelm@36990
    22
    val UNDEFINED = Value("UNDEFINED")
wenzelm@34318
    23
  }
wenzelm@34707
    24
wenzelm@37197
    25
  case class HighlightInfo(kind: String, sub_kind: Option[String]) {
wenzelm@37197
    26
    override def toString = kind
wenzelm@37197
    27
  }
wenzelm@34717
    28
  case class TypeInfo(ty: String)
wenzelm@34707
    29
  case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@38355
    30
    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
wenzelm@38361
    31
wenzelm@38361
    32
wenzelm@38361
    33
  /** accumulated results from prover **/
wenzelm@38361
    34
wenzelm@38361
    35
  class State(
wenzelm@38361
    36
    val command: Command,
wenzelm@38361
    37
    val status: Command.Status.Value,
wenzelm@38361
    38
    val forks: Int,
wenzelm@38361
    39
    val reverse_results: List[XML.Tree],
wenzelm@38361
    40
    val markup_root: Markup_Text)
wenzelm@38361
    41
  {
wenzelm@38361
    42
    def this(command: Command) =
wenzelm@38361
    43
      this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
wenzelm@38361
    44
wenzelm@38361
    45
wenzelm@38361
    46
    /* content */
wenzelm@38361
    47
wenzelm@38361
    48
    private def set_status(st: Command.Status.Value): State =
wenzelm@38361
    49
      new State(command, st, forks, reverse_results, markup_root)
wenzelm@38361
    50
wenzelm@38361
    51
    private def add_forks(i: Int): State =
wenzelm@38361
    52
      new State(command, status, forks + i, reverse_results, markup_root)
wenzelm@38361
    53
wenzelm@38361
    54
    private def add_result(res: XML.Tree): State =
wenzelm@38361
    55
      new State(command, status, forks, res :: reverse_results, markup_root)
wenzelm@38361
    56
wenzelm@38361
    57
    private def add_markup(node: Markup_Tree): State =
wenzelm@38361
    58
      new State(command, status, forks, reverse_results, markup_root + node)
wenzelm@38361
    59
wenzelm@38361
    60
    lazy val results = reverse_results.reverse
wenzelm@38361
    61
wenzelm@38361
    62
wenzelm@38361
    63
    /* markup */
wenzelm@38361
    64
wenzelm@38361
    65
    lazy val highlight: Markup_Text =
wenzelm@38361
    66
    {
wenzelm@38361
    67
      markup_root.filter(_.info match {
wenzelm@38361
    68
        case Command.HighlightInfo(_, _) => true
wenzelm@38361
    69
        case _ => false
wenzelm@38361
    70
      })
wenzelm@38361
    71
    }
wenzelm@38361
    72
wenzelm@38361
    73
    private lazy val types: List[Markup_Node] =
wenzelm@38361
    74
      markup_root.filter(_.info match {
wenzelm@38361
    75
        case Command.TypeInfo(_) => true
wenzelm@38361
    76
        case _ => false }).flatten
wenzelm@38361
    77
wenzelm@38361
    78
    def type_at(pos: Int): Option[String] =
wenzelm@38361
    79
    {
wenzelm@38361
    80
      types.find(t => t.start <= pos && pos < t.stop) match {
wenzelm@38361
    81
        case Some(t) =>
wenzelm@38361
    82
          t.info match {
wenzelm@38361
    83
            case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
wenzelm@38361
    84
            case _ => None
wenzelm@38361
    85
          }
wenzelm@38361
    86
        case None => None
wenzelm@38361
    87
      }
wenzelm@38361
    88
    }
wenzelm@38361
    89
wenzelm@38361
    90
    private lazy val refs: List[Markup_Node] =
wenzelm@38361
    91
      markup_root.filter(_.info match {
wenzelm@38361
    92
        case Command.RefInfo(_, _, _, _) => true
wenzelm@38361
    93
        case _ => false }).flatten
wenzelm@38361
    94
wenzelm@38361
    95
    def ref_at(pos: Int): Option[Markup_Node] =
wenzelm@38361
    96
      refs.find(t => t.start <= pos && pos < t.stop)
wenzelm@38361
    97
wenzelm@38361
    98
wenzelm@38361
    99
    /* message dispatch */
wenzelm@38361
   100
wenzelm@38361
   101
    def accumulate(message: XML.Tree): Command.State =
wenzelm@38361
   102
      message match {
wenzelm@38361
   103
        case XML.Elem(Markup(Markup.STATUS, _), elems) =>
wenzelm@38361
   104
          (this /: elems)((state, elem) =>
wenzelm@38361
   105
            elem match {
wenzelm@38361
   106
              case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
wenzelm@38361
   107
              case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
wenzelm@38361
   108
              case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
wenzelm@38361
   109
              case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
wenzelm@38361
   110
              case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
wenzelm@38361
   111
              case _ => System.err.println("Ignored status message: " + elem); state
wenzelm@38361
   112
            })
wenzelm@38361
   113
wenzelm@38361
   114
        case XML.Elem(Markup(Markup.REPORT, _), elems) =>
wenzelm@38361
   115
          (this /: elems)((state, elem) =>
wenzelm@38361
   116
            elem match {
wenzelm@38361
   117
              case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
wenzelm@38361
   118
                atts match {
wenzelm@38361
   119
                  case Position.Range(begin, end) =>
wenzelm@38361
   120
                    if (kind == Markup.ML_TYPING) {
wenzelm@38361
   121
                      val info = Pretty.string_of(body, margin = 40)
wenzelm@38361
   122
                      state.add_markup(
wenzelm@38361
   123
                        command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
wenzelm@38361
   124
                    }
wenzelm@38361
   125
                    else if (kind == Markup.ML_REF) {
wenzelm@38361
   126
                      body match {
wenzelm@38361
   127
                        case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
wenzelm@38361
   128
                          state.add_markup(command.markup_node(
wenzelm@38361
   129
                            begin - 1, end - 1,
wenzelm@38361
   130
                            Command.RefInfo(
wenzelm@38361
   131
                              Position.get_file(props),
wenzelm@38361
   132
                              Position.get_line(props),
wenzelm@38361
   133
                              Position.get_id(props),
wenzelm@38361
   134
                              Position.get_offset(props))))
wenzelm@38361
   135
                        case _ => state
wenzelm@38361
   136
                      }
wenzelm@38361
   137
                    }
wenzelm@38361
   138
                    else {
wenzelm@38361
   139
                      state.add_markup(
wenzelm@38361
   140
                        command.markup_node(begin - 1, end - 1,
wenzelm@38361
   141
                          Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
wenzelm@38361
   142
                    }
wenzelm@38361
   143
                  case _ => state
wenzelm@38361
   144
                }
wenzelm@38361
   145
              case _ => System.err.println("Ignored report message: " + elem); state
wenzelm@38361
   146
            })
wenzelm@38361
   147
        case _ => add_result(message)
wenzelm@38361
   148
      }
wenzelm@38361
   149
  }
wenzelm@34318
   150
}
wenzelm@34318
   151
wenzelm@38361
   152
wenzelm@34697
   153
class Command(
wenzelm@38150
   154
    val id: Document.Command_ID,
wenzelm@37129
   155
    val span: Thy_Syntax.Span,
wenzelm@38220
   156
    val static_parent: Option[Command] = None)  // FIXME !?
wenzelm@34815
   157
  extends Session.Entity
wenzelm@34451
   158
{
wenzelm@34859
   159
  /* classification */
wenzelm@34500
   160
wenzelm@36012
   161
  def is_command: Boolean = !span.isEmpty && span.head.is_command
wenzelm@34865
   162
  def is_ignored: Boolean = span.forall(_.is_ignored)
wenzelm@34859
   163
  def is_malformed: Boolean = !is_command && !is_ignored
wenzelm@34859
   164
wenzelm@36012
   165
  def name: String = if (is_command) span.head.content else ""
wenzelm@37129
   166
  override def toString =
wenzelm@37373
   167
    id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
wenzelm@34495
   168
wenzelm@34859
   169
wenzelm@34859
   170
  /* source text */
wenzelm@34451
   171
wenzelm@34859
   172
  val source: String = span.map(_.source).mkString
wenzelm@34859
   173
  def source(i: Int, j: Int): String = source.substring(i, j)
wenzelm@34859
   174
  def length: Int = source.length
wenzelm@34855
   175
wenzelm@34859
   176
  lazy val symbol_index = new Symbol.Index(source)
immler@34593
   177
wenzelm@34815
   178
wenzelm@34815
   179
  /* accumulated messages */
wenzelm@34815
   180
wenzelm@38361
   181
  @volatile protected var state = new Command.State(this)
wenzelm@38361
   182
  def current_state: Command.State = state
wenzelm@34815
   183
wenzelm@37129
   184
  private case class Consume(message: XML.Tree, forward: Command => Unit)
wenzelm@34832
   185
  private case object Assign
wenzelm@34815
   186
wenzelm@34815
   187
  private val accumulator = actor {
wenzelm@34832
   188
    var assigned = false
wenzelm@34815
   189
    loop {
wenzelm@34815
   190
      react {
wenzelm@37129
   191
        case Consume(message, forward) if !assigned =>
wenzelm@37129
   192
          val old_state = state
wenzelm@37178
   193
          state = old_state.accumulate(message)
wenzelm@37129
   194
          if (!(state eq old_state)) forward(static_parent getOrElse this)
wenzelm@34815
   195
wenzelm@34832
   196
        case Assign =>
wenzelm@34835
   197
          assigned = true  // single assignment
wenzelm@34832
   198
          reply(())
wenzelm@34815
   199
wenzelm@37189
   200
        case bad => System.err.println("Command accumulator: ignoring bad message " + bad)
wenzelm@34815
   201
      }
wenzelm@34815
   202
    }
wenzelm@34815
   203
  }
wenzelm@34815
   204
wenzelm@37129
   205
  def consume(message: XML.Tree, forward: Command => Unit)
wenzelm@37129
   206
  {
wenzelm@37129
   207
    accumulator ! Consume(message, forward)
wenzelm@37129
   208
  }
wenzelm@34815
   209
wenzelm@38150
   210
  def assign_state(state_id: Document.State_ID): Command =
wenzelm@34815
   211
  {
wenzelm@37129
   212
    val cmd = new Command(state_id, span, Some(this))
wenzelm@34832
   213
    accumulator !? Assign
wenzelm@34815
   214
    cmd.state = current_state
wenzelm@34815
   215
    cmd
wenzelm@34815
   216
  }
immler@34676
   217
immler@34676
   218
immler@34676
   219
  /* markup */
wenzelm@34508
   220
wenzelm@34859
   221
  lazy val empty_markup = new Markup_Text(Nil, source)
immler@34676
   222
wenzelm@34717
   223
  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
wenzelm@34699
   224
  {
wenzelm@34703
   225
    val start = symbol_index.decode(begin)
wenzelm@34703
   226
    val stop = symbol_index.decode(end)
wenzelm@34717
   227
    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
wenzelm@34500
   228
  }
immler@34676
   229
}