somewhat more general JEdit_Lib;
authorwenzelm
Mon Sep 17 17:49:11 2012 +0200 (2012-09-17)
changeset 4940638db4832b210
parent 49405 2fc68b3787a8
child 49407 215ba6884bdf
somewhat more general JEdit_Lib;
tuned signatures;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/hyperlink.scala
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_thy_load.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/text_overview.scala
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Mon Sep 17 15:52:50 2012 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Sep 17 17:49:11 2012 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    "src/isabelle_options.scala"
     1.5    "src/isabelle_rendering.scala"
     1.6    "src/isabelle_sidekick.scala"
     1.7 +  "src/jedit_lib.scala"
     1.8    "src/jedit_thy_load.scala"
     1.9    "src/jedit_options.scala"
    1.10    "src/output_dockable.scala"
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Sep 17 15:52:50 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Sep 17 17:49:11 2012 +0200
     2.3 @@ -66,7 +66,7 @@
     2.4    def node_header(): Document.Node.Header =
     2.5    {
     2.6      Swing_Thread.require()
     2.7 -    Isabelle.buffer_lock(buffer) {
     2.8 +    JEdit_Lib.buffer_lock(buffer) {
     2.9        Exn.capture {
    2.10          Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
    2.11        } match {
    2.12 @@ -96,7 +96,7 @@
    2.13    /* point range */
    2.14  
    2.15    def point_range(offset: Text.Offset): Text.Range =
    2.16 -    Isabelle.buffer_lock(buffer) {
    2.17 +    JEdit_Lib.buffer_lock(buffer) {
    2.18        def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
    2.19        try {
    2.20          val c = text(offset)
    2.21 @@ -151,7 +151,7 @@
    2.22      def init()
    2.23      {
    2.24        flush()
    2.25 -      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
    2.26 +      session.init_node(name, node_header(), perspective(), JEdit_Lib.buffer_text(buffer))
    2.27      }
    2.28  
    2.29      def exit()
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 15:52:50 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 17:49:11 2012 +0200
     3.3 @@ -202,7 +202,7 @@
     3.4      override def mouseMoved(e: MouseEvent) {
     3.5        control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
     3.6        if (control && model.buffer.isLoaded) {
     3.7 -        Isabelle.buffer_lock(model.buffer) {
     3.8 +        JEdit_Lib.buffer_lock(model.buffer) {
     3.9            val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
    3.10            val mouse_range = model.point_range(text_area.xyToOffset(e.getX(), e.getY()))
    3.11            active_areas.foreach(_.update_rendering(rendering, mouse_range))
    3.12 @@ -248,7 +248,7 @@
    3.13          val FOLD_MARKER_SIZE = 12
    3.14  
    3.15          if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
    3.16 -          Isabelle.buffer_lock(model.buffer) {
    3.17 +          JEdit_Lib.buffer_lock(model.buffer) {
    3.18              val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
    3.19  
    3.20              for (i <- 0 until physical_lines.length) {
    3.21 @@ -308,7 +308,7 @@
    3.22          case changed: Session.Commands_Changed =>
    3.23            val buffer = model.buffer
    3.24            Swing_Thread.later {
    3.25 -            Isabelle.buffer_lock(buffer) {
    3.26 +            JEdit_Lib.buffer_lock(buffer) {
    3.27                if (model.buffer == text_area.getBuffer) {
    3.28                  val snapshot = model.snapshot()
    3.29  
     4.1 --- a/src/Tools/jEdit/src/hyperlink.scala	Mon Sep 17 15:52:50 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/hyperlink.scala	Mon Sep 17 17:49:11 2012 +0200
     4.3 @@ -31,7 +31,7 @@
     4.4    {
     4.5      Swing_Thread.require()
     4.6  
     4.7 -    Isabelle.jedit_buffer(jedit_file) match {
     4.8 +    JEdit_Lib.jedit_buffer(jedit_file) match {
     4.9        case Some(buffer) =>
    4.10          view.goToBuffer(buffer)
    4.11          val text_area = view.getTextArea
     5.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Sep 17 15:52:50 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Sep 17 17:49:11 2012 +0200
     5.3 @@ -14,6 +14,8 @@
     5.4  import java.io.{File => JFile}
     5.5  
     5.6  import org.gjt.sp.jedit.syntax.{Token => JEditToken}
     5.7 +import org.gjt.sp.jedit.GUIUtilities
     5.8 +import org.gjt.sp.util.Log
     5.9  
    5.10  import scala.collection.immutable.SortedMap
    5.11  
    5.12 @@ -24,17 +26,28 @@
    5.13      new Isabelle_Rendering(snapshot, options)
    5.14  
    5.15  
    5.16 -  /* physical rendering */
    5.17 +  /* message priorities */
    5.18  
    5.19    private val writeln_pri = 1
    5.20    private val warning_pri = 2
    5.21    private val legacy_pri = 3
    5.22    private val error_pri = 4
    5.23  
    5.24 +
    5.25 +  /* icons */
    5.26 +
    5.27 +  private def load_icon(name: String): Icon =
    5.28 +  {
    5.29 +    val icon = GUIUtilities.loadIcon(name)
    5.30 +    if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
    5.31 +      Log.log(Log.ERROR, icon, "Bad icon: " + name)
    5.32 +    icon
    5.33 +  }
    5.34 +
    5.35    private val gutter_icons = Map(
    5.36 -    warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
    5.37 -    legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
    5.38 -    error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
    5.39 +    warning_pri -> load_icon("16x16/status/dialog-information.png"),
    5.40 +    legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
    5.41 +    error_pri -> load_icon("16x16/status/dialog-error.png"))
    5.42  
    5.43  
    5.44    /* token markup -- text styles */
     6.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Sep 17 15:52:50 2012 +0200
     6.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Sep 17 17:49:11 2012 +0200
     6.3 @@ -91,7 +91,7 @@
     6.4      Swing_Thread.assert()
     6.5  
     6.6      val buffer = pane.getBuffer
     6.7 -    Isabelle.buffer_lock(buffer) {
     6.8 +    JEdit_Lib.buffer_lock(buffer) {
     6.9        get_syntax match {
    6.10          case None => null
    6.11          case Some(syntax) =>
    6.12 @@ -166,7 +166,7 @@
    6.13  
    6.14      node_name(buffer) match {
    6.15        case Some(name) =>
    6.16 -        val text = Isabelle.buffer_text(buffer)
    6.17 +        val text = JEdit_Lib.buffer_text(buffer)
    6.18          val structure = Structure.parse(syntax, name, text)
    6.19          make_tree(0, structure) foreach (node => data.root.add(node))
    6.20          true
    6.21 @@ -177,15 +177,15 @@
    6.22  
    6.23  
    6.24  class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
    6.25 -  "isabelle", Isabelle.get_recent_syntax, Isabelle.buffer_node_name)
    6.26 +  "isabelle", Isabelle.get_recent_syntax, JEdit_Lib.buffer_node_name)
    6.27  
    6.28  
    6.29  class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
    6.30 -  "isabelle-options", Some(Options.options_syntax), Isabelle.buffer_node_dummy)
    6.31 +  "isabelle-options", Some(Options.options_syntax), JEdit_Lib.buffer_node_dummy)
    6.32  
    6.33  
    6.34  class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
    6.35 -  "isabelle-root", Some(Build.root_syntax), Isabelle.buffer_node_dummy)
    6.36 +  "isabelle-root", Some(Build.root_syntax), JEdit_Lib.buffer_node_dummy)
    6.37  
    6.38  
    6.39  class Isabelle_Sidekick_Raw
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Sep 17 17:49:11 2012 +0200
     7.3 @@ -0,0 +1,64 @@
     7.4 +/*  Title:      Tools/jEdit/src/jedit_lib.scala
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Misc library functions for jEdit.
     7.8 +*/
     7.9 +
    7.10 +package isabelle.jedit
    7.11 +
    7.12 +
    7.13 +import isabelle._
    7.14 +
    7.15 +
    7.16 +import org.gjt.sp.jedit.{jEdit, Buffer, View}
    7.17 +import org.gjt.sp.jedit.buffer.JEditBuffer
    7.18 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    7.19 +
    7.20 +
    7.21 +object JEdit_Lib
    7.22 +{
    7.23 +  /* buffers */
    7.24 +
    7.25 +  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    7.26 +    Swing_Thread.now { buffer_lock(buffer) { body } }
    7.27 +
    7.28 +  def buffer_text(buffer: JEditBuffer): String =
    7.29 +    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    7.30 +
    7.31 +  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    7.32 +
    7.33 +  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
    7.34 +    Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
    7.35 +
    7.36 +  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
    7.37 +  {
    7.38 +    val name = buffer_name(buffer)
    7.39 +    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
    7.40 +  }
    7.41 +
    7.42 +
    7.43 +  /* main jEdit components */
    7.44 +
    7.45 +  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    7.46 +
    7.47 +  def jedit_buffer(name: String): Option[Buffer] =
    7.48 +    jedit_buffers().find(buffer => buffer_name(buffer) == name)
    7.49 +
    7.50 +  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    7.51 +
    7.52 +  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
    7.53 +    view.getEditPanes().iterator.map(_.getTextArea)
    7.54 +
    7.55 +  def jedit_text_areas(): Iterator[JEditTextArea] =
    7.56 +    jedit_views().flatMap(jedit_text_areas(_))
    7.57 +
    7.58 +  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
    7.59 +    jedit_text_areas().filter(_.getBuffer == buffer)
    7.60 +
    7.61 +  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    7.62 +  {
    7.63 +    try { buffer.readLock(); body }
    7.64 +    finally { buffer.readUnlock() }
    7.65 +  }
    7.66 +}
    7.67 +
     8.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Mon Sep 17 15:52:50 2012 +0200
     8.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Mon Sep 17 17:49:11 2012 +0200
     8.3 @@ -36,9 +36,9 @@
     8.4    override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
     8.5    {
     8.6      Swing_Thread.now {
     8.7 -      Isabelle.jedit_buffer(name.node) match {
     8.8 +      JEdit_Lib.jedit_buffer(name.node) match {
     8.9          case Some(buffer) =>
    8.10 -          Isabelle.buffer_lock(buffer) {
    8.11 +          JEdit_Lib.buffer_lock(buffer) {
    8.12              Some(f(buffer.getSegment(0, buffer.getLength)))
    8.13            }
    8.14          case None => None
     9.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 17 15:52:50 2012 +0200
     9.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 17 17:49:11 2012 +0200
     9.3 @@ -9,23 +9,17 @@
     9.4  
     9.5  import isabelle._
     9.6  
     9.7 -import java.lang.System
     9.8 -import java.awt.Font
     9.9  import javax.swing.JOptionPane
    9.10  
    9.11 -import scala.collection.mutable
    9.12  import scala.swing.{ListView, ScrollPane}
    9.13  
    9.14 -import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
    9.15 -  Buffer, EditPane, ServiceManager, View}
    9.16 -import org.gjt.sp.jedit.buffer.JEditBuffer
    9.17 +import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View}
    9.18  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    9.19  import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
    9.20  import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
    9.21  import org.gjt.sp.jedit.gui.DockableWindowManager
    9.22  
    9.23  import org.gjt.sp.util.SyntaxUtilities
    9.24 -import org.gjt.sp.util.Log
    9.25  
    9.26  import scala.actors.Actor._
    9.27  
    9.28 @@ -82,62 +76,6 @@
    9.29    }
    9.30  
    9.31  
    9.32 -  /* icons */
    9.33 -
    9.34 -  def load_icon(name: String): javax.swing.Icon =
    9.35 -  {
    9.36 -    val icon = GUIUtilities.loadIcon(name)
    9.37 -    if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
    9.38 -      Log.log(Log.ERROR, icon, "Bad icon: " + name)
    9.39 -    icon
    9.40 -  }
    9.41 -
    9.42 -
    9.43 -  /* buffers */
    9.44 -
    9.45 -  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    9.46 -    Swing_Thread.now { buffer_lock(buffer) { body } }
    9.47 -
    9.48 -  def buffer_text(buffer: JEditBuffer): String =
    9.49 -    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    9.50 -
    9.51 -  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    9.52 -
    9.53 -  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
    9.54 -    Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
    9.55 -
    9.56 -  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
    9.57 -  {
    9.58 -    val name = buffer_name(buffer)
    9.59 -    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
    9.60 -  }
    9.61 -
    9.62 -
    9.63 -  /* main jEdit components */
    9.64 -
    9.65 -  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    9.66 -
    9.67 -  def jedit_buffer(name: String): Option[Buffer] =
    9.68 -    jedit_buffers().find(buffer => buffer_name(buffer) == name)
    9.69 -
    9.70 -  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    9.71 -
    9.72 -  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
    9.73 -    view.getEditPanes().iterator.map(_.getTextArea)
    9.74 -
    9.75 -  def jedit_text_areas(): Iterator[JEditTextArea] =
    9.76 -    jedit_views().flatMap(jedit_text_areas(_))
    9.77 -
    9.78 -  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
    9.79 -    jedit_text_areas().filter(_.getBuffer == buffer)
    9.80 -
    9.81 -  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    9.82 -  {
    9.83 -    try { buffer.readLock(); body }
    9.84 -    finally { buffer.readUnlock() }
    9.85 -  }
    9.86 -
    9.87 -
    9.88    /* document model and view */
    9.89  
    9.90    def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
    9.91 @@ -145,24 +83,24 @@
    9.92  
    9.93    def document_views(buffer: Buffer): List[Document_View] =
    9.94      for {
    9.95 -      text_area <- jedit_text_areas(buffer).toList
    9.96 +      text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
    9.97        doc_view = document_view(text_area)
    9.98        if doc_view.isDefined
    9.99      } yield doc_view.get
   9.100  
   9.101    def exit_model(buffer: Buffer)
   9.102    {
   9.103 -    swing_buffer_lock(buffer) {
   9.104 -      jedit_text_areas(buffer).foreach(Document_View.exit)
   9.105 +    JEdit_Lib.swing_buffer_lock(buffer) {
   9.106 +      JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
   9.107        Document_Model.exit(buffer)
   9.108      }
   9.109    }
   9.110  
   9.111    def init_model(buffer: Buffer)
   9.112    {
   9.113 -    swing_buffer_lock(buffer) {
   9.114 +    JEdit_Lib.swing_buffer_lock(buffer) {
   9.115        val opt_model =
   9.116 -        buffer_node_name(buffer) match {
   9.117 +        JEdit_Lib.buffer_node_name(buffer) match {
   9.118            case Some(node_name) =>
   9.119              document_model(buffer) match {
   9.120                case Some(model) if model.name == node_name => Some(model)
   9.121 @@ -171,7 +109,7 @@
   9.122            case None => None
   9.123          }
   9.124        if (opt_model.isDefined) {
   9.125 -        for (text_area <- jedit_text_areas(buffer)) {
   9.126 +        for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
   9.127            if (document_view(text_area).map(_.model) != opt_model)
   9.128              Document_View.init(opt_model.get, text_area)
   9.129          }
   9.130 @@ -181,7 +119,7 @@
   9.131  
   9.132    def init_view(buffer: Buffer, text_area: JEditTextArea)
   9.133    {
   9.134 -    swing_buffer_lock(buffer) {
   9.135 +    JEdit_Lib.swing_buffer_lock(buffer) {
   9.136        document_model(buffer) match {
   9.137          case Some(model) => Document_View.init(model, text_area)
   9.138          case None =>
   9.139 @@ -191,7 +129,7 @@
   9.140  
   9.141    def exit_view(buffer: Buffer, text_area: JEditTextArea)
   9.142    {
   9.143 -    swing_buffer_lock(buffer) {
   9.144 +    JEdit_Lib.swing_buffer_lock(buffer) {
   9.145        Document_View.exit(text_area)
   9.146      }
   9.147    }
   9.148 @@ -264,10 +202,10 @@
   9.149      {
   9.150        val view = jEdit.getActiveView()
   9.151  
   9.152 -      val buffers = Isabelle.jedit_buffers().toList
   9.153 +      val buffers = JEdit_Lib.jedit_buffers().toList
   9.154        if (buffers.forall(_.isLoaded)) {
   9.155          def loaded_buffer(name: String): Boolean =
   9.156 -          buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
   9.157 +          buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
   9.158  
   9.159          val thys =
   9.160            for (buffer <- buffers; model <- Isabelle.document_model(buffer))
   9.161 @@ -314,16 +252,16 @@
   9.162                }
   9.163  
   9.164              case Session.Ready =>
   9.165 -              Isabelle.jedit_buffers.foreach(Isabelle.init_model)
   9.166 +              JEdit_Lib.jedit_buffers.foreach(Isabelle.init_model)
   9.167                Swing_Thread.later { delay_load.invoke() }
   9.168  
   9.169              case Session.Shutdown =>
   9.170 -              Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
   9.171 +              JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
   9.172                Swing_Thread.later { delay_load.revoke() }
   9.173  
   9.174              case _ =>
   9.175            }
   9.176 -        case bad => System.err.println("session_manager: ignoring bad message " + bad)
   9.177 +        case bad => java.lang.System.err.println("session_manager: ignoring bad message " + bad)
   9.178        }
   9.179      }
   9.180    }
   9.181 @@ -426,7 +364,7 @@
   9.182        Isabelle.options.value.save_prefs()
   9.183  
   9.184      Isabelle.session.phase_changed -= session_manager
   9.185 -    Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
   9.186 +    JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
   9.187      Isabelle.session.stop()
   9.188    }
   9.189  }
    10.1 --- a/src/Tools/jEdit/src/text_overview.scala	Mon Sep 17 15:52:50 2012 +0200
    10.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Mon Sep 17 17:49:11 2012 +0200
    10.3 @@ -66,7 +66,7 @@
    10.4      Swing_Thread.assert()
    10.5  
    10.6      doc_view.robust_body(()) {
    10.7 -      Isabelle.buffer_lock(buffer) {
    10.8 +      JEdit_Lib.buffer_lock(buffer) {
    10.9          val snapshot = doc_view.model.snapshot()
   10.10  
   10.11          if (snapshot.is_outdated) {