src/Pure/PIDE/isar_document.scala
author wenzelm
Fri Sep 02 11:52:13 2011 +0200 (2011-09-02)
changeset 44644 317e4962dd0f
parent 44615 a4ff8a787202
child 44661 383c9d758a56
permissions -rw-r--r--
clarified define_command: store name as structural information;
     1 /*  Title:      Pure/PIDE/isar_document.scala
     2     Author:     Makarius
     3 
     4 Protocol message formats for interactive Isar documents.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Isar_Document
    11 {
    12   /* document editing */
    13 
    14   object Assign
    15   {
    16     def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] =
    17       msg match {
    18         case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
    19           try {
    20             import XML.Decode._
    21             val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body)
    22             Some(id, a)
    23           }
    24           catch {
    25             case _: XML.XML_Atom => None
    26             case _: XML.XML_Body => None
    27           }
    28         case _ => None
    29       }
    30   }
    31 
    32 
    33   /* toplevel transactions */
    34 
    35   sealed abstract class Status
    36   case object Unprocessed extends Status
    37   case class Forked(forks: Int) extends Status
    38   case object Finished extends Status
    39   case object Failed extends Status
    40 
    41   def command_status(markup: List[Markup]): Status =
    42   {
    43     val forks = (0 /: markup) {
    44       case (i, Markup(Markup.FORKED, _)) => i + 1
    45       case (i, Markup(Markup.JOINED, _)) => i - 1
    46       case (i, _) => i
    47     }
    48     if (forks != 0) Forked(forks)
    49     else if (markup.exists(_.name == Markup.FAILED)) Failed
    50     else if (markup.exists(_.name == Markup.FINISHED)) Finished
    51     else Unprocessed
    52   }
    53 
    54   sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
    55 
    56   def node_status(
    57     state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
    58   {
    59     var unprocessed = 0
    60     var running = 0
    61     var finished = 0
    62     var failed = 0
    63     node.commands.foreach(command =>
    64       command_status(state.command_state(version, command).status) match {
    65         case Unprocessed => unprocessed += 1
    66         case Forked(_) => running += 1
    67         case Finished => finished += 1
    68         case Failed => failed += 1
    69       })
    70     Node_Status(unprocessed, running, finished, failed)
    71   }
    72 
    73 
    74   /* result messages */
    75 
    76   def clean_message(body: XML.Body): XML.Body =
    77     body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
    78       { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
    79 
    80   def message_reports(msg: XML.Tree): List[XML.Elem] =
    81     msg match {
    82       case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
    83       case XML.Elem(_, body) => body.flatMap(message_reports)
    84       case XML.Text(_) => Nil
    85     }
    86 
    87 
    88   /* specific messages */
    89 
    90   def is_ready(msg: XML.Tree): Boolean =
    91     msg match {
    92       case XML.Elem(Markup(Markup.STATUS, _),
    93         List(XML.Elem(Markup(Markup.READY, _), _))) => true
    94       case _ => false
    95     }
    96 
    97  def is_tracing(msg: XML.Tree): Boolean =
    98     msg match {
    99       case XML.Elem(Markup(Markup.TRACING, _), _) => true
   100       case _ => false
   101     }
   102 
   103   def is_warning(msg: XML.Tree): Boolean =
   104     msg match {
   105       case XML.Elem(Markup(Markup.WARNING, _), _) => true
   106       case _ => false
   107     }
   108 
   109   def is_error(msg: XML.Tree): Boolean =
   110     msg match {
   111       case XML.Elem(Markup(Markup.ERROR, _), _) => true
   112       case _ => false
   113     }
   114 
   115   def is_state(msg: XML.Tree): Boolean =
   116     msg match {
   117       case XML.Elem(Markup(Markup.WRITELN, _),
   118         List(XML.Elem(Markup(Markup.STATE, _), _))) => true
   119       case _ => false
   120     }
   121 
   122 
   123   /* reported positions */
   124 
   125   private val include_pos =
   126     Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
   127 
   128   def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   129   {
   130     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
   131       tree match {
   132         case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
   133         if include_pos(name) && id == command.id =>
   134           val range = command.decode(raw_range).restrict(command.range)
   135           body.foldLeft(if (range.is_singularity) set else set + range)(positions)
   136         case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
   137         case _ => set
   138       }
   139     val set = positions(Set.empty, message)
   140     if (set.isEmpty && !is_state(message))
   141       set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
   142     else set
   143   }
   144 }
   145 
   146 
   147 trait Isar_Document extends Isabelle_Process
   148 {
   149   /* commands */
   150 
   151   def define_command(command: Command): Unit =
   152     input("Isar_Document.define_command",
   153       Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
   154 
   155 
   156   /* document versions */
   157 
   158   def cancel_execution()
   159   {
   160     input("Isar_Document.cancel_execution")
   161   }
   162 
   163   def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
   164     name: Document.Node.Name, perspective: Command.Perspective)
   165   {
   166     val ids =
   167     { import XML.Encode._
   168       list(long)(perspective.commands.map(_.id)) }
   169 
   170     input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
   171       name.node, YXML.string_of_body(ids))
   172   }
   173 
   174   def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
   175     edits: List[Document.Edit_Command])
   176   {
   177     val edits_yxml =
   178     { import XML.Encode._
   179       def id: T[Command] = (cmd => long(cmd.id))
   180       def encode: T[List[Document.Edit_Command]] =
   181         list(pair((name => string(name.node)),
   182           variant(List(
   183             { case Document.Node.Clear() => (Nil, Nil) },
   184             { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
   185             { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
   186                 (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
   187             { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
   188             { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))))
   189       YXML.string_of_body(encode(edits)) }
   190 
   191     input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
   192   }
   193 
   194 
   195   /* method invocation service */
   196 
   197   def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
   198   {
   199     input("Isar_Document.invoke_scala", id, tag.toString, res)
   200   }
   201 }