Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: simplifier_trace_dockable.scala Sprache: Scala

Original von: Isabelle^©

/*  Title:      Tools/jEdit/src/simplifier_trace_dockable.scala
    Author:     Lars Hupel

Dockable window with interactive simplifier trace.
*/

package isabelle.jedit

import isabelle._
import isabelle.jedit_base.Dockable

import scala.swing.{Button, CheckBox, Orientation, Separator}
import scala.swing.event.ButtonClicked

import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}

import org.gjt.sp.jedit.View

class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
{
  GUI_Thread.require {}

  /* component state -- owned by GUI thread */

  private var current_snapshot = Document.State.init.snapshot()
  private var current_command = Command.empty
  private var current_results = Command.Results.empty
  private var current_id = 0L
  private var do_update = true

  private val text_area = new Pretty_Text_Area(view)
  set_content(text_area)

  private def update_contents()
  {
    val snapshot = current_snapshot
    val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)

    answers.contents.clear()
    context.questions.values.toList match {
      case q :: _ =>
        val data = q.data
        val content = Pretty.separate(XML.Text(data.text) :: data.content)
        text_area.update(snapshot, Command.Results.empty, content)
        q.answers.foreach { answer =>
          answers.contents += new Button(answer.string) {
            reactions += {
              case ButtonClicked(_) =>
                Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
            }
          }
        }
      case Nil =>
        text_area.update(snapshot, Command.Results.empty, Nil)
    }

    do_paint()
  }

  private def show_trace()
  {
    val trace = Simplifier_Trace.generate_trace(PIDE.session, current_results)
    new Simplifier_Trace_Window(view, current_snapshot, trace)
  }

  private def do_paint()
  {
    GUI_Thread.later {
      text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
    }
  }

  private def handle_resize()
  {
    do_paint()
  }

  private def handle_update(follow: Boolean)
  {
    val (new_snapshot, new_command, new_results, new_id) =
      PIDE.editor.current_node_snapshot(view) match {
        case Some(snapshot) =>
          if (follow && !snapshot.is_outdated) {
            PIDE.editor.current_command(view, snapshot) match {
              case Some(cmd) =>
                (snapshot, cmd, snapshot.command_results(cmd), cmd.id)
              case None =>
                (Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L)
            }
          }
          else (current_snapshot, current_command, current_results, current_id)
        case None => (current_snapshot, current_command, current_results, current_id)
      }

    current_snapshot = new_snapshot
    current_command = new_command
    current_results = new_results
    current_id = new_id
    update_contents()
  }

  /* main */

  private val main =
    Session.Consumer[Any](getClass.getName) {
      case _: Session.Global_Options =>
        GUI_Thread.later { handle_resize() }

      case changed: Session.Commands_Changed =>
        GUI_Thread.later { handle_update(do_update) }

      case Session.Caret_Focus =>
        GUI_Thread.later { handle_update(do_update) }

      case Simplifier_Trace.Event =>
        GUI_Thread.later { handle_update(do_update) }
    }

  override def init()
  {
    PIDE.session.global_options += main
    PIDE.session.commands_changed += main
    PIDE.session.caret_focus += main
    PIDE.session.trace_events += main
    handle_update(true)
  }

  override def exit()
  {
    PIDE.session.global_options -= main
    PIDE.session.commands_changed -= main
    PIDE.session.caret_focus -= main
    PIDE.session.trace_events -= main
    delay_resize.revoke()
  }

  /* resize */

  private val delay_resize =
    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }

  addComponentListener(new ComponentAdapter {
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
  })

  /* controls */

  private val controls =
    Wrap_Panel(
      List(
        new CheckBox("Auto update") {
          selected = do_update
          reactions += {
            case ButtonClicked(_) =>
              do_update = this.selected
              handle_update(do_update)
          }
        },
        new Button("Update") {
          reactions += {
            case ButtonClicked(_) =>
              handle_update(true)
          }
        },
        new Separator(Orientation.Vertical),
        new Button("Show trace") {
          reactions += {
            case ButtonClicked(_) =>
              show_trace()
          }
        },
        new Button("Clear memory") {
          reactions += {
            case ButtonClicked(_) =>
              Simplifier_Trace.clear_memory(PIDE.session)
          }
        }))

  private val answers = Wrap_Panel(Nil, Wrap_Panel.Alignment.Left)

  add(controls.peer, BorderLayout.NORTH)
  add(answers.peer, BorderLayout.SOUTH)
}

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.