src/Pure/PIDE/isar_document.scala
author wenzelm
Mon Jul 11 16:48:02 2011 +0200 (2011-07-11)
changeset 43748 c70bd78ec83c
parent 43731 70072780e095
child 43767 e0219ef7f84c
permissions -rw-r--r--
JVM method invocation service via Scala layer;
     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     def unapply(msg: XML.Tree)
    16         : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
    17       msg match {
    18         case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
    19           val id_edits = edits.map(Edit.unapply)
    20           if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
    21           else None
    22         case _ => None
    23       }
    24   }
    25 
    26   object Edit {
    27     def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
    28       msg match {
    29         case XML.Elem(
    30           Markup(Markup.EDIT,
    31             List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
    32         case _ => None
    33       }
    34   }
    35 
    36 
    37   /* toplevel transactions */
    38 
    39   sealed abstract class Status
    40   case class Forked(forks: Int) extends Status
    41   case object Unprocessed extends Status
    42   case object Finished extends Status
    43   case object Failed extends Status
    44 
    45   def command_status(markup: List[Markup]): Status =
    46   {
    47     val forks = (0 /: markup) {
    48       case (i, Markup(Markup.FORKED, _)) => i + 1
    49       case (i, Markup(Markup.JOINED, _)) => i - 1
    50       case (i, _) => i
    51     }
    52     if (forks != 0) Forked(forks)
    53     else if (markup.exists(_.name == Markup.FAILED)) Failed
    54     else if (markup.exists(_.name == Markup.FINISHED)) Finished
    55     else Unprocessed
    56   }
    57 
    58 
    59   /* result messages */
    60 
    61   def clean_message(body: XML.Body): XML.Body =
    62     body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
    63       { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
    64 
    65   def message_reports(msg: XML.Tree): List[XML.Elem] =
    66     msg match {
    67       case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
    68       case XML.Elem(_, body) => body.flatMap(message_reports)
    69       case XML.Text(_) => Nil
    70     }
    71 
    72 
    73   /* specific messages */
    74 
    75   def is_ready(msg: XML.Tree): Boolean =
    76     msg match {
    77       case XML.Elem(Markup(Markup.STATUS, _),
    78         List(XML.Elem(Markup(Markup.READY, _), _))) => true
    79       case _ => false
    80     }
    81 
    82  def is_tracing(msg: XML.Tree): Boolean =
    83     msg match {
    84       case XML.Elem(Markup(Markup.TRACING, _), _) => true
    85       case _ => false
    86     }
    87 
    88   def is_warning(msg: XML.Tree): Boolean =
    89     msg match {
    90       case XML.Elem(Markup(Markup.WARNING, _), _) => true
    91       case _ => false
    92     }
    93 
    94   def is_error(msg: XML.Tree): Boolean =
    95     msg match {
    96       case XML.Elem(Markup(Markup.ERROR, _), _) => true
    97       case _ => false
    98     }
    99 
   100   def is_state(msg: XML.Tree): Boolean =
   101     msg match {
   102       case XML.Elem(Markup(Markup.WRITELN, _),
   103         List(XML.Elem(Markup(Markup.STATE, _), _))) => true
   104       case _ => false
   105     }
   106 
   107 
   108   /* reported positions */
   109 
   110   private val include_pos =
   111     Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
   112 
   113   def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   114   {
   115     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
   116       tree match {
   117         case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
   118         if include_pos(name) && id == command.id =>
   119           val range = command.decode(raw_range).restrict(command.range)
   120           body.foldLeft(if (range.is_singularity) set else set + range)(positions)
   121         case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
   122         case _ => set
   123       }
   124     val set = positions(Set.empty, message)
   125     if (set.isEmpty && !is_state(message))
   126       set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
   127     else set
   128   }
   129 }
   130 
   131 
   132 trait Isar_Document extends Isabelle_Process
   133 {
   134   /* commands */
   135 
   136   def define_command(id: Document.Command_ID, text: String): Unit =
   137     input("Isar_Document.define_command", Document.ID(id), text)
   138 
   139 
   140   /* document versions */
   141 
   142   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
   143       edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
   144   {
   145     val arg1 =
   146     { import XML_Data.Encode._
   147       list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
   148 
   149     val arg2 =
   150     { import XML_Data.Encode._
   151       list(pair(string, Thy_Header.encode_xml_data))(headers) }
   152 
   153     input("Isar_Document.edit_version",
   154       Document.ID(old_id), Document.ID(new_id),
   155         YXML.string_of_body(arg1), YXML.string_of_body(arg2))
   156   }
   157 
   158 
   159   /* method invocation service */
   160 
   161   def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
   162   {
   163     input("Isar_Document.invoke_scala", id, tag.toString, res)
   164   }
   165 }