concentrate protocol message formats in Isar_Document;
authorwenzelm
Fri Aug 20 11:57:43 2010 +0200 (2010-08-20)
changeset 38567b670faa807c9
parent 38566 8176107637ce
child 38568 f117ba49a59c
concentrate protocol message formats in Isar_Document;
src/Pure/Isar/toplevel.scala
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/build-jars
src/Tools/jEdit/src/jedit/document_view.scala
     1.1 --- a/src/Pure/Isar/toplevel.scala	Fri Aug 20 11:47:33 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,33 +0,0 @@
     1.4 -/*  Title:      Pure/Isar/toplevel.scala
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Isabelle/Isar toplevel transactions.
     1.8 -*/
     1.9 -
    1.10 -package isabelle
    1.11 -
    1.12 -
    1.13 -object Toplevel
    1.14 -{
    1.15 -  sealed abstract class Status
    1.16 -  case class Forked(forks: Int) extends Status
    1.17 -  case object Unprocessed extends Status
    1.18 -  case object Finished extends Status
    1.19 -  case object Failed extends Status
    1.20 -
    1.21 -  def command_status(markup: XML.Body): Status =
    1.22 -  {
    1.23 -    val forks = (0 /: markup) {
    1.24 -      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
    1.25 -      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
    1.26 -      case (i, _) => i
    1.27 -    }
    1.28 -    if (forks != 0) Forked(forks)
    1.29 -    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
    1.30 -      Failed
    1.31 -    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
    1.32 -      Finished
    1.33 -    else Unprocessed
    1.34 -  }
    1.35 -}
    1.36 -
     2.1 --- a/src/Pure/PIDE/isar_document.ML	Fri Aug 20 11:47:33 2010 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.ML	Fri Aug 20 11:57:43 2010 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      Pure/PIDE/isar_document.ML
     2.5      Author:     Makarius
     2.6  
     2.7 -Protocol commands for interactive Isar documents.
     2.8 +Protocol message formats for interactive Isar documents.
     2.9  *)
    2.10  
    2.11  structure Isar_Document: sig end =
     3.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Aug 20 11:47:33 2010 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 20 11:57:43 2010 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  /*  Title:      Pure/PIDE/isar_document.scala
     3.5      Author:     Makarius
     3.6  
     3.7 -Protocol commands for interactive Isar documents.
     3.8 +Protocol message formats for interactive Isar documents.
     3.9  */
    3.10  
    3.11  package isabelle
    3.12 @@ -9,7 +9,7 @@
    3.13  
    3.14  object Isar_Document
    3.15  {
    3.16 -  /* protocol messages */
    3.17 +  /* document editing */
    3.18  
    3.19    object Assign {
    3.20      def unapply(msg: XML.Tree)
    3.21 @@ -32,6 +32,30 @@
    3.22          case _ => None
    3.23        }
    3.24    }
    3.25 +
    3.26 +
    3.27 +  /* toplevel transactions */
    3.28 +
    3.29 +  sealed abstract class Status
    3.30 +  case class Forked(forks: Int) extends Status
    3.31 +  case object Unprocessed extends Status
    3.32 +  case object Finished extends Status
    3.33 +  case object Failed extends Status
    3.34 +
    3.35 +  def command_status(markup: XML.Body): Status =
    3.36 +  {
    3.37 +    val forks = (0 /: markup) {
    3.38 +      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
    3.39 +      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
    3.40 +      case (i, _) => i
    3.41 +    }
    3.42 +    if (forks != 0) Forked(forks)
    3.43 +    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
    3.44 +      Failed
    3.45 +    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
    3.46 +      Finished
    3.47 +    else Unprocessed
    3.48 +  }
    3.49  }
    3.50  
    3.51  
     4.1 --- a/src/Pure/build-jars	Fri Aug 20 11:47:33 2010 +0200
     4.2 +++ b/src/Pure/build-jars	Fri Aug 20 11:57:43 2010 +0200
     4.3 @@ -37,7 +37,6 @@
     4.4    Isar/keyword.scala
     4.5    Isar/outer_syntax.scala
     4.6    Isar/parse.scala
     4.7 -  Isar/toplevel.scala
     4.8    Isar/token.scala
     4.9    PIDE/command.scala
    4.10    PIDE/document.scala
     5.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Aug 20 11:47:33 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Aug 20 11:57:43 2010 +0200
     5.3 @@ -29,11 +29,11 @@
     5.4      val state = snapshot.state(command)
     5.5      if (snapshot.is_outdated) new Color(240, 240, 240)
     5.6      else
     5.7 -      Toplevel.command_status(state.status) match {
     5.8 -        case Toplevel.Forked(i) if i > 0 => new Color(255, 228, 225)
     5.9 -        case Toplevel.Finished => new Color(234, 248, 255)
    5.10 -        case Toplevel.Failed => new Color(255, 193, 193)
    5.11 -        case Toplevel.Unprocessed => new Color(255, 228, 225)
    5.12 +      Isar_Document.command_status(state.status) match {
    5.13 +        case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
    5.14 +        case Isar_Document.Finished => new Color(234, 248, 255)
    5.15 +        case Isar_Document.Failed => new Color(255, 193, 193)
    5.16 +        case Isar_Document.Unprocessed => new Color(255, 228, 225)
    5.17          case _ => Color.red
    5.18        }
    5.19    }