src/Pure/PIDE/markup.scala
changeset 50500 c94bba7906d2
parent 50499 f496b2b7bafb
child 50501 6f41f1646617
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Dec 12 23:36:07 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Dec 13 13:52:18 2012 +0100
     1.3 @@ -213,30 +213,6 @@
     1.4    val SUBGOAL = "subgoal"
     1.5  
     1.6  
     1.7 -  /* active areas */
     1.8 -
     1.9 -  val GRAPHVIEW = "graphview"
    1.10 -
    1.11 -  val SENDBACK = "sendback"
    1.12 -  val PADDING = "padding"
    1.13 -  val PADDING_LINE = (PADDING, LINE)
    1.14 -
    1.15 -  val DIALOG = "dialog"
    1.16 -  val DIALOG_RESULT = "dialog_result"
    1.17 -  val Result = new Properties.String("result")
    1.18 -
    1.19 -  object Dialog_Args
    1.20 -  {
    1.21 -    def unapply(props: Properties.T): Option[(String, String)] =
    1.22 -      (props, props) match {
    1.23 -        case (Markup.Name(name), Markup.Result(result)) => Some((name, result))
    1.24 -        case _ => None
    1.25 -      }
    1.26 -  }
    1.27 -
    1.28 -  val INTENSIFY = "intensify"
    1.29 -
    1.30 -
    1.31    /* command status */
    1.32  
    1.33    val TASK = "task"
    1.34 @@ -270,6 +246,7 @@
    1.35    val INIT = "init"
    1.36    val STATUS = "status"
    1.37    val REPORT = "report"
    1.38 +  val RESULT = "result"
    1.39    val WRITELN = "writeln"
    1.40    val TRACING = "tracing"
    1.41    val WARNING = "warning"
    1.42 @@ -298,6 +275,20 @@
    1.43  
    1.44    val BAD = "bad"
    1.45  
    1.46 +  val INTENSIFY = "intensify"
    1.47 +
    1.48 +
    1.49 +  /* active areas */
    1.50 +
    1.51 +  val GRAPHVIEW = "graphview"
    1.52 +
    1.53 +  val SENDBACK = "sendback"
    1.54 +  val PADDING = "padding"
    1.55 +  val PADDING_LINE = (PADDING, LINE)
    1.56 +
    1.57 +  val DIALOG = "dialog"
    1.58 +  val Result = new Properties.String("result")
    1.59 +
    1.60  
    1.61    /* protocol message functions */
    1.62