clarified modules;
authorwenzelm
Mon Mar 16 11:07:56 2015 +0100 (2015-03-16)
changeset 597136da3efec20ca
parent 59711 5b0003211207
child 59714 ae322325adbb
clarified modules;
src/Pure/PIDE/command.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/protocol_message.scala
src/Pure/PIDE/prover.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Mar 15 23:46:00 2015 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon Mar 16 11:07:56 2015 +0100
     1.3 @@ -234,7 +234,7 @@
     1.4                if (Protocol.is_inlined(message)) {
     1.5                  for {
     1.6                    (chunk_name, chunk) <- command.chunks.iterator
     1.7 -                  range <- Protocol.message_positions(
     1.8 +                  range <- Protocol_Message.positions(
     1.9                      self_id, command.position, chunk_name, chunk, message)
    1.10                  } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
    1.11                }
     2.1 --- a/src/Pure/PIDE/protocol.scala	Sun Mar 15 23:46:00 2015 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Mar 16 11:07:56 2015 +0100
     2.3 @@ -186,34 +186,6 @@
     2.4  
     2.5    /* result messages */
     2.6  
     2.7 -  private val clean_elements =
     2.8 -    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
     2.9 -
    2.10 -  def clean_message(body: XML.Body): XML.Body =
    2.11 -    body filter {
    2.12 -      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
    2.13 -      case XML.Elem(Markup(name, _), _) => !clean_elements(name)
    2.14 -      case _ => true
    2.15 -    } map {
    2.16 -      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
    2.17 -      case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts))
    2.18 -      case t => t
    2.19 -    }
    2.20 -
    2.21 -  def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    2.22 -    body flatMap {
    2.23 -      case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
    2.24 -        List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
    2.25 -      case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
    2.26 -        List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
    2.27 -      case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
    2.28 -      case XML.Elem(_, ts) => message_reports(props, ts)
    2.29 -      case XML.Text(_) => Nil
    2.30 -    }
    2.31 -
    2.32 -
    2.33 -  /* specific messages */
    2.34 -
    2.35    def is_result(msg: XML.Tree): Boolean =
    2.36      msg match {
    2.37        case XML.Elem(Markup(Markup.RESULT, _), _) => true
    2.38 @@ -302,53 +274,6 @@
    2.39          case _ => None
    2.40        }
    2.41    }
    2.42 -
    2.43 -
    2.44 -  /* reported positions */
    2.45 -
    2.46 -  private val position_elements =
    2.47 -    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    2.48 -
    2.49 -  def message_positions(
    2.50 -    self_id: Document_ID.Generic => Boolean,
    2.51 -    command_position: Position.T,
    2.52 -    chunk_name: Symbol.Text_Chunk.Name,
    2.53 -    chunk: Symbol.Text_Chunk,
    2.54 -    message: XML.Elem): Set[Text.Range] =
    2.55 -  {
    2.56 -    def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
    2.57 -      props match {
    2.58 -        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
    2.59 -          val opt_range =
    2.60 -            Position.Range.unapply(props) orElse {
    2.61 -              if (name == Symbol.Text_Chunk.Default)
    2.62 -                Position.Range.unapply(command_position)
    2.63 -              else None
    2.64 -            }
    2.65 -          opt_range match {
    2.66 -            case Some(symbol_range) =>
    2.67 -              chunk.incorporate(symbol_range) match {
    2.68 -                case Some(range) => set + range
    2.69 -                case _ => set
    2.70 -              }
    2.71 -            case None => set
    2.72 -          }
    2.73 -        case _ => set
    2.74 -      }
    2.75 -
    2.76 -    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    2.77 -      tree match {
    2.78 -        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
    2.79 -          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
    2.80 -        case XML.Elem(Markup(name, props), body) =>
    2.81 -          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
    2.82 -        case XML.Text(_) => set
    2.83 -      }
    2.84 -
    2.85 -    val set = positions(Set.empty, message)
    2.86 -    if (set.isEmpty) elem_positions(message.markup.properties, set)
    2.87 -    else set
    2.88 -  }
    2.89  }
    2.90  
    2.91  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/PIDE/protocol_message.scala	Mon Mar 16 11:07:56 2015 +0100
     3.3 @@ -0,0 +1,84 @@
     3.4 +/*  Title:      Pure/PIDE/protocol_message.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Auxiliary operations on protocol messages.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +object Protocol_Message
    3.14 +{
    3.15 +  /* inlined reports */
    3.16 +
    3.17 +  private val report_elements =
    3.18 +    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
    3.19 +
    3.20 +  def clean_reports(body: XML.Body): XML.Body =
    3.21 +    body filter {
    3.22 +      case XML.Wrapped_Elem(Markup(name, _), _, _) => !report_elements(name)
    3.23 +      case XML.Elem(Markup(name, _), _) => !report_elements(name)
    3.24 +      case _ => true
    3.25 +    } map {
    3.26 +      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_reports(ts))
    3.27 +      case XML.Elem(markup, ts) => XML.Elem(markup, clean_reports(ts))
    3.28 +      case t => t
    3.29 +    }
    3.30 +
    3.31 +  def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    3.32 +    body flatMap {
    3.33 +      case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
    3.34 +        List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
    3.35 +      case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
    3.36 +        List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
    3.37 +      case XML.Wrapped_Elem(_, _, ts) => reports(props, ts)
    3.38 +      case XML.Elem(_, ts) => reports(props, ts)
    3.39 +      case XML.Text(_) => Nil
    3.40 +    }
    3.41 +
    3.42 +
    3.43 +  /* reported positions */
    3.44 +
    3.45 +  private val position_elements =
    3.46 +    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    3.47 +
    3.48 +  def positions(
    3.49 +    self_id: Document_ID.Generic => Boolean,
    3.50 +    command_position: Position.T,
    3.51 +    chunk_name: Symbol.Text_Chunk.Name,
    3.52 +    chunk: Symbol.Text_Chunk,
    3.53 +    message: XML.Elem): Set[Text.Range] =
    3.54 +  {
    3.55 +    def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
    3.56 +      props match {
    3.57 +        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
    3.58 +          val opt_range =
    3.59 +            Position.Range.unapply(props) orElse {
    3.60 +              if (name == Symbol.Text_Chunk.Default)
    3.61 +                Position.Range.unapply(command_position)
    3.62 +              else None
    3.63 +            }
    3.64 +          opt_range match {
    3.65 +            case Some(symbol_range) =>
    3.66 +              chunk.incorporate(symbol_range) match {
    3.67 +                case Some(range) => set + range
    3.68 +                case _ => set
    3.69 +              }
    3.70 +            case None => set
    3.71 +          }
    3.72 +        case _ => set
    3.73 +      }
    3.74 +    def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
    3.75 +      t match {
    3.76 +        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
    3.77 +          body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
    3.78 +        case XML.Elem(Markup(name, props), body) =>
    3.79 +          body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
    3.80 +        case XML.Text(_) => set
    3.81 +      }
    3.82 +
    3.83 +    val set = tree(Set.empty, message)
    3.84 +    if (set.isEmpty) elem(message.markup.properties, set)
    3.85 +    else set
    3.86 +  }
    3.87 +}
     4.1 --- a/src/Pure/PIDE/prover.scala	Sun Mar 15 23:46:00 2015 +0100
     4.2 +++ b/src/Pure/PIDE/prover.scala	Mon Mar 16 11:07:56 2015 +0100
     4.3 @@ -108,8 +108,8 @@
     4.4    {
     4.5      if (kind == Markup.INIT) system_channel.accepted()
     4.6  
     4.7 -    val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
     4.8 -    val reports = Protocol.message_reports(props, body)
     4.9 +    val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
    4.10 +    val reports = Protocol_Message.reports(props, body)
    4.11      for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
    4.12    }
    4.13  
     5.1 --- a/src/Pure/build-jars	Sun Mar 15 23:46:00 2015 +0100
     5.2 +++ b/src/Pure/build-jars	Mon Mar 16 11:07:56 2015 +0100
     5.3 @@ -64,6 +64,7 @@
     5.4    PIDE/markup.scala
     5.5    PIDE/markup_tree.scala
     5.6    PIDE/protocol.scala
     5.7 +  PIDE/protocol_message.scala
     5.8    PIDE/prover.scala
     5.9    PIDE/query_operation.scala
    5.10    PIDE/resources.scala