src/Pure/PIDE/command.scala
author wenzelm
Sat Jan 07 12:39:46 2012 +0100 (2012-01-07)
changeset 46152 793cecd4ffc0
parent 45709 87017fcbad83
child 46164 a01c969f2e14
permissions -rw-r--r--
accumulate status as regular markup for command range;
tuned signature;
     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                 val info: Text.Markup = Text.Info(command.range, elem)
    38                 state.add_status(markup).add_markup(info)
    39 
    40               case _ => System.err.println("Ignored status message: " + msg); state
    41             })
    42 
    43         case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) =>
    44           (this /: msgs)((state, msg) =>
    45             msg match {
    46               case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
    47               if id == command.id && command.range.contains(command.decode(raw_range)) =>
    48                 val range = command.decode(raw_range)
    49                 val props = Position.purge(atts)
    50                 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    51                 state.add_markup(info)
    52               case _ =>
    53                 // FIXME System.err.println("Ignored report message: " + msg)
    54                 state
    55             })
    56         case XML.Elem(Markup(name, atts), body) =>
    57           atts match {
    58             case Isabelle_Markup.Serial(i) =>
    59               val result = XML.Elem(Markup(name, Position.purge(atts)), body)
    60               val st0 = copy(results = results + (i -> result))
    61               val st1 =
    62                 if (Protocol.is_tracing(message)) st0
    63                 else
    64                   (st0 /: Protocol.message_positions(command, message))(
    65                     (st, range) => st.add_markup(Text.Info(range, result)))
    66               val st2 = (st1 /: Protocol.message_reports(message))(_ + _)
    67               st2
    68             case _ => System.err.println("Ignored message without serial number: " + message); this
    69           }
    70       }
    71   }
    72 
    73 
    74   /* make commands */
    75 
    76   def apply(id: Document.Command_ID, node_name: Document.Node.Name, toks: List[Token]): Command =
    77   {
    78     val source: String =
    79       toks match {
    80         case List(tok) => tok.source
    81         case _ => toks.map(_.source).mkString
    82       }
    83 
    84     val span = new mutable.ListBuffer[Token]
    85     var i = 0
    86     for (Token(kind, s) <- toks) {
    87       val n = s.length
    88       val s1 = source.substring(i, i + n)
    89       span += Token(kind, s1)
    90       i += n
    91     }
    92 
    93     new Command(id, node_name, span.toList, source)
    94   }
    95 
    96   def apply(node_name: Document.Node.Name, toks: List[Token]): Command =
    97     Command(Document.no_id, node_name, toks)
    98 
    99   def unparsed(source: String): Command =
   100     Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
   101 
   102 
   103   /* perspective */
   104 
   105   object Perspective
   106   {
   107     val empty: Perspective = Perspective(Nil)
   108   }
   109 
   110   sealed case class Perspective(commands: List[Command])  // visible commands in canonical order
   111   {
   112     def same(that: Perspective): Boolean =
   113     {
   114       val cmds1 = this.commands
   115       val cmds2 = that.commands
   116       require(cmds1.forall(_.is_defined))
   117       require(cmds2.forall(_.is_defined))
   118       cmds1.length == cmds2.length &&
   119         (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
   120     }
   121   }
   122 }
   123 
   124 
   125 class Command private(
   126     val id: Document.Command_ID,
   127     val node_name: Document.Node.Name,
   128     val span: List[Token],
   129     val source: String)
   130 {
   131   /* classification */
   132 
   133   def is_defined: Boolean = id != Document.no_id
   134 
   135   def is_command: Boolean = !span.isEmpty && span.head.is_command
   136   def is_ignored: Boolean = span.forall(_.is_ignored)
   137   def is_malformed: Boolean = !is_command && !is_ignored
   138 
   139   def name: String = if (is_command) span.head.content else ""
   140   override def toString =
   141     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
   142 
   143 
   144   /* source text */
   145 
   146   def source(range: Text.Range): String = source.substring(range.start, range.stop)
   147   def length: Int = source.length
   148 
   149   val newlines =
   150     (0 /: Symbol.iterator(source)) {
   151       case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
   152 
   153   val range: Text.Range = Text.Range(0, length)
   154 
   155   lazy val symbol_index = new Symbol.Index(source)
   156   def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
   157   def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
   158 
   159 
   160   /* accumulated results */
   161 
   162   val empty_state: Command.State = Command.State(this)
   163 }