trace windows uses search feature of Pretty_Text_Area;
authorLars Hupel <lars.hupel@mytum.de>
Mon May 19 19:17:15 2014 +0200 (2014-05-19)
changeset 57004c8288ce9676a
parent 57003 188b70a00229
child 57005 33f3d2ea803d
trace windows uses search feature of Pretty_Text_Area;
recursive invocations and intermediate steps are now shown in order;
refinements to the exclusion of uninteresting subtraces in the output
src/Tools/jEdit/src/simplifier_trace_window.scala
     1.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Mon May 19 16:51:44 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Mon May 19 19:17:15 2014 +0200
     1.3 @@ -27,83 +27,62 @@
     1.4  {
     1.5    sealed trait Trace_Tree
     1.6    {
     1.7 -    var children: SortedMap[Long, Elem_Tree] = SortedMap.empty
     1.8 +    // FIXME replace with immutable tree builder
     1.9 +    var children: SortedMap[Long, Either[Simplifier_Trace.Item.Data, Elem_Tree]] = SortedMap.empty
    1.10      val serial: Long
    1.11      val parent: Option[Trace_Tree]
    1.12 -    var hints: List[Simplifier_Trace.Item.Data]
    1.13 -    def set_interesting(): Unit
    1.14 +    val markup: String
    1.15 +    def interesting: Boolean
    1.16 +
    1.17 +    def tree_children: List[Elem_Tree] = children.values.toList.collect {
    1.18 +      case Right(tree) => tree
    1.19 +    }
    1.20    }
    1.21  
    1.22    final class Root_Tree(val serial: Long) extends Trace_Tree
    1.23    {
    1.24      val parent = None
    1.25 -    val hints = Nil
    1.26 -    def hints_=(xs: List[Simplifier_Trace.Item.Data]) =
    1.27 -      throw new IllegalStateException("Root_Tree.hints")
    1.28 -    def set_interesting() = ()
    1.29 +    val interesting = true
    1.30 +    val markup = ""
    1.31  
    1.32 -    def format(regex: Option[Regex]): XML.Body =
    1.33 -      Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut))
    1.34 +    def format: XML.Body =
    1.35 +      Pretty.separate(tree_children.flatMap(_.format))
    1.36    }
    1.37  
    1.38    final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree])
    1.39      extends Trace_Tree
    1.40    {
    1.41      val serial = data.serial
    1.42 -    var hints = List.empty[Simplifier_Trace.Item.Data]
    1.43 -    var interesting: Boolean = false
    1.44 +    val markup = data.markup
    1.45  
    1.46 -    def set_interesting(): Unit =
    1.47 -      if (!interesting)
    1.48 -      {
    1.49 -        interesting = true
    1.50 -        parent match {
    1.51 -          case Some(p) =>
    1.52 -            p.set_interesting()
    1.53 -          case None =>
    1.54 -        }
    1.55 -      }
    1.56 +    lazy val interesting: Boolean =
    1.57 +      data.markup == Markup.SIMP_TRACE_STEP ||
    1.58 +      data.markup == Markup.SIMP_TRACE_LOG ||
    1.59 +      tree_children.exists(_.interesting)
    1.60  
    1.61 -    def format(regex: Option[Regex]): (Boolean, XML.Tree) =
    1.62 +    private def body_contains(regex: Regex, body: XML.Body): Boolean =
    1.63 +      body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
    1.64 +
    1.65 +    def format: Option[XML.Tree] =
    1.66      {
    1.67 -      def format_child(child: Elem_Tree): Option[XML.Tree] = child.format(regex) match {
    1.68 -        case (false, _) =>
    1.69 -          None
    1.70 -        case (true, res) =>
    1.71 -          Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
    1.72 -      }
    1.73 -
    1.74        def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree =
    1.75 -        Pretty.block(Pretty.separate(
    1.76 -          XML.Text(data.text) ::
    1.77 -          data.content
    1.78 -        ))
    1.79 -
    1.80 -      def body_contains(regex: Regex, body: XML.Body): Boolean =
    1.81 -        body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
    1.82 -
    1.83 -      val children_bodies: XML.Body =
    1.84 -        children.values.filter(_.interesting).flatMap(format_child).toList
    1.85 -
    1.86 -      lazy val hint_bodies: XML.Body =
    1.87 -        hints.reverse.map(format_hint)
    1.88 +        Pretty.block(Pretty.separate(XML.Text(data.text) :: data.content))
    1.89  
    1.90 -      val eligible = regex match {
    1.91 -        case None =>
    1.92 -          true
    1.93 -        case Some(r) =>
    1.94 -          body_contains(r, data.content) || hints.exists(h => body_contains(r, h.content))
    1.95 -      }
    1.96 +      lazy val bodies: XML.Body =
    1.97 +        children.values.toList.collect {
    1.98 +          case Left(data) => Some(format_hint(data))
    1.99 +          case Right(tree) if tree.interesting => tree.format
   1.100 +        }.flatten.map(item =>
   1.101 +          XML.Elem(Markup(Markup.ITEM, Nil), List(item))
   1.102 +        )
   1.103  
   1.104 -      val all =
   1.105 -        if (eligible)
   1.106 -          XML.Text(data.text) :: data.content ::: children_bodies ::: hint_bodies
   1.107 -        else
   1.108 -          XML.Text(data.text) :: children_bodies
   1.109 -
   1.110 +      val all = XML.Text(data.text) :: data.content ::: bodies
   1.111        val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all))))
   1.112  
   1.113 -      (eligible || children_bodies != Nil, res)
   1.114 +      if (bodies != Nil)
   1.115 +        Some(res)
   1.116 +      else
   1.117 +        None
   1.118      }
   1.119    }
   1.120  
   1.121 @@ -117,7 +96,15 @@
   1.122            case Some(parent) =>
   1.123              if (head.markup == Markup.SIMP_TRACE_HINT)
   1.124              {
   1.125 -              parent.hints ::= head
   1.126 +              head.props match {
   1.127 +                case Simplifier_Trace.Success(x)
   1.128 +                  if x ||
   1.129 +                     parent.markup == Markup.SIMP_TRACE_LOG ||
   1.130 +                     parent.markup == Markup.SIMP_TRACE_STEP =>
   1.131 +                  parent.children += ((head.serial, Left(head)))
   1.132 +                case _ =>
   1.133 +                  // ignore
   1.134 +              }
   1.135                walk_trace(tail, lookup)
   1.136              }
   1.137              else if (head.markup == Markup.SIMP_TRACE_IGNORE)
   1.138 @@ -127,15 +114,13 @@
   1.139                    Output.error_message("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
   1.140                  case Some(tree) =>
   1.141                    tree.children -= head.parent
   1.142 -                  walk_trace(tail, lookup) // FIXME discard from lookup
   1.143 +                  walk_trace(tail, lookup)
   1.144                }
   1.145              }
   1.146              else
   1.147              {
   1.148                val entry = new Elem_Tree(head, Some(parent))
   1.149 -              parent.children += ((head.serial, entry))
   1.150 -              if (head.markup == Markup.SIMP_TRACE_STEP || head.markup == Markup.SIMP_TRACE_LOG)
   1.151 -                entry.set_interesting()
   1.152 +              parent.children += ((head.serial, Right(entry)))
   1.153                walk_trace(tail, lookup + (head.serial -> entry))
   1.154              }
   1.155  
   1.156 @@ -152,13 +137,15 @@
   1.157  {
   1.158    Swing_Thread.require {}
   1.159  
   1.160 -  val area = new Pretty_Text_Area(view)
   1.161 +  val pretty_text_area = new Pretty_Text_Area(view)
   1.162  
   1.163    size = new Dimension(500, 500)
   1.164    contents = new BorderPanel {
   1.165 -    layout(Component.wrap(area)) = BorderPanel.Position.Center
   1.166 +    layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
   1.167    }
   1.168  
   1.169 +  trace.entries.foreach(System.err.println)
   1.170 +
   1.171    private val tree = trace.entries.headOption match {
   1.172      case Some(first) =>
   1.173        val tree = new Simplifier_Trace_Window.Root_Tree(first.parent)
   1.174 @@ -168,20 +155,20 @@
   1.175        new Simplifier_Trace_Window.Root_Tree(0)
   1.176    }
   1.177  
   1.178 -  do_update(None)
   1.179 +  do_update()
   1.180    open()
   1.181    do_paint()
   1.182  
   1.183 -  def do_update(regex: Option[Regex])
   1.184 +  def do_update()
   1.185    {
   1.186 -    val xml = tree.format(regex)
   1.187 -    area.update(snapshot, Command.Results.empty, xml)
   1.188 +    val xml = tree.format
   1.189 +    pretty_text_area.update(snapshot, Command.Results.empty, xml)
   1.190    }
   1.191  
   1.192    def do_paint()
   1.193    {
   1.194      Swing_Thread.later {
   1.195 -      area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
   1.196 +      pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
   1.197      }
   1.198    }
   1.199  
   1.200 @@ -204,28 +191,9 @@
   1.201  
   1.202    /* controls */
   1.203  
   1.204 -  val use_regex = new CheckBox("Regex")
   1.205 -
   1.206    private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
   1.207 -    new Label("Search"),
   1.208 -    new TextField(30) {
   1.209 -      listenTo(keys)
   1.210 -      reactions += {
   1.211 -        case KeyPressed(_, Key.Enter, 0, _) =>
   1.212 -          val input = text.trim
   1.213 -          val regex =
   1.214 -            if (input.isEmpty)
   1.215 -              None
   1.216 -            else if (use_regex.selected)
   1.217 -              Some(input.r)
   1.218 -            else
   1.219 -              Some(java.util.regex.Pattern.quote(input).r)
   1.220 -          do_update(regex)
   1.221 -          do_paint()
   1.222 -      }
   1.223 -    },
   1.224 -    use_regex
   1.225 -  )
   1.226 +    pretty_text_area.search_label,
   1.227 +    pretty_text_area.search_pattern)
   1.228  
   1.229    peer.add(controls.peer, BorderLayout.NORTH)
   1.230  }