set view title dynamically;
authorwenzelm
Fri May 04 16:22:09 2018 +0200 (13 months ago)
changeset 6808017f79ae49401
parent 68078 48e188cb1591
child 68081 3d8f34715013
set view title dynamically;
Admin/lib/Tools/makedist_bundle
NEWS
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/Admin/lib/Tools/makedist_bundle	Fri May 04 15:59:21 2018 +0200
     1.2 +++ b/Admin/lib/Tools/makedist_bundle	Fri May 04 16:22:09 2018 +0200
     1.3 @@ -185,9 +185,6 @@
     1.4  
     1.5  # platform-specific setup (inside archive)
     1.6  
     1.7 -perl -pi -e "s,view.title=Isabelle/jEdit,view.title=${ISABELLE_NAME},g;" \
     1.8 -  "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
     1.9 -
    1.10  case "$PLATFORM_FAMILY" in
    1.11    linux)
    1.12      purge_target 'contrib -name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
     2.1 --- a/NEWS	Fri May 04 15:59:21 2018 +0200
     2.2 +++ b/NEWS	Fri May 04 16:22:09 2018 +0200
     2.3 @@ -71,6 +71,10 @@
     2.4  
     2.5  *** Isabelle/jEdit Prover IDE ***
     2.6  
     2.7 +* The view title is set dynamically, according to the Isabelle
     2.8 +distribution and the logic session name. The user can override this via
     2.9 +set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).
    2.10 +
    2.11  * System options "spell_checker_include" and "spell_checker_exclude"
    2.12  supersede former "spell_checker_elements" to determine regions of text
    2.13  that are subject to spell-checking. Minor INCOMPATIBILITY.
     3.1 --- a/src/Tools/jEdit/src/jEdit.props	Fri May 04 15:59:21 2018 +0200
     3.2 +++ b/src/Tools/jEdit/src/jEdit.props	Fri May 04 16:22:09 2018 +0200
     3.3 @@ -310,6 +310,5 @@
     3.4  view.middleMousePaste=true
     3.5  view.showToolbar=true
     3.6  view.thickCaret=true
     3.7 -view.title=Isabelle/jEdit -\u0020
     3.8  view.width=1072
     3.9  xml-insert-closing-tag.shortcut=
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri May 04 15:59:21 2018 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri May 04 16:22:09 2018 +0200
     4.3 @@ -16,7 +16,8 @@
     4.4  import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, PerspectiveManager}
     4.5  import org.gjt.sp.jedit.textarea.JEditTextArea
     4.6  import org.gjt.sp.jedit.syntax.ModeProvider
     4.7 -import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
     4.8 +import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged,
     4.9 +  ViewUpdate}
    4.10  import org.gjt.sp.util.SyntaxUtilities
    4.11  import org.gjt.sp.util.Log
    4.12  
    4.13 @@ -292,6 +293,19 @@
    4.14      Keymap_Merge.check_dialog(view)
    4.15    }
    4.16  
    4.17 +  private def init_title(view: View)
    4.18 +  {
    4.19 +    val title =
    4.20 +      proper_string(Isabelle_System.getenv("ISABELLE_IDENTIFIER")).getOrElse("Isabelle") +
    4.21 +        "/" + PIDE.resources.session_name
    4.22 +    val marker = "\u200B"
    4.23 +
    4.24 +    val old_title = view.getViewConfig.title
    4.25 +    if (old_title == null || old_title.startsWith(marker)) {
    4.26 +      view.setUserTitle(marker + title)
    4.27 +    }
    4.28 +  }
    4.29 +
    4.30    override def handleMessage(message: EBMessage)
    4.31    {
    4.32      GUI_Thread.assert {}
    4.33 @@ -330,6 +344,10 @@
    4.34            PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
    4.35              JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
    4.36  
    4.37 +        case msg: ViewUpdate
    4.38 +        if msg.getWhat == ViewUpdate.CREATED && msg.getView != null =>
    4.39 +          init_title(msg.getView)
    4.40 +
    4.41          case msg: BufferUpdate
    4.42          if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
    4.43            if (msg.getBuffer != null) {
    4.44 @@ -436,6 +454,8 @@
    4.45        completion_history.load()
    4.46        spell_checker.update(options.value)
    4.47  
    4.48 +      JEdit_Lib.jedit_views.foreach(init_title(_))
    4.49 +
    4.50        isabelle.jedit_base.Syntax_Style.set_style_extender(Syntax_Style.Extender)
    4.51        init_mode_provider()
    4.52        JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)