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;
     1 /*  Title:      Pure/PIDE/command.scala
     2     Author:     Johannes Hölzl, TU Munich
     3     Author:     Fabian Immler, TU Munich
     4     Author:     Makarius
     5 
     6 Prover commands with semantic state.
     7 */
     8 
     9 package isabelle
    10 
    11 
    12 import scala.actors.Actor, Actor._
    13 import scala.collection.mutable
    14 
    15 
    16 object Command
    17 {
    18   object Status extends Enumeration
    19   {
    20     val UNPROCESSED = Value("UNPROCESSED")
    21     val FINISHED = Value("FINISHED")
    22     val FAILED = Value("FAILED")
    23   }
    24 
    25   case class HighlightInfo(highlight: String) { override def toString = highlight }
    26   case class TypeInfo(ty: String)
    27   case class RefInfo(file: Option[String], line: Option[Int],
    28     command_id: Option[String], offset: Option[Int])
    29 }
    30 
    31 
    32 class Command(
    33     val id: Isar_Document.Command_ID,
    34     val span: Thy_Syntax.Span)
    35   extends Session.Entity
    36 {
    37   /* classification */
    38 
    39   def is_command: Boolean = !span.isEmpty && span.head.is_command
    40   def is_ignored: Boolean = span.forall(_.is_ignored)
    41   def is_malformed: Boolean = !is_command && !is_ignored
    42 
    43   def name: String = if (is_command) span.head.content else ""
    44   override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
    45 
    46 
    47   /* source text */
    48 
    49   val source: String = span.map(_.source).mkString
    50   def source(i: Int, j: Int): String = source.substring(i, j)
    51   def length: Int = source.length
    52 
    53   lazy val symbol_index = new Symbol.Index(source)
    54 
    55 
    56   /* accumulated messages */
    57 
    58   @volatile protected var state = new State(this)
    59   def current_state: State = state
    60 
    61   private case class Consume(session: Session, message: XML.Tree)
    62   private case object Assign
    63 
    64   private val accumulator = actor {
    65     var assigned = false
    66     loop {
    67       react {
    68         case Consume(session: Session, message: XML.Tree) if !assigned =>
    69           state = state.+(session, message)
    70 
    71         case Assign =>
    72           assigned = true  // single assignment
    73           reply(())
    74 
    75         case bad => System.err.println("command accumulator: ignoring bad message " + bad)
    76       }
    77     }
    78   }
    79 
    80   def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
    81 
    82   def assign_state(state_id: Isar_Document.State_ID): Command =
    83   {
    84     val cmd = new Command(state_id, span)
    85     accumulator !? Assign
    86     cmd.state = current_state
    87     cmd
    88   }
    89 
    90 
    91   /* markup */
    92 
    93   lazy val empty_markup = new Markup_Text(Nil, source)
    94 
    95   def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
    96   {
    97     val start = symbol_index.decode(begin)
    98     val stop = symbol_index.decode(end)
    99     new Markup_Tree(new Markup_Node(start, stop, info), Nil)
   100   }
   101 }