src/Pure/PIDE/protocol.scala
changeset 50201 c26369c9eda6
parent 50157 76efdb6daab2
child 50450 358b6020f8b6
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sun Nov 25 18:50:13 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sun Nov 25 19:49:24 2012 +0100
     1.3 @@ -66,17 +66,17 @@
     1.4    }
     1.5  
     1.6    val command_status_markup: Set[String] =
     1.7 -    Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FORKED, Isabelle_Markup.JOINED,
     1.8 -      Isabelle_Markup.RUNNING, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED)
     1.9 +    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    1.10 +      Markup.FINISHED, Markup.FAILED)
    1.11  
    1.12    def command_status(status: Status, markup: Markup): Status =
    1.13      markup match {
    1.14 -      case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true)
    1.15 -      case Markup(Isabelle_Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
    1.16 -      case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
    1.17 -      case Markup(Isabelle_Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
    1.18 -      case Markup(Isabelle_Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
    1.19 -      case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
    1.20 +      case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
    1.21 +      case Markup(Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
    1.22 +      case Markup(Markup.JOINED, _) => status.copy(forks = status.forks - 1)
    1.23 +      case Markup(Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
    1.24 +      case Markup(Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
    1.25 +      case Markup(Markup.FAILED, _) => status.copy(failed = true)
    1.26        case _ => status
    1.27      }
    1.28  
    1.29 @@ -120,8 +120,8 @@
    1.30  
    1.31    def clean_message(body: XML.Body): XML.Body =
    1.32      body filter {
    1.33 -      case XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => false
    1.34 -      case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false
    1.35 +      case XML.Elem(Markup(Markup.REPORT, _), _) => false
    1.36 +      case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false
    1.37        case _ => true
    1.38      } map {
    1.39        case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
    1.40 @@ -131,8 +131,8 @@
    1.41  
    1.42    def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    1.43      body flatMap {
    1.44 -      case XML.Elem(Markup(Isabelle_Markup.REPORT, ps), ts) =>
    1.45 -        List(XML.Elem(Markup(Isabelle_Markup.REPORT, props ::: ps), ts))
    1.46 +      case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
    1.47 +        List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
    1.48        case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
    1.49        case XML.Elem(_, ts) => message_reports(props, ts)
    1.50        case XML.Text(_) => Nil
    1.51 @@ -143,40 +143,38 @@
    1.52  
    1.53    def is_tracing(msg: XML.Tree): Boolean =
    1.54      msg match {
    1.55 -      case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
    1.56 -      case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true
    1.57 +      case XML.Elem(Markup(Markup.TRACING, _), _) => true
    1.58 +      case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true
    1.59        case _ => false
    1.60      }
    1.61  
    1.62    def is_warning(msg: XML.Tree): Boolean =
    1.63      msg match {
    1.64 -      case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
    1.65 -      case XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _) => true
    1.66 +      case XML.Elem(Markup(Markup.WARNING, _), _) => true
    1.67 +      case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
    1.68        case _ => false
    1.69      }
    1.70  
    1.71    def is_error(msg: XML.Tree): Boolean =
    1.72      msg match {
    1.73 -      case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
    1.74 -      case XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _) => true
    1.75 +      case XML.Elem(Markup(Markup.ERROR, _), _) => true
    1.76 +      case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
    1.77        case _ => false
    1.78      }
    1.79  
    1.80    def is_state(msg: XML.Tree): Boolean =
    1.81      msg match {
    1.82 -      case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
    1.83 -        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
    1.84 -      case XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _),
    1.85 -        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
    1.86 +      case XML.Elem(Markup(Markup.WRITELN, _),
    1.87 +        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    1.88 +      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
    1.89 +        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    1.90        case _ => false
    1.91      }
    1.92  
    1.93  
    1.94    /* reported positions */
    1.95  
    1.96 -  private val include_pos =
    1.97 -    Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT,
    1.98 -      Isabelle_Markup.POSITION)
    1.99 +  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
   1.100  
   1.101    def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   1.102    {