--- a/src/Tools/jEdit/src/plugin.scala Fri May 04 15:59:21 2018 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Fri May 04 16:22:09 2018 +0200
@@ -16,7 +16,8 @@
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, PerspectiveManager}
import org.gjt.sp.jedit.textarea.JEditTextArea
import org.gjt.sp.jedit.syntax.ModeProvider
-import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
+import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged,
+ ViewUpdate}
import org.gjt.sp.util.SyntaxUtilities
import org.gjt.sp.util.Log
@@ -292,6 +293,19 @@
Keymap_Merge.check_dialog(view)
}
+ private def init_title(view: View)
+ {
+ val title =
+ proper_string(Isabelle_System.getenv("ISABELLE_IDENTIFIER")).getOrElse("Isabelle") +
+ "/" + PIDE.resources.session_name
+ val marker = "\u200B"
+
+ val old_title = view.getViewConfig.title
+ if (old_title == null || old_title.startsWith(marker)) {
+ view.setUserTitle(marker + title)
+ }
+ }
+
override def handleMessage(message: EBMessage)
{
GUI_Thread.assert {}
@@ -330,6 +344,10 @@
PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
+ case msg: ViewUpdate
+ if msg.getWhat == ViewUpdate.CREATED && msg.getView != null =>
+ init_title(msg.getView)
+
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
if (msg.getBuffer != null) {
@@ -436,6 +454,8 @@
completion_history.load()
spell_checker.update(options.value)
+ JEdit_Lib.jedit_views.foreach(init_title(_))
+
isabelle.jedit_base.Syntax_Style.set_style_extender(Syntax_Style.Extender)
init_mode_provider()
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)