src/Pure/PIDE/command.scala
author wenzelm
Sun Aug 15 22:48:56 2010 +0200 (2010-08-15)
changeset 38426 2858ec7b6dd8
parent 38415 f3220ef79d51
child 38427 7066fbd315ae
permissions -rw-r--r--
specific types Text.Offset and Text.Range;
minor tuning;
     1 /*  Title:      Pure/PIDE/command.scala
     2     Author:     Fabian Immler, TU Munich
     3     Author:     Makarius
     4 
     5 Prover commands with semantic state.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.actors.Actor, Actor._
    12 import scala.collection.mutable
    13 
    14 
    15 object Command
    16 {
    17   object Status extends Enumeration
    18   {
    19     val UNPROCESSED = Value("UNPROCESSED")
    20     val FINISHED = Value("FINISHED")
    21     val FAILED = Value("FAILED")
    22     val UNDEFINED = Value("UNDEFINED")
    23   }
    24 
    25   case class HighlightInfo(kind: String, sub_kind: Option[String]) {
    26     override def toString = kind
    27   }
    28   case class TypeInfo(ty: String)
    29   case class RefInfo(file: Option[String], line: Option[Int],
    30     command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
    31 
    32 
    33 
    34   /** accumulated results from prover **/
    35 
    36   case class State(
    37     val command: Command,
    38     val status: Command.Status.Value,
    39     val forks: Int,
    40     val reverse_results: List[XML.Tree],
    41     val markup: Markup_Text)
    42   {
    43     /* content */
    44 
    45     lazy val results = reverse_results.reverse
    46 
    47     def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
    48 
    49     def add_markup(node: Markup_Tree): State = copy(markup = markup + node)
    50 
    51 
    52     /* markup */
    53 
    54     lazy val highlight: Markup_Text =
    55     {
    56       markup.filter(_.info match {
    57         case Command.HighlightInfo(_, _) => true
    58         case _ => false
    59       })
    60     }
    61 
    62     private lazy val types: List[Markup_Node] =
    63       markup.filter(_.info match {
    64         case Command.TypeInfo(_) => true
    65         case _ => false }).flatten
    66 
    67     def type_at(pos: Text.Offset): Option[String] =
    68     {
    69       types.find(t => t.range.start <= pos && pos < t.range.stop) match {
    70         case Some(t) =>
    71           t.info match {
    72             case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
    73             case _ => None
    74           }
    75         case None => None
    76       }
    77     }
    78 
    79     private lazy val refs: List[Markup_Node] =
    80       markup.filter(_.info match {
    81         case Command.RefInfo(_, _, _, _) => true
    82         case _ => false }).flatten
    83 
    84     def ref_at(pos: Text.Offset): Option[Markup_Node] =
    85       refs.find(t => t.range.start <= pos && pos < t.range.stop)
    86 
    87 
    88     /* message dispatch */
    89 
    90     def accumulate(message: XML.Tree): Command.State =
    91       message match {
    92         case XML.Elem(Markup(Markup.STATUS, _), elems) =>
    93           (this /: elems)((state, elem) =>
    94             elem match {
    95               case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED)
    96               case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED)
    97               case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED)
    98               case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1)
    99               case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1)
   100               case _ => System.err.println("Ignored status message: " + elem); state
   101             })
   102 
   103         case XML.Elem(Markup(Markup.REPORT, _), elems) =>
   104           (this /: elems)((state, elem) =>
   105             elem match {
   106               case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
   107                 atts match {
   108                   case Position.Range(begin, end) =>
   109                     if (kind == Markup.ML_TYPING) {
   110                       val info = Pretty.string_of(body, margin = 40)
   111                       state.add_markup(
   112                         command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
   113                     }
   114                     else if (kind == Markup.ML_REF) {
   115                       body match {
   116                         case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
   117                           state.add_markup(
   118                             command.markup_node(
   119                               begin - 1, end - 1,
   120                               Command.RefInfo(
   121                                 Position.get_file(props),
   122                                 Position.get_line(props),
   123                                 Position.get_id(props),
   124                                 Position.get_offset(props))))
   125                         case _ => state
   126                       }
   127                     }
   128                     else {
   129                       state.add_markup(
   130                         command.markup_node(begin - 1, end - 1,
   131                           Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
   132                     }
   133                   case _ => state
   134                 }
   135               case _ => System.err.println("Ignored report message: " + elem); state
   136             })
   137         case _ => add_result(message)
   138       }
   139   }
   140 
   141 
   142   /* unparsed dummy commands */
   143 
   144   def unparsed(source: String) =
   145     new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
   146 }
   147 
   148 
   149 class Command(
   150     val id: Document.Command_ID,
   151     val span: List[Token])
   152 {
   153   /* classification */
   154 
   155   def is_command: Boolean = !span.isEmpty && span.head.is_command
   156   def is_ignored: Boolean = span.forall(_.is_ignored)
   157   def is_malformed: Boolean = !is_command && !is_ignored
   158 
   159   def is_unparsed = id == Document.NO_ID
   160 
   161   def name: String = if (is_command) span.head.content else ""
   162   override def toString =
   163     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
   164 
   165 
   166   /* source text */
   167 
   168   val source: String = span.map(_.source).mkString
   169   def source(range: Text.Range): String = source.substring(range.start, range.stop)
   170   def length: Int = source.length
   171 
   172   lazy val symbol_index = new Symbol.Index(source)
   173 
   174 
   175   /* markup */
   176 
   177   def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
   178   {
   179     val start = symbol_index.decode(begin)
   180     val stop = symbol_index.decode(end)
   181     new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
   182   }
   183 
   184 
   185   /* accumulated results */
   186 
   187   val empty_state: Command.State =
   188     Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source))
   189 }