# HG changeset patch # User wenzelm # Date 1355416163 -3600 # Node ID 6f41f1646617c7b1a30ca8d1407f5fe31c473cf1 # Parent c94bba7906d23915651e3770bde793ed83fda647 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; diff -r c94bba7906d2 -r 6f41f1646617 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Pure/PIDE/command.scala Thu Dec 13 17:29:23 2012 +0100 @@ -17,11 +17,14 @@ { /** accumulated results from prover **/ + type Results = SortedMap[Long, XML.Tree] + val empty_results: Results = SortedMap.empty + sealed case class State( - val command: Command, - val status: List[Markup] = Nil, - val results: SortedMap[Long, XML.Tree] = SortedMap.empty, - val markup: Markup_Tree = Markup_Tree.empty) + command: Command, + status: List[Markup] = Nil, + results: Results = empty_results, + markup: Markup_Tree = Markup_Tree.empty) { def markup_to_XML(filter: XML.Elem => Boolean): XML.Body = markup.to_XML(command.range, command.source, filter) @@ -89,8 +92,8 @@ type Span = List[Token] - def apply(id: Document.Command_ID, node_name: Document.Node.Name, - span: Span, markup: Markup_Tree): Command = + def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span, + results: Results = empty_results, markup: Markup_Tree = Markup_Tree.empty): Command = { val source: String = span match { @@ -107,21 +110,23 @@ i += n } - new Command(id, node_name, span1.toList, source, markup) + new Command(id, node_name, span1.toList, source, results, markup) } - val empty = Command(Document.no_id, Document.Node.Name.empty, Nil, Markup_Tree.empty) + val empty = Command(Document.no_id, Document.Node.Name.empty, Nil) - def unparsed(id: Document.Command_ID, source: String, markup: Markup_Tree): Command = - Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), markup) + def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree) + : Command = + Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup) - def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty) + def unparsed(source: String): Command = + unparsed(Document.no_id, source, empty_results, Markup_Tree.empty) - def rich_text(id: Document.Command_ID, body: XML.Body): Command = + def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command = { val text = XML.content(body) val markup = Markup_Tree.from_XML(body) - unparsed(id, text, markup) + unparsed(id, text, results, markup) } @@ -152,6 +157,7 @@ val node_name: Document.Node.Name, val span: Command.Span, val source: String, + val init_results: Command.Results, val init_markup: Markup_Tree) { /* classification */ @@ -188,5 +194,6 @@ /* accumulated results */ - val init_state: Command.State = Command.State(this, markup = init_markup) + val init_state: Command.State = + Command.State(this, results = init_results, markup = init_markup) } diff -r c94bba7906d2 -r 6f41f1646617 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Pure/PIDE/markup.scala Thu Dec 13 17:29:23 2012 +0100 @@ -264,8 +264,7 @@ val message: String => String = Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE, - WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE) - .withDefault((name: String) => name + "_message") + WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE).withDefault((s: String) => s) val Return_Code = new Properties.Int("return_code") diff -r c94bba7906d2 -r 6f41f1646617 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Pure/PIDE/protocol.scala Thu Dec 13 17:29:23 2012 +0100 @@ -209,13 +209,15 @@ object Dialog_Result { - def apply(serial: Long, result: String): XML.Elem = - XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result))) + def apply(id: Document.ID, serial: Long, result: String): XML.Elem = + { + val props = Position.Id(id) ::: Markup.Serial(serial) + XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result))) + } - def unapply(tree: XML.Tree): Option[(Long, String)] = + def unapply(tree: XML.Tree): Option[String] = tree match { - case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result))) => - Some((serial, result)) + case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result) case _ => None } } diff -r c94bba7906d2 -r 6f41f1646617 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Pure/System/session.scala Thu Dec 13 17:29:23 2012 +0100 @@ -422,7 +422,7 @@ case Session.Dialog_Result(id, serial, result) if prover.isDefined => prover.get.dialog_result(serial, result) - handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(serial, result))) + handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result))) case Messages(msgs) => msgs foreach { diff -r c94bba7906d2 -r 6f41f1646617 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Thu Dec 13 17:29:23 2012 +0100 @@ -68,7 +68,7 @@ /* result structure */ val spans = parse_spans(syntax.scan(text)) - spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty))) + spans.foreach(span => add(Command(Document.no_id, node_name, span))) result() } } @@ -226,7 +226,7 @@ commands case cmd :: _ => val hook = commands.prev(cmd) - val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty)) + val inserted = spans2.map(span => Command(Document.new_id(), name, span)) (commands /: cmds2)(_ - _).append_after(hook, inserted) } } diff -r c94bba7906d2 -r 6f41f1646617 src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Thu Dec 13 17:29:23 2012 +0100 @@ -65,7 +65,7 @@ override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = { val rendering = Rendering(snapshot, PIDE.options.value) - new Pretty_Tooltip(view, parent, rendering, x, y, body) + new Pretty_Tooltip(view, parent, rendering, x, y, Command.empty_results, body) null } } diff -r c94bba7906d2 -r 6f41f1646617 src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Tools/jEdit/src/info_dockable.scala Thu Dec 13 17:29:23 2012 +0100 @@ -26,22 +26,24 @@ /* implicit arguments -- owned by Swing thread */ private var implicit_snapshot = Document.State.init.snapshot() + private var implicit_results = Command.empty_results private var implicit_info: XML.Body = Nil - private def set_implicit(snapshot: Document.Snapshot, info: XML.Body) + private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body) { Swing_Thread.require() implicit_snapshot = snapshot + implicit_results = results implicit_info = info } private def reset_implicit(): Unit = - set_implicit(Document.State.init.snapshot(), Nil) + set_implicit(Document.State.init.snapshot(), Command.empty_results, Nil) - def apply(view: View, snapshot: Document.Snapshot, info: XML.Body) + def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body) { - set_implicit(snapshot, info) + set_implicit(snapshot, results, info) view.getDockableWindowManager.floatDockableWindow("isabelle-info") } } @@ -57,11 +59,12 @@ private var zoom_factor = 100 private val snapshot = Info_Dockable.implicit_snapshot + private val results = Info_Dockable.implicit_results private val info = Info_Dockable.implicit_info private val window_focus_listener = new WindowFocusListener { - def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, info) } + def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, results, info) } def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() } } @@ -71,7 +74,7 @@ private val pretty_text_area = new Pretty_Text_Area(view) set_content(pretty_text_area) - pretty_text_area.update(snapshot, info) + pretty_text_area.update(snapshot, results, info) private def handle_resize() { diff -r c94bba7906d2 -r 6f41f1646617 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Tools/jEdit/src/output_dockable.scala Thu Dec 13 17:29:23 2012 +0100 @@ -77,7 +77,7 @@ else current_output if (new_output != current_output) - pretty_text_area.update(new_snapshot, Pretty.separate(new_output)) + pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output)) current_snapshot = new_snapshot current_state = new_state @@ -152,7 +152,8 @@ private val detach = new Button("Detach") { reactions += { case ButtonClicked(_) => - Info_Dockable(view, current_snapshot, Pretty.separate(current_output)) + Info_Dockable(view, current_snapshot, + current_state.results, Pretty.separate(current_output)) } } detach.tooltip = "Detach window with static copy of current output" diff -r c94bba7906d2 -r 6f41f1646617 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Dec 13 17:29:23 2012 +0100 @@ -21,18 +21,18 @@ object Pretty_Text_Area { - private def text_rendering(base_snapshot: Document.Snapshot, formatted_body: XML.Body): - (String, Rendering) = + private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results, + formatted_body: XML.Body): (String, Rendering) = { - val (text, state) = Pretty_Text_Area.document_state(base_snapshot, formatted_body) + val (text, state) = Pretty_Text_Area.document_state(base_snapshot, base_results, formatted_body) val rendering = Rendering(state.snapshot(), PIDE.options.value) (text, rendering) } - private def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body) - : (String, Document.State) = + private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results, + formatted_body: XML.Body): (String, Document.State) = { - val command = Command.rich_text(Document.new_id(), formatted_body) + val command = Command.rich_text(Document.new_id(), base_results, formatted_body) val node_name = command.node_name val edits: List[Document.Edit_Text] = List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source)))) @@ -62,8 +62,9 @@ private var current_font_size: Int = 12 private var current_body: XML.Body = Nil private var current_base_snapshot = Document.State.init.snapshot() + private var current_base_results = Command.empty_results private var current_rendering: Rendering = - Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2 + Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2 private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None private val rich_text_area = @@ -84,12 +85,14 @@ val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20 val base_snapshot = current_base_snapshot + val base_results = current_base_results val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics)) future_rendering.map(_.cancel(true)) future_rendering = Some(default_thread_pool.submit(() => { - val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body) + val (text, rendering) = + Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) Simple_Thread.interrupted_exception() Swing_Thread.later { @@ -115,12 +118,13 @@ refresh() } - def update(base_snapshot: Document.Snapshot, body: XML.Body) + def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body) { Swing_Thread.require() require(!base_snapshot.is_outdated) current_base_snapshot = base_snapshot + current_base_results = base_results current_body = body refresh() } diff -r c94bba7906d2 -r 6f41f1646617 src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Thu Dec 13 17:29:23 2012 +0100 @@ -25,7 +25,9 @@ view: View, parent: JComponent, rendering: Rendering, - mouse_x: Int, mouse_y: Int, body: XML.Body) + mouse_x: Int, mouse_y: Int, + results: Command.Results, + body: XML.Body) extends JWindow(JEdit_Lib.parent_window(parent) getOrElse view) { window => @@ -70,7 +72,7 @@ pretty_text_area.getPainter.setBackground(rendering.tooltip_color) pretty_text_area.resize(Rendering.font_family(), Rendering.font_size("jedit_tooltip_font_scale").round) - pretty_text_area.update(rendering.snapshot, body) + pretty_text_area.update(rendering.snapshot, results, body) pretty_text_area.registerKeyboardAction(action_listener, "close_all", KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED) @@ -92,7 +94,9 @@ tooltip = "Detach tooltip window" listenTo(mouse.clicks) reactions += { - case _: MouseClicked => Info_Dockable(view, rendering.snapshot, body); window.dispose() + case _: MouseClicked => + Info_Dockable(view, rendering.snapshot, results, body) + window.dispose() } } diff -r c94bba7906d2 -r 6f41f1646617 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Thu Dec 13 17:29:23 2012 +0100 @@ -254,16 +254,20 @@ def active(range: Text.Range): Option[Text.Info[XML.Elem]] = snapshot.select_markup(range, Some(active_include), command_state => - { // FIXME inactive dialog - case Text.Info(info_range, elem @ XML.Elem(markup, _)) - if active_include(markup.name) => Text.Info(snapshot.convert(info_range), elem) + { + case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _)) + if !command_state.results.isDefinedAt(serial) => + Text.Info(snapshot.convert(info_range), elem) + case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _)) + if name == Markup.GRAPHVIEW || name == Markup.SENDBACK => + Text.Info(snapshot.convert(info_range), elem) }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None } def tooltip_message(range: Text.Range): XML.Body = { val msgs = - snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty, + snapshot.cumulate_markup[Command.Results](range, Command.empty_results, Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ => { case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) @@ -433,12 +437,17 @@ (None, Some(bad_color)) case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => (None, Some(intensify_color)) - case (_, Text.Info(_, Protocol.Dialog(_, serial, result))) => - command_state.results.get(serial) match { - case Some(Protocol.Dialog_Result(_, res)) if res == result => - (None, Some(active_result_color)) - case _ => - (None, Some(active_color)) + case (acc, Text.Info(_, elem @ XML.Elem(Markup(Markup.DIALOG, _), _))) => + // FIXME pattern match problem in scala-2.9.2 (!??) + elem match { + case Protocol.Dialog(_, serial, result) => + command_state.results.get(serial) match { + case Some(Protocol.Dialog_Result(res)) if res == result => + (None, Some(active_result_color)) + case _ => + (None, Some(active_color)) + } + case _ => acc } case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) => (None, Some(active_color)) diff -r c94bba7906d2 -r 6f41f1646617 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Thu Dec 13 13:52:18 2012 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Dec 13 17:29:23 2012 +0100 @@ -204,13 +204,14 @@ JEdit_Lib.pixel_range(text_area, x, y) match { case None => case Some(range) => + // FIXME cumulate results!? val tip = if (control) rendering.tooltip(range) else rendering.tooltip_message(range) if (!tip.isEmpty) { val painter = text_area.getPainter val y1 = y + painter.getFontMetrics.getHeight / 2 - new Pretty_Tooltip(view, painter, rendering, x, y1, tip) + new Pretty_Tooltip(view, painter, rendering, x, y1, Command.empty_results, tip) } } }