src/Pure/PIDE/isar_document.scala
author wenzelm
Tue Sep 07 15:03:59 2010 +0200 (2010-09-07)
changeset 39170 04ad0fed81f5
parent 39042 470fd769ae53
child 39172 31b95e0da7b7
permissions -rw-r--r--
Isar_Document.reported_positions: exclude proof state output;
     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   /* reported positions */
    60 
    61   private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    62   private val exclude_pos = Set(Markup.LOCATION)
    63 
    64   private def is_state(msg: XML.Tree): Boolean =
    65     msg match {
    66       case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    67       case _ => false
    68     }
    69 
    70   def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
    71   {
    72     def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    73       tree match {
    74         case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
    75         if include_pos(name) && id == command_id =>
    76           body.foldLeft(set + range)(reported)
    77         case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
    78           body.foldLeft(set)(reported)
    79         case _ => set
    80       }
    81     val set = reported(Set.empty, message)
    82     if (set.isEmpty && !is_state(message))
    83       set ++ Position.Range.unapply(message.markup.properties)
    84     else set
    85   }
    86 }
    87 
    88 
    89 trait Isar_Document extends Isabelle_Process
    90 {
    91   import Isar_Document._
    92 
    93 
    94   /* commands */
    95 
    96   def define_command(id: Document.Command_ID, text: String): Unit =
    97     input("Isar_Document.define_command", Document.ID(id), text)
    98 
    99 
   100   /* document versions */
   101 
   102   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
   103       edits: List[Document.Edit[Document.Command_ID]])
   104   {
   105     val arg =
   106       XML_Data.make_list(
   107         XML_Data.make_pair(XML_Data.make_string)(
   108           XML_Data.make_option(XML_Data.make_list(
   109               XML_Data.make_pair(
   110                 XML_Data.make_option(XML_Data.make_long))(
   111                 XML_Data.make_option(XML_Data.make_long))))))(edits)
   112 
   113     input("Isar_Document.edit_version",
   114       Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
   115   }
   116 }