# HG changeset patch
# User wenzelm
# Date 1525465585 -7200
# Node ID b25ccd85b1fd2f696ab487cbb18085172b711d92
# Parent  9c2088adff8b19ffb3de2a02c8dc7d6f0b05a9e5# Parent  3d8f34715013a05b171e1051de8745d8357bd477
merged

diff -r 9c2088adff8b -r b25ccd85b1fd Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri May 04 18:41:11 2018 +0200
+++ b/Admin/components/components.sha1	Fri May 04 22:26:25 2018 +0200
@@ -126,6 +126,7 @@
 d4e1496c257659cf15458d718f4663cdd95a404e  jedit_build-20161024.tar.gz
 d806c1c26b571b5b4ef05ea11e8b9cf936518e06  jedit_build-20170319.tar.gz
 7bcb202e13358dd750e964b2f747664428b5d8b3  jedit_build-20180417.tar.gz
+23c8a05687d05a6937f7d600ac3aa19e3ce59c9c  jedit_build-20180504.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 d911f63a5c9b4c7335bb73f805cb1711ce017a84  jfreechart-1.5.0.tar.gz
diff -r 9c2088adff8b -r b25ccd85b1fd Admin/components/main
--- a/Admin/components/main	Fri May 04 18:41:11 2018 +0200
+++ b/Admin/components/main	Fri May 04 22:26:25 2018 +0200
@@ -6,7 +6,7 @@
 e-2.0-1
 isabelle_fonts-20180113
 jdk-8u172
-jedit_build-20180417
+jedit_build-20180504
 jfreechart-1.5.0
 jortho-1.0-2
 kodkodi-1.5.2
diff -r 9c2088adff8b -r b25ccd85b1fd Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Fri May 04 18:41:11 2018 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Fri May 04 22:26:25 2018 +0200
@@ -185,9 +185,6 @@
 
 # platform-specific setup (inside archive)
 
-perl -pi -e "s,view.title=Isabelle/jEdit,view.title=${ISABELLE_NAME},g;" \
-  "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
-
 case "$PLATFORM_FAMILY" in
   linux)
     purge_target 'contrib -name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
diff -r 9c2088adff8b -r b25ccd85b1fd NEWS
--- a/NEWS	Fri May 04 18:41:11 2018 +0200
+++ b/NEWS	Fri May 04 22:26:25 2018 +0200
@@ -71,6 +71,10 @@
 
 *** Isabelle/jEdit Prover IDE ***
 
+* The view title is set dynamically, according to the Isabelle
+distribution and the logic session name. The user can override this via
+set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).
+
 * System options "spell_checker_include" and "spell_checker_exclude"
 supersede former "spell_checker_elements" to determine regions of text
 that are subject to spell-checking. Minor INCOMPATIBILITY.
diff -r 9c2088adff8b -r b25ccd85b1fd src/Tools/jEdit/patches/title
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/title	Fri May 04 22:26:25 2018 +0200
@@ -0,0 +1,23 @@
+diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/View.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java
+--- 5.5.0/jEdit/org/gjt/sp/jedit/View.java	2018-04-09 01:57:31.000000000 +0200
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java	2018-05-04 21:18:11.891194939 +0200
+@@ -1233,15 +1233,10 @@
+ 
+ 		StringBuilder title = new StringBuilder();
+ 
+-		/* On Mac OS X, apps are not supposed to show their name in the
+-		title bar. */
+-		if(!OperatingSystem.isMacOS())
+-		{
+-			if (userTitle != null)
+-				title.append(userTitle);
+-			else
+-				title.append(jEdit.getProperty("view.title"));
+-		}
++		if (userTitle != null)
++			title.append(userTitle);
++		else
++			title.append(jEdit.getProperty("view.title"));
+ 
+ 		for(int i = 0; i < buffers.size(); i++)
+ 		{
diff -r 9c2088adff8b -r b25ccd85b1fd src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Fri May 04 18:41:11 2018 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Fri May 04 22:26:25 2018 +0200
@@ -310,6 +310,5 @@
 view.middleMousePaste=true
 view.showToolbar=true
 view.thickCaret=true
-view.title=Isabelle/jEdit -\u0020
 view.width=1072
 xml-insert-closing-tag.shortcut=
diff -r 9c2088adff8b -r b25ccd85b1fd src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri May 04 18:41:11 2018 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri May 04 22:26:25 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 _)