src/Pure/PIDE/command.scala
author wenzelm
Wed Aug 18 11:25:09 2010 +0200 (2010-08-18)
changeset 38476 d72479a07882
parent 38429 9951852fae91
child 38479 e628da370072
permissions -rw-r--r--
decode Isabelle symbol positions in one spot;
     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   case class HighlightInfo(kind: String, sub_kind: Option[String]) {
    18     override def toString = kind
    19   }
    20   case class TypeInfo(ty: String)
    21   case class RefInfo(file: Option[String], line: Option[Int],
    22     command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
    23 
    24 
    25 
    26   /** accumulated results from prover **/
    27 
    28   case class State(
    29     val command: Command,
    30     val status: List[Markup],
    31     val reverse_results: List[XML.Tree],
    32     val markup: Markup_Text)
    33   {
    34     /* content */
    35 
    36     lazy val results = reverse_results.reverse
    37 
    38     def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
    39 
    40     def add_markup(node: Markup_Tree): State = copy(markup = markup + node)
    41 
    42 
    43     /* markup */
    44 
    45     lazy val highlight: Markup_Text =
    46     {
    47       markup.filter(_.info match {
    48         case Command.HighlightInfo(_, _) => true
    49         case _ => false
    50       })
    51     }
    52 
    53     private lazy val types: List[Markup_Node] =
    54       markup.filter(_.info match {
    55         case Command.TypeInfo(_) => true
    56         case _ => false }).flatten
    57 
    58     def type_at(pos: Text.Offset): Option[String] =
    59     {
    60       types.find(_.range.contains(pos)) match {
    61         case Some(t) =>
    62           t.info match {
    63             case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
    64             case _ => None
    65           }
    66         case None => None
    67       }
    68     }
    69 
    70     private lazy val refs: List[Markup_Node] =
    71       markup.filter(_.info match {
    72         case Command.RefInfo(_, _, _, _) => true
    73         case _ => false }).flatten
    74 
    75     def ref_at(pos: Text.Offset): Option[Markup_Node] =
    76       refs.find(_.range.contains(pos))
    77 
    78 
    79     /* message dispatch */
    80 
    81     def accumulate(message: XML.Tree): Command.State =
    82       message match {
    83         case XML.Elem(Markup(Markup.STATUS, _), elems) =>
    84           copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status)
    85 
    86         case XML.Elem(Markup(Markup.REPORT, _), elems) =>
    87           (this /: elems)((state, elem) =>
    88             elem match {
    89               case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
    90                 atts match {
    91                   case Position.Range(begin, end) =>
    92                     if (kind == Markup.ML_TYPING) {
    93                       val info = Pretty.string_of(body, margin = 40)
    94                       state.add_markup(
    95                         command.markup_node(begin, end, Command.TypeInfo(info)))
    96                     }
    97                     else if (kind == Markup.ML_REF) {
    98                       body match {
    99                         case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
   100                           state.add_markup(
   101                             command.markup_node(
   102                               begin, end,
   103                               Command.RefInfo(
   104                                 Position.get_file(props),
   105                                 Position.get_line(props),
   106                                 Position.get_id(props),
   107                                 Position.get_offset(props))))
   108                         case _ => state
   109                       }
   110                     }
   111                     else {
   112                       state.add_markup(
   113                         command.markup_node(begin, end,
   114                           Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
   115                     }
   116                   case _ => state
   117                 }
   118               case _ => System.err.println("Ignored report message: " + elem); state
   119             })
   120         case _ => add_result(message)
   121       }
   122   }
   123 
   124 
   125   /* unparsed dummy commands */
   126 
   127   def unparsed(source: String) =
   128     new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
   129 }
   130 
   131 
   132 class Command(
   133     val id: Document.Command_ID,
   134     val span: List[Token])
   135 {
   136   /* classification */
   137 
   138   def is_command: Boolean = !span.isEmpty && span.head.is_command
   139   def is_ignored: Boolean = span.forall(_.is_ignored)
   140   def is_malformed: Boolean = !is_command && !is_ignored
   141 
   142   def is_unparsed = id == Document.NO_ID
   143 
   144   def name: String = if (is_command) span.head.content else ""
   145   override def toString =
   146     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
   147 
   148 
   149   /* source text */
   150 
   151   val source: String = span.map(_.source).mkString
   152   def source(range: Text.Range): String = source.substring(range.start, range.stop)
   153   def length: Int = source.length
   154 
   155   lazy val symbol_index = new Symbol.Index(source)
   156 
   157 
   158   /* markup */
   159 
   160   def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
   161   {
   162     val start = symbol_index.decode(begin - 1)
   163     val stop = symbol_index.decode(end - 1)
   164     new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
   165   }
   166 
   167 
   168   /* accumulated results */
   169 
   170   val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source))
   171 }