src/Pure/PIDE/command.scala
author wenzelm
Thu Aug 05 14:35:35 2010 +0200 (2010-08-05 ago)
changeset 38150 67fc24df3721
parent 37373 25078ba44436
child 38220 b30aa2dbedca
permissions -rw-r--r--
simplified/refined document model: collection of named nodes, without proper dependencies yet;
moved basic type definitions for ids and edits from Isar_Document to Document;
removed begin_document/end_document for now -- nodes emerge via edits;
edits refer to named nodes explicitly;
wenzelm@36676
     1
/*  Title:      Pure/PIDE/command.scala
wenzelm@36676
     2
    Author:     Johannes Hölzl, TU Munich
wenzelm@36676
     3
    Author:     Fabian Immler, TU Munich
wenzelm@36676
     4
    Author:     Makarius
wenzelm@36676
     5
wenzelm@36676
     6
Prover commands with semantic state.
wenzelm@36676
     7
*/
wenzelm@34407
     8
wenzelm@34871
     9
package isabelle
wenzelm@34318
    10
wenzelm@34451
    11
wenzelm@34699
    12
import scala.actors.Actor, Actor._
wenzelm@34497
    13
import scala.collection.mutable
wenzelm@34486
    14
wenzelm@34451
    15
wenzelm@37129
    16
case class Command_Set(set: Set[Command])
wenzelm@37129
    17
wenzelm@37129
    18
wenzelm@34637
    19
object Command
wenzelm@34637
    20
{
wenzelm@34637
    21
  object Status extends Enumeration
wenzelm@34637
    22
  {
wenzelm@34318
    23
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    24
    val FINISHED = Value("FINISHED")
wenzelm@34318
    25
    val FAILED = Value("FAILED")
wenzelm@36990
    26
    val UNDEFINED = Value("UNDEFINED")
wenzelm@34318
    27
  }
wenzelm@34707
    28
wenzelm@37197
    29
  case class HighlightInfo(kind: String, sub_kind: Option[String]) {
wenzelm@37197
    30
    override def toString = kind
wenzelm@37197
    31
  }
wenzelm@34717
    32
  case class TypeInfo(ty: String)
wenzelm@34707
    33
  case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@34717
    34
    command_id: Option[String], offset: Option[Int])
wenzelm@34318
    35
}
wenzelm@34318
    36
wenzelm@34697
    37
class Command(
wenzelm@38150
    38
    val id: Document.Command_ID,
wenzelm@37129
    39
    val span: Thy_Syntax.Span,
wenzelm@37129
    40
    val static_parent: Option[Command] = None)
wenzelm@34815
    41
  extends Session.Entity
wenzelm@34451
    42
{
wenzelm@34859
    43
  /* classification */
wenzelm@34500
    44
wenzelm@36012
    45
  def is_command: Boolean = !span.isEmpty && span.head.is_command
wenzelm@34865
    46
  def is_ignored: Boolean = span.forall(_.is_ignored)
wenzelm@34859
    47
  def is_malformed: Boolean = !is_command && !is_ignored
wenzelm@34859
    48
wenzelm@36012
    49
  def name: String = if (is_command) span.head.content else ""
wenzelm@37129
    50
  override def toString =
wenzelm@37373
    51
    id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
wenzelm@34495
    52
wenzelm@34859
    53
wenzelm@34859
    54
  /* source text */
wenzelm@34451
    55
wenzelm@34859
    56
  val source: String = span.map(_.source).mkString
wenzelm@34859
    57
  def source(i: Int, j: Int): String = source.substring(i, j)
wenzelm@34859
    58
  def length: Int = source.length
wenzelm@34855
    59
wenzelm@34859
    60
  lazy val symbol_index = new Symbol.Index(source)
immler@34593
    61
wenzelm@34815
    62
wenzelm@34815
    63
  /* accumulated messages */
wenzelm@34815
    64
wenzelm@34815
    65
  @volatile protected var state = new State(this)
wenzelm@34815
    66
  def current_state: State = state
wenzelm@34815
    67
wenzelm@37129
    68
  private case class Consume(message: XML.Tree, forward: Command => Unit)
wenzelm@34832
    69
  private case object Assign
wenzelm@34815
    70
wenzelm@34815
    71
  private val accumulator = actor {
wenzelm@34832
    72
    var assigned = false
wenzelm@34815
    73
    loop {
wenzelm@34815
    74
      react {
wenzelm@37129
    75
        case Consume(message, forward) if !assigned =>
wenzelm@37129
    76
          val old_state = state
wenzelm@37178
    77
          state = old_state.accumulate(message)
wenzelm@37129
    78
          if (!(state eq old_state)) forward(static_parent getOrElse this)
wenzelm@34815
    79
wenzelm@34832
    80
        case Assign =>
wenzelm@34835
    81
          assigned = true  // single assignment
wenzelm@34832
    82
          reply(())
wenzelm@34815
    83
wenzelm@37189
    84
        case bad => System.err.println("Command accumulator: ignoring bad message " + bad)
wenzelm@34815
    85
      }
wenzelm@34815
    86
    }
wenzelm@34815
    87
  }
wenzelm@34815
    88
wenzelm@37129
    89
  def consume(message: XML.Tree, forward: Command => Unit)
wenzelm@37129
    90
  {
wenzelm@37129
    91
    accumulator ! Consume(message, forward)
wenzelm@37129
    92
  }
wenzelm@34815
    93
wenzelm@38150
    94
  def assign_state(state_id: Document.State_ID): Command =
wenzelm@34815
    95
  {
wenzelm@37129
    96
    val cmd = new Command(state_id, span, Some(this))
wenzelm@34832
    97
    accumulator !? Assign
wenzelm@34815
    98
    cmd.state = current_state
wenzelm@34815
    99
    cmd
wenzelm@34815
   100
  }
immler@34676
   101
immler@34676
   102
immler@34676
   103
  /* markup */
wenzelm@34508
   104
wenzelm@34859
   105
  lazy val empty_markup = new Markup_Text(Nil, source)
immler@34676
   106
wenzelm@34717
   107
  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
wenzelm@34699
   108
  {
wenzelm@34703
   109
    val start = symbol_index.decode(begin)
wenzelm@34703
   110
    val stop = symbol_index.decode(end)
wenzelm@34717
   111
    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
wenzelm@34500
   112
  }
immler@34676
   113
}