src/Tools/jEdit/src/simplifier_trace_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56770 e160ae47db94
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
     1 /*  Title:      Tools/jEdit/src/simplifier_trace_dockable.scala
     2     Author:     Lars Hupel
     3 
     4 Dockable window with interactive simplifier trace.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import scala.swing.{Button, CheckBox, Orientation, Separator}
    13 import scala.swing.event.ButtonClicked
    14 
    15 import java.awt.BorderLayout
    16 import java.awt.event.{ComponentEvent, ComponentAdapter}
    17 
    18 import org.gjt.sp.jedit.View
    19 
    20 
    21 class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
    22 {
    23   Swing_Thread.require {}
    24 
    25   /* component state -- owned by Swing thread */
    26 
    27   private var current_snapshot = Document.State.init.snapshot()
    28   private var current_command = Command.empty
    29   private var current_results = Command.Results.empty
    30   private var current_id = 0L
    31   private var do_update = true
    32   private var do_auto_reply = false
    33 
    34 
    35   private val text_area = new Pretty_Text_Area(view)
    36   set_content(text_area)
    37 
    38   private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.Tree =
    39   {
    40     val data = question.data
    41 
    42     def make_button(answer: Simplifier_Trace.Answer): XML.Tree =
    43       XML.Wrapped_Elem(
    44         Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)),
    45         Nil,
    46         List(XML.Text(answer.string))
    47       )
    48 
    49     def make_block(body: XML.Body): XML.Body =
    50       List(Pretty.Block(0, body))
    51 
    52     val all = Pretty.separate(
    53       XML.Text(data.text) ::
    54       data.content :::
    55       make_block(Library.separate(XML.Text(", "), question.answers map make_button))
    56     )
    57 
    58     XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(all)))
    59   }
    60 
    61   private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
    62   {
    63     Swing_Thread.require {}
    64     val questions = context.questions.values
    65     if (do_auto_reply && !questions.isEmpty)
    66     {
    67       questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer))
    68       handle_update(do_update)
    69     }
    70     else
    71     {
    72       val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut))
    73       text_area.update(snapshot, Command.Results.empty, contents)
    74       do_paint()
    75     }
    76   }
    77 
    78   private def show_trace()
    79   {
    80     val trace = Simplifier_Trace.generate_trace(current_results)
    81     new Simplifier_Trace_Window(view, current_snapshot, trace)
    82   }
    83 
    84   private def do_paint()
    85   {
    86     Swing_Thread.later {
    87       text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
    88     }
    89   }
    90 
    91   private def update_contents()
    92   {
    93     set_context(
    94       current_snapshot,
    95       Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
    96     )
    97   }
    98 
    99   private def handle_resize()
   100   {
   101     do_paint()
   102   }
   103 
   104   private def handle_update(follow: Boolean)
   105   {
   106     val (new_snapshot, new_command, new_results, new_id) =
   107       PIDE.editor.current_node_snapshot(view) match {
   108         case Some(snapshot) =>
   109           if (follow && !snapshot.is_outdated) {
   110             PIDE.editor.current_command(view, snapshot) match {
   111               case Some(cmd) =>
   112                 (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd), cmd.id)
   113               case None =>
   114                 (Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L)
   115             }
   116           }
   117           else (current_snapshot, current_command, current_results, current_id)
   118         case None => (current_snapshot, current_command, current_results, current_id)
   119       }
   120 
   121     current_snapshot = new_snapshot
   122     current_command = new_command
   123     current_results = new_results
   124     current_id = new_id
   125     update_contents()
   126   }
   127 
   128 
   129   /* main */
   130 
   131   private val main =
   132     Session.Consumer[Any](getClass.getName) {
   133       case _: Session.Global_Options =>
   134         Swing_Thread.later { handle_resize() }
   135 
   136       case changed: Session.Commands_Changed =>
   137         Swing_Thread.later { handle_update(do_update) }
   138 
   139       case Session.Caret_Focus =>
   140         Swing_Thread.later { handle_update(do_update) }
   141 
   142       case Simplifier_Trace.Event =>
   143         Swing_Thread.later { handle_update(do_update) }
   144     }
   145 
   146   override def init()
   147   {
   148     Swing_Thread.require {}
   149 
   150     PIDE.session.global_options += main
   151     PIDE.session.commands_changed += main
   152     PIDE.session.caret_focus += main
   153     PIDE.session.trace_events += main
   154     handle_update(true)
   155   }
   156 
   157   override def exit()
   158   {
   159     Swing_Thread.require {}
   160 
   161     PIDE.session.global_options -= main
   162     PIDE.session.commands_changed -= main
   163     PIDE.session.caret_focus -= main
   164     PIDE.session.trace_events -= main
   165     delay_resize.revoke()
   166   }
   167 
   168 
   169   /* resize */
   170 
   171   private val delay_resize =
   172     Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   173 
   174   addComponentListener(new ComponentAdapter {
   175     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   176     override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
   177   })
   178 
   179 
   180   /* controls */
   181 
   182   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
   183     new CheckBox("Auto update") {
   184       selected = do_update
   185       reactions += {
   186         case ButtonClicked(_) =>
   187           do_update = this.selected
   188           handle_update(do_update)
   189       }
   190     },
   191     new Button("Update") {
   192       reactions += {
   193         case ButtonClicked(_) =>
   194           handle_update(true)
   195       }
   196     },
   197     new Separator(Orientation.Vertical),
   198     new CheckBox("Auto reply") {
   199       selected = do_auto_reply
   200       reactions += {
   201         case ButtonClicked(_) =>
   202           do_auto_reply = this.selected
   203           handle_update(do_update)
   204       }
   205     },
   206     new Separator(Orientation.Vertical),
   207     new Button("Show trace") {
   208       reactions += {
   209         case ButtonClicked(_) =>
   210           show_trace()
   211       }
   212     },
   213     new Button("Clear memory") {
   214       reactions += {
   215         case ButtonClicked(_) =>
   216           Simplifier_Trace.clear_memory()
   217       }
   218     }
   219   )
   220 
   221   add(controls.peer, BorderLayout.NORTH)
   222 }