more formal class Command.Results;
authorwenzelm
Fri Dec 14 12:09:08 2012 +0100 (2012-12-14)
changeset 505079605b0d93d1e
parent 50505 33c92722cc3d
child 50508 5b7150395568
more formal class Command.Results;
src/Pure/PIDE/command.scala
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Dec 13 19:53:55 2012 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Fri Dec 14 12:09:08 2012 +0100
     1.3 @@ -17,13 +17,30 @@
     1.4  {
     1.5    /** accumulated results from prover **/
     1.6  
     1.7 -  type Results = SortedMap[Long, XML.Tree]
     1.8 -  val empty_results: Results = SortedMap.empty
     1.9 +  /* results */
    1.10 +
    1.11 +  object Results
    1.12 +  {
    1.13 +    val empty = new Results(SortedMap.empty)
    1.14 +    def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
    1.15 +  }
    1.16 +
    1.17 +  final class Results private(private val rep: SortedMap[Long, XML.Tree])
    1.18 +  {
    1.19 +    def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
    1.20 +    def get(serial: Long): Option[XML.Tree] = rep.get(serial)
    1.21 +    def entries: Iterator[(Long, XML.Tree)] = rep.iterator
    1.22 +    def + (entry: (Long, XML.Tree)): Results = new Results(rep + entry)
    1.23 +    def ++ (other: Results): Results = new Results(rep ++ other.rep)
    1.24 +  }
    1.25 +
    1.26 +
    1.27 +  /* state */
    1.28  
    1.29    sealed case class State(
    1.30      command: Command,
    1.31      status: List[Markup] = Nil,
    1.32 -    results: Results = empty_results,
    1.33 +    results: Results = Results.empty,
    1.34      markup: Markup_Tree = Markup_Tree.empty)
    1.35    {
    1.36      def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
    1.37 @@ -93,7 +110,7 @@
    1.38    type Span = List[Token]
    1.39  
    1.40    def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span,
    1.41 -    results: Results = empty_results, markup: Markup_Tree = Markup_Tree.empty): Command =
    1.42 +    results: Results = Results.empty, markup: Markup_Tree = Markup_Tree.empty): Command =
    1.43    {
    1.44      val source: String =
    1.45        span match {
    1.46 @@ -120,7 +137,7 @@
    1.47      Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
    1.48  
    1.49    def unparsed(source: String): Command =
    1.50 -    unparsed(Document.no_id, source, empty_results, Markup_Tree.empty)
    1.51 +    unparsed(Document.no_id, source, Results.empty, Markup_Tree.empty)
    1.52  
    1.53    def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
    1.54    {
     2.1 --- a/src/Pure/PIDE/protocol.scala	Thu Dec 13 19:53:55 2012 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Dec 14 12:09:08 2012 +0100
     2.3 @@ -106,7 +106,7 @@
     2.4          val status = command_status(st.status)
     2.5          if (status.is_running) running += 1
     2.6          else if (status.is_finished) {
     2.7 -          if (st.results.exists(p => is_warning(p._2))) warned += 1
     2.8 +          if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
     2.9            else finished += 1
    2.10          }
    2.11          else if (status.is_failed) failed += 1
     3.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Dec 13 19:53:55 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Fri Dec 14 12:09:08 2012 +0100
     3.3 @@ -65,7 +65,7 @@
     3.4            override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
     3.5            {
     3.6              val rendering = Rendering(snapshot, PIDE.options.value)
     3.7 -            new Pretty_Tooltip(view, parent, rendering, x, y, Command.empty_results, body)
     3.8 +            new Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
     3.9              null
    3.10            }
    3.11          }
     4.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Thu Dec 13 19:53:55 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Dec 14 12:09:08 2012 +0100
     4.3 @@ -26,7 +26,7 @@
     4.4    /* implicit arguments -- owned by Swing thread */
     4.5  
     4.6    private var implicit_snapshot = Document.State.init.snapshot()
     4.7 -  private var implicit_results = Command.empty_results
     4.8 +  private var implicit_results = Command.Results.empty
     4.9    private var implicit_info: XML.Body = Nil
    4.10  
    4.11    private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
    4.12 @@ -39,7 +39,7 @@
    4.13    }
    4.14  
    4.15    private def reset_implicit(): Unit =
    4.16 -    set_implicit(Document.State.init.snapshot(), Command.empty_results, Nil)
    4.17 +    set_implicit(Document.State.init.snapshot(), Command.Results.empty, Nil)
    4.18  
    4.19    def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
    4.20    {
     5.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Dec 13 19:53:55 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Dec 14 12:09:08 2012 +0100
     5.3 @@ -62,7 +62,7 @@
     5.4    private var current_font_size: Int = 12
     5.5    private var current_body: XML.Body = Nil
     5.6    private var current_base_snapshot = Document.State.init.snapshot()
     5.7 -  private var current_base_results = Command.empty_results
     5.8 +  private var current_base_results = Command.Results.empty
     5.9    private var current_rendering: Rendering =
    5.10      Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
    5.11    private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
     6.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 19:53:55 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Dec 14 12:09:08 2012 +0100
     6.3 @@ -256,7 +256,7 @@
     6.4      snapshot.select_markup(range, Some(active_include), command_state =>
     6.5          {
     6.6            case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
     6.7 -          if !command_state.results.isDefinedAt(serial) =>
     6.8 +          if !command_state.results.defined(serial) =>
     6.9              Text.Info(snapshot.convert(info_range), elem)
    6.10            case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
    6.11            if name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
    6.12 @@ -269,24 +269,25 @@
    6.13      val results =
    6.14        snapshot.select_markup[Command.Results](range, None, command_state =>
    6.15          { case _ => command_state.results }).map(_.info)
    6.16 -    (Command.empty_results /: results)(_ ++ _)
    6.17 +    (Command.Results.empty /: results)(_ ++ _)
    6.18    }
    6.19  
    6.20    def tooltip_message(range: Text.Range): XML.Body =
    6.21    {
    6.22      val msgs =
    6.23 -      snapshot.cumulate_markup[Command.Results](range, Command.empty_results,
    6.24 -        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
    6.25 -        {
    6.26 -          case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
    6.27 -          if name == Markup.WRITELN ||
    6.28 -              name == Markup.WARNING ||
    6.29 -              name == Markup.ERROR =>
    6.30 -            msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
    6.31 -          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    6.32 -          if !body.isEmpty => msgs + (Document.new_id() -> msg)
    6.33 -        }).toList.flatMap(_.info)
    6.34 -    Pretty.separate(msgs.iterator.map(_._2).toList)
    6.35 +      Command.Results.merge(
    6.36 +        snapshot.cumulate_markup[Command.Results](range, Command.Results.empty,
    6.37 +          Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
    6.38 +          {
    6.39 +            case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
    6.40 +            if name == Markup.WRITELN ||
    6.41 +                name == Markup.WARNING ||
    6.42 +                name == Markup.ERROR =>
    6.43 +              msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
    6.44 +            case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    6.45 +            if !body.isEmpty => msgs + (Document.new_id() -> msg)
    6.46 +          }).map(_.info))
    6.47 +    Pretty.separate(msgs.entries.map(_._2).toList)
    6.48    }
    6.49  
    6.50  
    6.51 @@ -420,7 +421,7 @@
    6.52  
    6.53    def output_messages(st: Command.State): List[XML.Tree] =
    6.54    {
    6.55 -    st.results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
    6.56 +    st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
    6.57    }
    6.58  
    6.59