src/Pure/PIDE/command.scala
author wenzelm
Wed May 05 22:23:45 2010 +0200 (2010-05-05 ago)
changeset 36676 ac7961d42ac3
parent 36012 src/Pure/Thy/command.scala@0614676f14d4
child 36990 449628c148cf
permissions -rw-r--r--
some rearrangement of Scala sources;
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@34637
    16
object Command
wenzelm@34637
    17
{
wenzelm@34637
    18
  object Status extends Enumeration
wenzelm@34637
    19
  {
wenzelm@34318
    20
    val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318
    21
    val FINISHED = Value("FINISHED")
wenzelm@34318
    22
    val FAILED = Value("FAILED")
wenzelm@34318
    23
  }
wenzelm@34707
    24
wenzelm@34707
    25
  case class HighlightInfo(highlight: String) { override def toString = highlight }
wenzelm@34717
    26
  case class TypeInfo(ty: String)
wenzelm@34707
    27
  case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@34717
    28
    command_id: Option[String], offset: Option[Int])
wenzelm@34318
    29
}
wenzelm@34318
    30
wenzelm@34451
    31
wenzelm@34697
    32
class Command(
wenzelm@34813
    33
    val id: Isar_Document.Command_ID,
wenzelm@34859
    34
    val span: Thy_Syntax.Span)
wenzelm@34815
    35
  extends Session.Entity
wenzelm@34451
    36
{
wenzelm@34859
    37
  /* classification */
wenzelm@34500
    38
wenzelm@36012
    39
  def is_command: Boolean = !span.isEmpty && span.head.is_command
wenzelm@34865
    40
  def is_ignored: Boolean = span.forall(_.is_ignored)
wenzelm@34859
    41
  def is_malformed: Boolean = !is_command && !is_ignored
wenzelm@34859
    42
wenzelm@36012
    43
  def name: String = if (is_command) span.head.content else ""
wenzelm@34859
    44
  override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
wenzelm@34495
    45
wenzelm@34859
    46
wenzelm@34859
    47
  /* source text */
wenzelm@34451
    48
wenzelm@34859
    49
  val source: String = span.map(_.source).mkString
wenzelm@34859
    50
  def source(i: Int, j: Int): String = source.substring(i, j)
wenzelm@34859
    51
  def length: Int = source.length
wenzelm@34855
    52
wenzelm@34859
    53
  lazy val symbol_index = new Symbol.Index(source)
immler@34593
    54
wenzelm@34815
    55
wenzelm@34815
    56
  /* accumulated messages */
wenzelm@34815
    57
wenzelm@34815
    58
  @volatile protected var state = new State(this)
wenzelm@34815
    59
  def current_state: State = state
wenzelm@34815
    60
wenzelm@34815
    61
  private case class Consume(session: Session, message: XML.Tree)
wenzelm@34832
    62
  private case object Assign
wenzelm@34815
    63
wenzelm@34815
    64
  private val accumulator = actor {
wenzelm@34832
    65
    var assigned = false
wenzelm@34815
    66
    loop {
wenzelm@34815
    67
      react {
wenzelm@34832
    68
        case Consume(session: Session, message: XML.Tree) if !assigned =>
wenzelm@34815
    69
          state = state.+(session, message)
wenzelm@34815
    70
wenzelm@34832
    71
        case Assign =>
wenzelm@34835
    72
          assigned = true  // single assignment
wenzelm@34832
    73
          reply(())
wenzelm@34815
    74
wenzelm@34815
    75
        case bad => System.err.println("command accumulator: ignoring bad message " + bad)
wenzelm@34815
    76
      }
wenzelm@34815
    77
    }
wenzelm@34815
    78
  }
wenzelm@34815
    79
wenzelm@34815
    80
  def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
wenzelm@34815
    81
wenzelm@34832
    82
  def assign_state(state_id: Isar_Document.State_ID): Command =
wenzelm@34815
    83
  {
wenzelm@34859
    84
    val cmd = new Command(state_id, span)
wenzelm@34832
    85
    accumulator !? Assign
wenzelm@34815
    86
    cmd.state = current_state
wenzelm@34815
    87
    cmd
wenzelm@34815
    88
  }
immler@34676
    89
immler@34676
    90
immler@34676
    91
  /* markup */
wenzelm@34508
    92
wenzelm@34859
    93
  lazy val empty_markup = new Markup_Text(Nil, source)
immler@34676
    94
wenzelm@34717
    95
  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
wenzelm@34699
    96
  {
wenzelm@34703
    97
    val start = symbol_index.decode(begin)
wenzelm@34703
    98
    val stop = symbol_index.decode(end)
wenzelm@34717
    99
    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
wenzelm@34500
   100
  }
immler@34676
   101
}