--- a/src/Tools/jEdit/lib/Tools/jedit Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Sep 17 17:49:11 2012 +0200
@@ -18,6 +18,7 @@
"src/isabelle_options.scala"
"src/isabelle_rendering.scala"
"src/isabelle_sidekick.scala"
+ "src/jedit_lib.scala"
"src/jedit_thy_load.scala"
"src/jedit_options.scala"
"src/output_dockable.scala"
--- a/src/Tools/jEdit/src/document_model.scala Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Sep 17 17:49:11 2012 +0200
@@ -66,7 +66,7 @@
def node_header(): Document.Node.Header =
{
Swing_Thread.require()
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
Exn.capture {
Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
} match {
@@ -96,7 +96,7 @@
/* point range */
def point_range(offset: Text.Offset): Text.Range =
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
try {
val c = text(offset)
@@ -151,7 +151,7 @@
def init()
{
flush()
- session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
+ session.init_node(name, node_header(), perspective(), JEdit_Lib.buffer_text(buffer))
}
def exit()
--- a/src/Tools/jEdit/src/document_view.scala Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Mon Sep 17 17:49:11 2012 +0200
@@ -202,7 +202,7 @@
override def mouseMoved(e: MouseEvent) {
control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
if (control && model.buffer.isLoaded) {
- Isabelle.buffer_lock(model.buffer) {
+ JEdit_Lib.buffer_lock(model.buffer) {
val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
val mouse_range = model.point_range(text_area.xyToOffset(e.getX(), e.getY()))
active_areas.foreach(_.update_rendering(rendering, mouse_range))
@@ -248,7 +248,7 @@
val FOLD_MARKER_SIZE = 12
if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
- Isabelle.buffer_lock(model.buffer) {
+ JEdit_Lib.buffer_lock(model.buffer) {
val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
for (i <- 0 until physical_lines.length) {
@@ -308,7 +308,7 @@
case changed: Session.Commands_Changed =>
val buffer = model.buffer
Swing_Thread.later {
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
if (model.buffer == text_area.getBuffer) {
val snapshot = model.snapshot()
--- a/src/Tools/jEdit/src/hyperlink.scala Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/src/hyperlink.scala Mon Sep 17 17:49:11 2012 +0200
@@ -31,7 +31,7 @@
{
Swing_Thread.require()
- Isabelle.jedit_buffer(jedit_file) match {
+ JEdit_Lib.jedit_buffer(jedit_file) match {
case Some(buffer) =>
view.goToBuffer(buffer)
val text_area = view.getTextArea
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Mon Sep 17 17:49:11 2012 +0200
@@ -14,6 +14,8 @@
import java.io.{File => JFile}
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
+import org.gjt.sp.jedit.GUIUtilities
+import org.gjt.sp.util.Log
import scala.collection.immutable.SortedMap
@@ -24,17 +26,28 @@
new Isabelle_Rendering(snapshot, options)
- /* physical rendering */
+ /* message priorities */
private val writeln_pri = 1
private val warning_pri = 2
private val legacy_pri = 3
private val error_pri = 4
+
+ /* icons */
+
+ private def load_icon(name: String): Icon =
+ {
+ val icon = GUIUtilities.loadIcon(name)
+ if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
+ Log.log(Log.ERROR, icon, "Bad icon: " + name)
+ icon
+ }
+
private val gutter_icons = Map(
- warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
- legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
- error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
+ warning_pri -> load_icon("16x16/status/dialog-information.png"),
+ legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
+ error_pri -> load_icon("16x16/status/dialog-error.png"))
/* token markup -- text styles */
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Sep 17 17:49:11 2012 +0200
@@ -91,7 +91,7 @@
Swing_Thread.assert()
val buffer = pane.getBuffer
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
get_syntax match {
case None => null
case Some(syntax) =>
@@ -166,7 +166,7 @@
node_name(buffer) match {
case Some(name) =>
- val text = Isabelle.buffer_text(buffer)
+ val text = JEdit_Lib.buffer_text(buffer)
val structure = Structure.parse(syntax, name, text)
make_tree(0, structure) foreach (node => data.root.add(node))
true
@@ -177,15 +177,15 @@
class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
- "isabelle", Isabelle.get_recent_syntax, Isabelle.buffer_node_name)
+ "isabelle", Isabelle.get_recent_syntax, JEdit_Lib.buffer_node_name)
class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
- "isabelle-options", Some(Options.options_syntax), Isabelle.buffer_node_dummy)
+ "isabelle-options", Some(Options.options_syntax), JEdit_Lib.buffer_node_dummy)
class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
- "isabelle-root", Some(Build.root_syntax), Isabelle.buffer_node_dummy)
+ "isabelle-root", Some(Build.root_syntax), JEdit_Lib.buffer_node_dummy)
class Isabelle_Sidekick_Raw
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Sep 17 17:49:11 2012 +0200
@@ -0,0 +1,64 @@
+/* Title: Tools/jEdit/src/jedit_lib.scala
+ Author: Makarius
+
+Misc library functions for jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import org.gjt.sp.jedit.{jEdit, Buffer, View}
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+
+
+object JEdit_Lib
+{
+ /* buffers */
+
+ def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
+ Swing_Thread.now { buffer_lock(buffer) { body } }
+
+ def buffer_text(buffer: JEditBuffer): String =
+ buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+
+ def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+
+ def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
+ Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
+
+ def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
+ {
+ val name = buffer_name(buffer)
+ Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
+ }
+
+
+ /* main jEdit components */
+
+ def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
+
+ def jedit_buffer(name: String): Option[Buffer] =
+ jedit_buffers().find(buffer => buffer_name(buffer) == name)
+
+ def jedit_views(): Iterator[View] = jEdit.getViews().iterator
+
+ def jedit_text_areas(view: View): Iterator[JEditTextArea] =
+ view.getEditPanes().iterator.map(_.getTextArea)
+
+ def jedit_text_areas(): Iterator[JEditTextArea] =
+ jedit_views().flatMap(jedit_text_areas(_))
+
+ def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
+ jedit_text_areas().filter(_.getBuffer == buffer)
+
+ def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
+ {
+ try { buffer.readLock(); body }
+ finally { buffer.readUnlock() }
+ }
+}
+
--- a/src/Tools/jEdit/src/jedit_thy_load.scala Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Mon Sep 17 17:49:11 2012 +0200
@@ -36,9 +36,9 @@
override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
{
Swing_Thread.now {
- Isabelle.jedit_buffer(name.node) match {
+ JEdit_Lib.jedit_buffer(name.node) match {
case Some(buffer) =>
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
Some(f(buffer.getSegment(0, buffer.getLength)))
}
case None => None
--- a/src/Tools/jEdit/src/plugin.scala Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Sep 17 17:49:11 2012 +0200
@@ -9,23 +9,17 @@
import isabelle._
-import java.lang.System
-import java.awt.Font
import javax.swing.JOptionPane
-import scala.collection.mutable
import scala.swing.{ListView, ScrollPane}
-import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
- Buffer, EditPane, ServiceManager, View}
-import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View}
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
import org.gjt.sp.jedit.gui.DockableWindowManager
import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.util.Log
import scala.actors.Actor._
@@ -82,62 +76,6 @@
}
- /* icons */
-
- def load_icon(name: String): javax.swing.Icon =
- {
- val icon = GUIUtilities.loadIcon(name)
- if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
- Log.log(Log.ERROR, icon, "Bad icon: " + name)
- icon
- }
-
-
- /* buffers */
-
- def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
- Swing_Thread.now { buffer_lock(buffer) { body } }
-
- def buffer_text(buffer: JEditBuffer): String =
- buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
-
- def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
-
- def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
- Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
-
- def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
- {
- val name = buffer_name(buffer)
- Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
- }
-
-
- /* main jEdit components */
-
- def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
-
- def jedit_buffer(name: String): Option[Buffer] =
- jedit_buffers().find(buffer => buffer_name(buffer) == name)
-
- def jedit_views(): Iterator[View] = jEdit.getViews().iterator
-
- def jedit_text_areas(view: View): Iterator[JEditTextArea] =
- view.getEditPanes().iterator.map(_.getTextArea)
-
- def jedit_text_areas(): Iterator[JEditTextArea] =
- jedit_views().flatMap(jedit_text_areas(_))
-
- def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
- jedit_text_areas().filter(_.getBuffer == buffer)
-
- def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
- {
- try { buffer.readLock(); body }
- finally { buffer.readUnlock() }
- }
-
-
/* document model and view */
def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
@@ -145,24 +83,24 @@
def document_views(buffer: Buffer): List[Document_View] =
for {
- text_area <- jedit_text_areas(buffer).toList
+ text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
doc_view = document_view(text_area)
if doc_view.isDefined
} yield doc_view.get
def exit_model(buffer: Buffer)
{
- swing_buffer_lock(buffer) {
- jedit_text_areas(buffer).foreach(Document_View.exit)
+ JEdit_Lib.swing_buffer_lock(buffer) {
+ JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
Document_Model.exit(buffer)
}
}
def init_model(buffer: Buffer)
{
- swing_buffer_lock(buffer) {
+ JEdit_Lib.swing_buffer_lock(buffer) {
val opt_model =
- buffer_node_name(buffer) match {
+ JEdit_Lib.buffer_node_name(buffer) match {
case Some(node_name) =>
document_model(buffer) match {
case Some(model) if model.name == node_name => Some(model)
@@ -171,7 +109,7 @@
case None => None
}
if (opt_model.isDefined) {
- for (text_area <- jedit_text_areas(buffer)) {
+ for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
if (document_view(text_area).map(_.model) != opt_model)
Document_View.init(opt_model.get, text_area)
}
@@ -181,7 +119,7 @@
def init_view(buffer: Buffer, text_area: JEditTextArea)
{
- swing_buffer_lock(buffer) {
+ JEdit_Lib.swing_buffer_lock(buffer) {
document_model(buffer) match {
case Some(model) => Document_View.init(model, text_area)
case None =>
@@ -191,7 +129,7 @@
def exit_view(buffer: Buffer, text_area: JEditTextArea)
{
- swing_buffer_lock(buffer) {
+ JEdit_Lib.swing_buffer_lock(buffer) {
Document_View.exit(text_area)
}
}
@@ -264,10 +202,10 @@
{
val view = jEdit.getActiveView()
- val buffers = Isabelle.jedit_buffers().toList
+ val buffers = JEdit_Lib.jedit_buffers().toList
if (buffers.forall(_.isLoaded)) {
def loaded_buffer(name: String): Boolean =
- buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
+ buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
val thys =
for (buffer <- buffers; model <- Isabelle.document_model(buffer))
@@ -314,16 +252,16 @@
}
case Session.Ready =>
- Isabelle.jedit_buffers.foreach(Isabelle.init_model)
+ JEdit_Lib.jedit_buffers.foreach(Isabelle.init_model)
Swing_Thread.later { delay_load.invoke() }
case Session.Shutdown =>
- Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+ JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
Swing_Thread.later { delay_load.revoke() }
case _ =>
}
- case bad => System.err.println("session_manager: ignoring bad message " + bad)
+ case bad => java.lang.System.err.println("session_manager: ignoring bad message " + bad)
}
}
}
@@ -426,7 +364,7 @@
Isabelle.options.value.save_prefs()
Isabelle.session.phase_changed -= session_manager
- Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+ JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
Isabelle.session.stop()
}
}
--- a/src/Tools/jEdit/src/text_overview.scala Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala Mon Sep 17 17:49:11 2012 +0200
@@ -66,7 +66,7 @@
Swing_Thread.assert()
doc_view.robust_body(()) {
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
val snapshot = doc_view.model.snapshot()
if (snapshot.is_outdated) {