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