src/Pure/PIDE/command.scala
author wenzelm
Mon Mar 19 14:59:31 2012 +0100 (2012-03-19)
changeset 47012 0e246130486b
parent 46910 3e068ef04b42
child 47459 373e456149cc
permissions -rw-r--r--
clarified command span classification: strict Command.is_command, permissive Command.name;
     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 import java.lang.System
    11 
    12 import scala.collection.mutable
    13 import scala.collection.immutable.SortedMap
    14 
    15 
    16 object Command
    17 {
    18   /** accumulated results from prover **/
    19 
    20   sealed case class State(
    21     val command: Command,
    22     val status: List[Markup] = Nil,
    23     val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
    24     val markup: Markup_Tree = Markup_Tree.empty)
    25   {
    26     /* accumulate content */
    27 
    28     private def add_status(st: Markup): State = copy(status = st :: status)
    29     private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
    30 
    31     def + (message: XML.Elem): Command.State =
    32       message match {
    33         case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
    34           (this /: msgs)((state, msg) =>
    35             msg match {
    36               case elem @ XML.Elem(markup, Nil) =>
    37                 state.add_status(markup).add_markup(Text.Info(command.proper_range, elem))
    38 
    39               case _ => System.err.println("Ignored status message: " + msg); state
    40             })
    41 
    42         case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) =>
    43           (this /: msgs)((state, msg) =>
    44             msg match {
    45               case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
    46               if id == command.id && command.range.contains(command.decode(raw_range)) =>
    47                 val range = command.decode(raw_range)
    48                 val props = Position.purge(atts)
    49                 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    50                 state.add_markup(info)
    51               case _ =>
    52                 // FIXME System.err.println("Ignored report message: " + msg)
    53                 state
    54             })
    55         case XML.Elem(Markup(name, atts), body) =>
    56           atts match {
    57             case Isabelle_Markup.Serial(i) =>
    58               val result = XML.Elem(Markup(name, Position.purge(atts)), body)
    59               val st0 = copy(results = results + (i -> result))
    60               val st1 =
    61                 if (Protocol.is_tracing(message)) st0
    62                 else
    63                   (st0 /: Protocol.message_positions(command, message))(
    64                     (st, range) => st.add_markup(Text.Info(range, result)))
    65               val st2 = (st1 /: Protocol.message_reports(message))(_ + _)
    66               st2
    67             case _ => System.err.println("Ignored message without serial number: " + message); this
    68           }
    69       }
    70   }
    71 
    72 
    73   /* make commands */
    74 
    75   def apply(id: Document.Command_ID, node_name: Document.Node.Name, toks: List[Token]): Command =
    76   {
    77     val source: String =
    78       toks match {
    79         case List(tok) => tok.source
    80         case _ => toks.map(_.source).mkString
    81       }
    82 
    83     val span = new mutable.ListBuffer[Token]
    84     var i = 0
    85     for (Token(kind, s) <- toks) {
    86       val n = s.length
    87       val s1 = source.substring(i, i + n)
    88       span += Token(kind, s1)
    89       i += n
    90     }
    91 
    92     new Command(id, node_name, span.toList, source)
    93   }
    94 
    95   def unparsed(source: String): Command =
    96     Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
    97 
    98 
    99   /* perspective */
   100 
   101   object Perspective
   102   {
   103     val empty: Perspective = Perspective(Nil)
   104   }
   105 
   106   sealed case class Perspective(commands: List[Command])  // visible commands in canonical order
   107   {
   108     def same(that: Perspective): Boolean =
   109     {
   110       val cmds1 = this.commands
   111       val cmds2 = that.commands
   112       require(cmds1.forall(_.is_defined))
   113       require(cmds2.forall(_.is_defined))
   114       cmds1.length == cmds2.length &&
   115         (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
   116     }
   117   }
   118 }
   119 
   120 
   121 final class Command private(
   122     val id: Document.Command_ID,
   123     val node_name: Document.Node.Name,
   124     val span: List[Token],
   125     val source: String)
   126 {
   127   /* classification */
   128 
   129   def is_defined: Boolean = id != Document.no_id
   130 
   131   val is_ignored: Boolean = span.forall(_.is_ignored)
   132   val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_unparsed))
   133   def is_command: Boolean = !is_ignored && !is_malformed
   134 
   135   def name: String =
   136     span.find(_.is_command) match { case Some(tok) => tok.content case _ => "" }
   137 
   138   override def toString =
   139     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
   140 
   141 
   142   /* source text */
   143 
   144   def length: Int = source.length
   145   val range: Text.Range = Text.Range(0, length)
   146 
   147   val proper_range: Text.Range =
   148     Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
   149 
   150   def source(range: Text.Range): String = source.substring(range.start, range.stop)
   151 
   152   val newlines =
   153     (0 /: Symbol.iterator(source)) {
   154       case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
   155 
   156   lazy val symbol_index = new Symbol.Index(source)
   157   def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
   158   def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
   159 
   160 
   161   /* accumulated results */
   162 
   163   val empty_state: Command.State = Command.State(this)
   164 }