src/Pure/PIDE/command.scala
author wenzelm
Tue Mar 13 21:17:37 2012 +0100 (2012-03-13)
changeset 46910 3e068ef04b42
parent 46813 bb7280848c99
child 47012 0e246130486b
permissions -rw-r--r--
clarified command state -- markup within proper_range, excluding trailing whitespace;
     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 apply(node_name: Document.Node.Name, toks: List[Token]): Command =
    96     Command(Document.no_id, node_name, toks)
    97 
    98   def unparsed(source: String): Command =
    99     Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
   100 
   101 
   102   /* perspective */
   103 
   104   object Perspective
   105   {
   106     val empty: Perspective = Perspective(Nil)
   107   }
   108 
   109   sealed case class Perspective(commands: List[Command])  // visible commands in canonical order
   110   {
   111     def same(that: Perspective): Boolean =
   112     {
   113       val cmds1 = this.commands
   114       val cmds2 = that.commands
   115       require(cmds1.forall(_.is_defined))
   116       require(cmds2.forall(_.is_defined))
   117       cmds1.length == cmds2.length &&
   118         (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
   119     }
   120   }
   121 }
   122 
   123 
   124 final class Command private(
   125     val id: Document.Command_ID,
   126     val node_name: Document.Node.Name,
   127     val span: List[Token],
   128     val source: String)
   129 {
   130   /* classification */
   131 
   132   def is_defined: Boolean = id != Document.no_id
   133 
   134   def is_command: Boolean = !span.isEmpty && span.head.is_command
   135   def is_ignored: Boolean = span.forall(_.is_ignored)
   136   def is_malformed: Boolean = !is_command && !is_ignored
   137 
   138   def name: String = if (is_command) span.head.content else ""
   139   override def toString =
   140     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
   141 
   142 
   143   /* source text */
   144 
   145   def length: Int = source.length
   146   val range: Text.Range = Text.Range(0, length)
   147 
   148   val proper_range: Text.Range =
   149     Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
   150 
   151   def source(range: Text.Range): String = source.substring(range.start, range.stop)
   152 
   153   val newlines =
   154     (0 /: Symbol.iterator(source)) {
   155       case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
   156 
   157   lazy val symbol_index = new Symbol.Index(source)
   158   def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
   159   def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
   160 
   161 
   162   /* accumulated results */
   163 
   164   val empty_state: Command.State = Command.State(this)
   165 }