src/Pure/PIDE/command.scala
author wenzelm
Thu Aug 05 14:35:35 2010 +0200 (2010-08-05)
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;
     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 case class Command_Set(set: Set[Command])
    17 
    18 
    19 object Command
    20 {
    21   object Status extends Enumeration
    22   {
    23     val UNPROCESSED = Value("UNPROCESSED")
    24     val FINISHED = Value("FINISHED")
    25     val FAILED = Value("FAILED")
    26     val UNDEFINED = Value("UNDEFINED")
    27   }
    28 
    29   case class HighlightInfo(kind: String, sub_kind: Option[String]) {
    30     override def toString = kind
    31   }
    32   case class TypeInfo(ty: String)
    33   case class RefInfo(file: Option[String], line: Option[Int],
    34     command_id: Option[String], offset: Option[Int])
    35 }
    36 
    37 class Command(
    38     val id: Document.Command_ID,
    39     val span: Thy_Syntax.Span,
    40     val static_parent: Option[Command] = None)
    41   extends Session.Entity
    42 {
    43   /* classification */
    44 
    45   def is_command: Boolean = !span.isEmpty && span.head.is_command
    46   def is_ignored: Boolean = span.forall(_.is_ignored)
    47   def is_malformed: Boolean = !is_command && !is_ignored
    48 
    49   def name: String = if (is_command) span.head.content else ""
    50   override def toString =
    51     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
    52 
    53 
    54   /* source text */
    55 
    56   val source: String = span.map(_.source).mkString
    57   def source(i: Int, j: Int): String = source.substring(i, j)
    58   def length: Int = source.length
    59 
    60   lazy val symbol_index = new Symbol.Index(source)
    61 
    62 
    63   /* accumulated messages */
    64 
    65   @volatile protected var state = new State(this)
    66   def current_state: State = state
    67 
    68   private case class Consume(message: XML.Tree, forward: Command => Unit)
    69   private case object Assign
    70 
    71   private val accumulator = actor {
    72     var assigned = false
    73     loop {
    74       react {
    75         case Consume(message, forward) if !assigned =>
    76           val old_state = state
    77           state = old_state.accumulate(message)
    78           if (!(state eq old_state)) forward(static_parent getOrElse this)
    79 
    80         case Assign =>
    81           assigned = true  // single assignment
    82           reply(())
    83 
    84         case bad => System.err.println("Command accumulator: ignoring bad message " + bad)
    85       }
    86     }
    87   }
    88 
    89   def consume(message: XML.Tree, forward: Command => Unit)
    90   {
    91     accumulator ! Consume(message, forward)
    92   }
    93 
    94   def assign_state(state_id: Document.State_ID): Command =
    95   {
    96     val cmd = new Command(state_id, span, Some(this))
    97     accumulator !? Assign
    98     cmd.state = current_state
    99     cmd
   100   }
   101 
   102 
   103   /* markup */
   104 
   105   lazy val empty_markup = new Markup_Text(Nil, source)
   106 
   107   def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
   108   {
   109     val start = symbol_index.decode(begin)
   110     val stop = symbol_index.decode(end)
   111     new Markup_Tree(new Markup_Node(start, stop, info), Nil)
   112   }
   113 }