more careful handling of Dialog_Result, with active area and color feedback;
authorwenzelm
Thu Dec 13 17:29:23 2012 +0100 (2012-12-13 ago)
changeset 505016f41f1646617
parent 50500 c94bba7906d2
child 50502 51408dde956f
more careful handling of Dialog_Result, with active area and color feedback;
more formal type Command.Results;
propagate command results to output, which is required to resolve update of dialog state;
clarified Markup.message: retain uninterpreted messages;
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Dec 13 13:52:18 2012 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Dec 13 17:29:23 2012 +0100
     1.3 @@ -17,11 +17,14 @@
     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 +
    1.10    sealed case class State(
    1.11 -    val command: Command,
    1.12 -    val status: List[Markup] = Nil,
    1.13 -    val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
    1.14 -    val markup: Markup_Tree = Markup_Tree.empty)
    1.15 +    command: Command,
    1.16 +    status: List[Markup] = Nil,
    1.17 +    results: Results = empty_results,
    1.18 +    markup: Markup_Tree = Markup_Tree.empty)
    1.19    {
    1.20      def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
    1.21        markup.to_XML(command.range, command.source, filter)
    1.22 @@ -89,8 +92,8 @@
    1.23  
    1.24    type Span = List[Token]
    1.25  
    1.26 -  def apply(id: Document.Command_ID, node_name: Document.Node.Name,
    1.27 -    span: Span, markup: Markup_Tree): Command =
    1.28 +  def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span,
    1.29 +    results: Results = empty_results, markup: Markup_Tree = Markup_Tree.empty): Command =
    1.30    {
    1.31      val source: String =
    1.32        span match {
    1.33 @@ -107,21 +110,23 @@
    1.34        i += n
    1.35      }
    1.36  
    1.37 -    new Command(id, node_name, span1.toList, source, markup)
    1.38 +    new Command(id, node_name, span1.toList, source, results, markup)
    1.39    }
    1.40  
    1.41 -  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil, Markup_Tree.empty)
    1.42 +  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
    1.43  
    1.44 -  def unparsed(id: Document.Command_ID, source: String, markup: Markup_Tree): Command =
    1.45 -    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), markup)
    1.46 +  def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree)
    1.47 +      : Command =
    1.48 +    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
    1.49  
    1.50 -  def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty)
    1.51 +  def unparsed(source: String): Command =
    1.52 +    unparsed(Document.no_id, source, empty_results, Markup_Tree.empty)
    1.53  
    1.54 -  def rich_text(id: Document.Command_ID, body: XML.Body): Command =
    1.55 +  def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
    1.56    {
    1.57      val text = XML.content(body)
    1.58      val markup = Markup_Tree.from_XML(body)
    1.59 -    unparsed(id, text, markup)
    1.60 +    unparsed(id, text, results, markup)
    1.61    }
    1.62  
    1.63  
    1.64 @@ -152,6 +157,7 @@
    1.65      val node_name: Document.Node.Name,
    1.66      val span: Command.Span,
    1.67      val source: String,
    1.68 +    val init_results: Command.Results,
    1.69      val init_markup: Markup_Tree)
    1.70  {
    1.71    /* classification */
    1.72 @@ -188,5 +194,6 @@
    1.73  
    1.74    /* accumulated results */
    1.75  
    1.76 -  val init_state: Command.State = Command.State(this, markup = init_markup)
    1.77 +  val init_state: Command.State =
    1.78 +    Command.State(this, results = init_results, markup = init_markup)
    1.79  }
     2.1 --- a/src/Pure/PIDE/markup.scala	Thu Dec 13 13:52:18 2012 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Thu Dec 13 17:29:23 2012 +0100
     2.3 @@ -264,8 +264,7 @@
     2.4  
     2.5    val message: String => String =
     2.6      Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
     2.7 -        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
     2.8 -      .withDefault((name: String) => name + "_message")
     2.9 +        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE).withDefault((s: String) => s)
    2.10  
    2.11    val Return_Code = new Properties.Int("return_code")
    2.12  
     3.1 --- a/src/Pure/PIDE/protocol.scala	Thu Dec 13 13:52:18 2012 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Dec 13 17:29:23 2012 +0100
     3.3 @@ -209,13 +209,15 @@
     3.4  
     3.5    object Dialog_Result
     3.6    {
     3.7 -    def apply(serial: Long, result: String): XML.Elem =
     3.8 -      XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result)))
     3.9 +    def apply(id: Document.ID, serial: Long, result: String): XML.Elem =
    3.10 +    {
    3.11 +      val props = Position.Id(id) ::: Markup.Serial(serial)
    3.12 +      XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
    3.13 +    }
    3.14  
    3.15 -    def unapply(tree: XML.Tree): Option[(Long, String)] =
    3.16 +    def unapply(tree: XML.Tree): Option[String] =
    3.17        tree match {
    3.18 -        case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result))) =>
    3.19 -          Some((serial, result))
    3.20 +        case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
    3.21          case _ => None
    3.22        }
    3.23    }
     4.1 --- a/src/Pure/System/session.scala	Thu Dec 13 13:52:18 2012 +0100
     4.2 +++ b/src/Pure/System/session.scala	Thu Dec 13 17:29:23 2012 +0100
     4.3 @@ -422,7 +422,7 @@
     4.4  
     4.5          case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
     4.6            prover.get.dialog_result(serial, result)
     4.7 -          handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(serial, result)))
     4.8 +          handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
     4.9  
    4.10          case Messages(msgs) =>
    4.11            msgs foreach {
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Dec 13 13:52:18 2012 +0100
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Dec 13 17:29:23 2012 +0100
     5.3 @@ -68,7 +68,7 @@
     5.4        /* result structure */
     5.5  
     5.6        val spans = parse_spans(syntax.scan(text))
     5.7 -      spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty)))
     5.8 +      spans.foreach(span => add(Command(Document.no_id, node_name, span)))
     5.9        result()
    5.10      }
    5.11    }
    5.12 @@ -226,7 +226,7 @@
    5.13          commands
    5.14        case cmd :: _ =>
    5.15          val hook = commands.prev(cmd)
    5.16 -        val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty))
    5.17 +        val inserted = spans2.map(span => Command(Document.new_id(), name, span))
    5.18          (commands /: cmds2)(_ - _).append_after(hook, inserted)
    5.19      }
    5.20    }
     6.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Dec 13 13:52:18 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Thu Dec 13 17:29:23 2012 +0100
     6.3 @@ -65,7 +65,7 @@
     6.4            override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
     6.5            {
     6.6              val rendering = Rendering(snapshot, PIDE.options.value)
     6.7 -            new Pretty_Tooltip(view, parent, rendering, x, y, body)
     6.8 +            new Pretty_Tooltip(view, parent, rendering, x, y, Command.empty_results, body)
     6.9              null
    6.10            }
    6.11          }
     7.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Thu Dec 13 13:52:18 2012 +0100
     7.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Thu Dec 13 17:29:23 2012 +0100
     7.3 @@ -26,22 +26,24 @@
     7.4    /* implicit arguments -- owned by Swing thread */
     7.5  
     7.6    private var implicit_snapshot = Document.State.init.snapshot()
     7.7 +  private var implicit_results = Command.empty_results
     7.8    private var implicit_info: XML.Body = Nil
     7.9  
    7.10 -  private def set_implicit(snapshot: Document.Snapshot, info: XML.Body)
    7.11 +  private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
    7.12    {
    7.13      Swing_Thread.require()
    7.14  
    7.15      implicit_snapshot = snapshot
    7.16 +    implicit_results = results
    7.17      implicit_info = info
    7.18    }
    7.19  
    7.20    private def reset_implicit(): Unit =
    7.21 -    set_implicit(Document.State.init.snapshot(), Nil)
    7.22 +    set_implicit(Document.State.init.snapshot(), Command.empty_results, Nil)
    7.23  
    7.24 -  def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
    7.25 +  def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
    7.26    {
    7.27 -    set_implicit(snapshot, info)
    7.28 +    set_implicit(snapshot, results, info)
    7.29      view.getDockableWindowManager.floatDockableWindow("isabelle-info")
    7.30    }
    7.31  }
    7.32 @@ -57,11 +59,12 @@
    7.33    private var zoom_factor = 100
    7.34  
    7.35    private val snapshot = Info_Dockable.implicit_snapshot
    7.36 +  private val results = Info_Dockable.implicit_results
    7.37    private val info = Info_Dockable.implicit_info
    7.38  
    7.39    private val window_focus_listener =
    7.40      new WindowFocusListener {
    7.41 -      def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, info) }
    7.42 +      def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, results, info) }
    7.43        def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
    7.44      }
    7.45  
    7.46 @@ -71,7 +74,7 @@
    7.47    private val pretty_text_area = new Pretty_Text_Area(view)
    7.48    set_content(pretty_text_area)
    7.49  
    7.50 -  pretty_text_area.update(snapshot, info)
    7.51 +  pretty_text_area.update(snapshot, results, info)
    7.52  
    7.53    private def handle_resize()
    7.54    {
     8.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Thu Dec 13 13:52:18 2012 +0100
     8.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Dec 13 17:29:23 2012 +0100
     8.3 @@ -77,7 +77,7 @@
     8.4        else current_output
     8.5  
     8.6      if (new_output != current_output)
     8.7 -      pretty_text_area.update(new_snapshot, Pretty.separate(new_output))
     8.8 +      pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
     8.9  
    8.10      current_snapshot = new_snapshot
    8.11      current_state = new_state
    8.12 @@ -152,7 +152,8 @@
    8.13    private val detach = new Button("Detach") {
    8.14      reactions += {
    8.15        case ButtonClicked(_) =>
    8.16 -        Info_Dockable(view, current_snapshot, Pretty.separate(current_output))
    8.17 +        Info_Dockable(view, current_snapshot,
    8.18 +          current_state.results, Pretty.separate(current_output))
    8.19      }
    8.20    }
    8.21    detach.tooltip = "Detach window with static copy of current output"
     9.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Dec 13 13:52:18 2012 +0100
     9.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Dec 13 17:29:23 2012 +0100
     9.3 @@ -21,18 +21,18 @@
     9.4  
     9.5  object Pretty_Text_Area
     9.6  {
     9.7 -  private def text_rendering(base_snapshot: Document.Snapshot, formatted_body: XML.Body):
     9.8 -    (String, Rendering) =
     9.9 +  private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
    9.10 +    formatted_body: XML.Body): (String, Rendering) =
    9.11    {
    9.12 -    val (text, state) = Pretty_Text_Area.document_state(base_snapshot, formatted_body)
    9.13 +    val (text, state) = Pretty_Text_Area.document_state(base_snapshot, base_results, formatted_body)
    9.14      val rendering = Rendering(state.snapshot(), PIDE.options.value)
    9.15      (text, rendering)
    9.16    }
    9.17  
    9.18 -  private def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
    9.19 -    : (String, Document.State) =
    9.20 +  private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
    9.21 +    formatted_body: XML.Body): (String, Document.State) =
    9.22    {
    9.23 -    val command = Command.rich_text(Document.new_id(), formatted_body)
    9.24 +    val command = Command.rich_text(Document.new_id(), base_results, formatted_body)
    9.25      val node_name = command.node_name
    9.26      val edits: List[Document.Edit_Text] =
    9.27        List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
    9.28 @@ -62,8 +62,9 @@
    9.29    private var current_font_size: Int = 12
    9.30    private var current_body: XML.Body = Nil
    9.31    private var current_base_snapshot = Document.State.init.snapshot()
    9.32 +  private var current_base_results = Command.empty_results
    9.33    private var current_rendering: Rendering =
    9.34 -    Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2
    9.35 +    Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
    9.36    private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
    9.37  
    9.38    private val rich_text_area =
    9.39 @@ -84,12 +85,14 @@
    9.40        val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
    9.41  
    9.42        val base_snapshot = current_base_snapshot
    9.43 +      val base_results = current_base_results
    9.44        val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
    9.45  
    9.46        future_rendering.map(_.cancel(true))
    9.47        future_rendering = Some(default_thread_pool.submit(() =>
    9.48          {
    9.49 -          val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
    9.50 +          val (text, rendering) =
    9.51 +            Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body)
    9.52            Simple_Thread.interrupted_exception()
    9.53  
    9.54            Swing_Thread.later {
    9.55 @@ -115,12 +118,13 @@
    9.56      refresh()
    9.57    }
    9.58  
    9.59 -  def update(base_snapshot: Document.Snapshot, body: XML.Body)
    9.60 +  def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
    9.61    {
    9.62      Swing_Thread.require()
    9.63      require(!base_snapshot.is_outdated)
    9.64  
    9.65      current_base_snapshot = base_snapshot
    9.66 +    current_base_results = base_results
    9.67      current_body = body
    9.68      refresh()
    9.69    }
    10.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Dec 13 13:52:18 2012 +0100
    10.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Dec 13 17:29:23 2012 +0100
    10.3 @@ -25,7 +25,9 @@
    10.4    view: View,
    10.5    parent: JComponent,
    10.6    rendering: Rendering,
    10.7 -  mouse_x: Int, mouse_y: Int, body: XML.Body)
    10.8 +  mouse_x: Int, mouse_y: Int,
    10.9 +  results: Command.Results,
   10.10 +  body: XML.Body)
   10.11    extends JWindow(JEdit_Lib.parent_window(parent) getOrElse view)
   10.12  {
   10.13    window =>
   10.14 @@ -70,7 +72,7 @@
   10.15    pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
   10.16    pretty_text_area.resize(Rendering.font_family(),
   10.17      Rendering.font_size("jedit_tooltip_font_scale").round)
   10.18 -  pretty_text_area.update(rendering.snapshot, body)
   10.19 +  pretty_text_area.update(rendering.snapshot, results, body)
   10.20  
   10.21    pretty_text_area.registerKeyboardAction(action_listener, "close_all",
   10.22      KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
   10.23 @@ -92,7 +94,9 @@
   10.24      tooltip = "Detach tooltip window"
   10.25      listenTo(mouse.clicks)
   10.26      reactions += {
   10.27 -      case _: MouseClicked => Info_Dockable(view, rendering.snapshot, body); window.dispose()
   10.28 +      case _: MouseClicked =>
   10.29 +        Info_Dockable(view, rendering.snapshot, results, body)
   10.30 +        window.dispose()
   10.31      }
   10.32    }
   10.33  
    11.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 13:52:18 2012 +0100
    11.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 17:29:23 2012 +0100
    11.3 @@ -254,16 +254,20 @@
    11.4  
    11.5    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
    11.6      snapshot.select_markup(range, Some(active_include), command_state =>
    11.7 -        {  // FIXME inactive dialog
    11.8 -          case Text.Info(info_range, elem @ XML.Elem(markup, _))
    11.9 -          if active_include(markup.name) => Text.Info(snapshot.convert(info_range), elem)
   11.10 +        {
   11.11 +          case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
   11.12 +          if !command_state.results.isDefinedAt(serial) =>
   11.13 +            Text.Info(snapshot.convert(info_range), elem)
   11.14 +          case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
   11.15 +          if name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
   11.16 +            Text.Info(snapshot.convert(info_range), elem)
   11.17          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   11.18  
   11.19  
   11.20    def tooltip_message(range: Text.Range): XML.Body =
   11.21    {
   11.22      val msgs =
   11.23 -      snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
   11.24 +      snapshot.cumulate_markup[Command.Results](range, Command.empty_results,
   11.25          Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
   11.26          {
   11.27            case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   11.28 @@ -433,12 +437,17 @@
   11.29                  (None, Some(bad_color))
   11.30                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   11.31                  (None, Some(intensify_color))
   11.32 -              case (_, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   11.33 -                command_state.results.get(serial) match {
   11.34 -                  case Some(Protocol.Dialog_Result(_, res)) if res == result =>
   11.35 -                    (None, Some(active_result_color))
   11.36 -                  case _ =>
   11.37 -                    (None, Some(active_color))
   11.38 +              case (acc, Text.Info(_, elem @ XML.Elem(Markup(Markup.DIALOG, _), _))) =>
   11.39 +                // FIXME pattern match problem in scala-2.9.2 (!??)
   11.40 +                elem match {
   11.41 +                  case Protocol.Dialog(_, serial, result) =>
   11.42 +                    command_state.results.get(serial) match {
   11.43 +                      case Some(Protocol.Dialog_Result(res)) if res == result =>
   11.44 +                        (None, Some(active_result_color))
   11.45 +                      case _ =>
   11.46 +                        (None, Some(active_color))
   11.47 +                    }
   11.48 +                  case _ => acc
   11.49                  }
   11.50                case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
   11.51                  (None, Some(active_color))
    12.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Dec 13 13:52:18 2012 +0100
    12.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Dec 13 17:29:23 2012 +0100
    12.3 @@ -204,13 +204,14 @@
    12.4            JEdit_Lib.pixel_range(text_area, x, y) match {
    12.5              case None =>
    12.6              case Some(range) =>
    12.7 +              // FIXME cumulate results!?
    12.8                val tip =
    12.9                  if (control) rendering.tooltip(range)
   12.10                  else rendering.tooltip_message(range)
   12.11                if (!tip.isEmpty) {
   12.12                  val painter = text_area.getPainter
   12.13                  val y1 = y + painter.getFontMetrics.getHeight / 2
   12.14 -                new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
   12.15 +                new Pretty_Tooltip(view, painter, rendering, x, y1, Command.empty_results, tip)
   12.16                }
   12.17            }
   12.18          }