src/Tools/jEdit/src/simplifier_trace_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 60748 6d718fda8215
child 65195 ffab6f460a82
permissions -rw-r--r--
tuned signature;
     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   GUI_Thread.require {}
    24 
    25 
    26   /* component state -- owned by GUI thread */
    27 
    28   private var current_snapshot = Document.State.init.snapshot()
    29   private var current_command = Command.empty
    30   private var current_results = Command.Results.empty
    31   private var current_id = 0L
    32   private var do_update = true
    33 
    34 
    35   private val text_area = new Pretty_Text_Area(view)
    36   set_content(text_area)
    37 
    38   private def update_contents()
    39   {
    40     val snapshot = current_snapshot
    41     val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
    42 
    43     answers.contents.clear()
    44     context.questions.values.toList match {
    45       case q :: _ =>
    46         val data = q.data
    47         val content = Pretty.separate(XML.Text(data.text) :: data.content)
    48         text_area.update(snapshot, Command.Results.empty, content)
    49         q.answers.foreach { answer =>
    50           answers.contents += new Button(answer.string) {
    51             reactions += {
    52               case ButtonClicked(_) =>
    53                 Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
    54             }
    55           }
    56         }
    57       case Nil =>
    58         text_area.update(snapshot, Command.Results.empty, Nil)
    59     }
    60 
    61     do_paint()
    62   }
    63 
    64   private def show_trace()
    65   {
    66     val trace = Simplifier_Trace.generate_trace(current_results)
    67     new Simplifier_Trace_Window(view, current_snapshot, trace)
    68   }
    69 
    70   private def do_paint()
    71   {
    72     GUI_Thread.later {
    73       text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
    74     }
    75   }
    76 
    77   private def handle_resize()
    78   {
    79     do_paint()
    80   }
    81 
    82   private def handle_update(follow: Boolean)
    83   {
    84     val (new_snapshot, new_command, new_results, new_id) =
    85       PIDE.editor.current_node_snapshot(view) match {
    86         case Some(snapshot) =>
    87           if (follow && !snapshot.is_outdated) {
    88             PIDE.editor.current_command(view, snapshot) match {
    89               case Some(cmd) =>
    90                 (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd), cmd.id)
    91               case None =>
    92                 (Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L)
    93             }
    94           }
    95           else (current_snapshot, current_command, current_results, current_id)
    96         case None => (current_snapshot, current_command, current_results, current_id)
    97       }
    98 
    99     current_snapshot = new_snapshot
   100     current_command = new_command
   101     current_results = new_results
   102     current_id = new_id
   103     update_contents()
   104   }
   105 
   106 
   107   /* main */
   108 
   109   private val main =
   110     Session.Consumer[Any](getClass.getName) {
   111       case _: Session.Global_Options =>
   112         GUI_Thread.later { handle_resize() }
   113 
   114       case changed: Session.Commands_Changed =>
   115         GUI_Thread.later { handle_update(do_update) }
   116 
   117       case Session.Caret_Focus =>
   118         GUI_Thread.later { handle_update(do_update) }
   119 
   120       case Simplifier_Trace.Event =>
   121         GUI_Thread.later { handle_update(do_update) }
   122     }
   123 
   124   override def init()
   125   {
   126     PIDE.session.global_options += main
   127     PIDE.session.commands_changed += main
   128     PIDE.session.caret_focus += main
   129     PIDE.session.trace_events += main
   130     handle_update(true)
   131   }
   132 
   133   override def exit()
   134   {
   135     PIDE.session.global_options -= main
   136     PIDE.session.commands_changed -= main
   137     PIDE.session.caret_focus -= main
   138     PIDE.session.trace_events -= main
   139     delay_resize.revoke()
   140   }
   141 
   142 
   143   /* resize */
   144 
   145   private val delay_resize =
   146     GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   147 
   148   addComponentListener(new ComponentAdapter {
   149     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   150     override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   151   })
   152 
   153 
   154   /* controls */
   155 
   156   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
   157     new CheckBox("Auto update") {
   158       selected = do_update
   159       reactions += {
   160         case ButtonClicked(_) =>
   161           do_update = this.selected
   162           handle_update(do_update)
   163       }
   164     },
   165     new Button("Update") {
   166       reactions += {
   167         case ButtonClicked(_) =>
   168           handle_update(true)
   169       }
   170     },
   171     new Separator(Orientation.Vertical),
   172     new Button("Show trace") {
   173       reactions += {
   174         case ButtonClicked(_) =>
   175           show_trace()
   176       }
   177     },
   178     new Button("Clear memory") {
   179       reactions += {
   180         case ButtonClicked(_) =>
   181           Simplifier_Trace.clear_memory()
   182       }
   183     }
   184   )
   185 
   186   private val answers = new Wrap_Panel(Wrap_Panel.Alignment.Left)()
   187 
   188   add(controls.peer, BorderLayout.NORTH)
   189   add(answers.peer, BorderLayout.SOUTH)
   190 }