# HG changeset patch # User wenzelm # Date 1347896951 -7200 # Node ID 38db4832b210259669df4d6fbe26df2d6b47e712 # Parent 2fc68b3787a80b810a5b9b0e4c30be7762617114 somewhat more general JEdit_Lib; tuned signatures; diff -r 2fc68b3787a8 -r 38db4832b210 src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 2fc68b3787a8 -r 38db4832b210 src/Tools/jEdit/src/document_model.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() diff -r 2fc68b3787a8 -r 38db4832b210 src/Tools/jEdit/src/document_view.scala --- 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() diff -r 2fc68b3787a8 -r 38db4832b210 src/Tools/jEdit/src/hyperlink.scala --- 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 diff -r 2fc68b3787a8 -r 38db4832b210 src/Tools/jEdit/src/isabelle_rendering.scala --- 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 */ diff -r 2fc68b3787a8 -r 38db4832b210 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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 diff -r 2fc68b3787a8 -r 38db4832b210 src/Tools/jEdit/src/jedit_lib.scala --- /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() } + } +} + diff -r 2fc68b3787a8 -r 38db4832b210 src/Tools/jEdit/src/jedit_thy_load.scala --- 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 diff -r 2fc68b3787a8 -r 38db4832b210 src/Tools/jEdit/src/plugin.scala --- 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() } } diff -r 2fc68b3787a8 -r 38db4832b210 src/Tools/jEdit/src/text_overview.scala --- 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) {