Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robust selection: avoid duplicates via "batch" number; evade attempts to select separator via keyboard or mouse (non-keyboard), assuming there are no consecutive separators;
  2. tuned GUI;
  3. clarified GUI.Selector, with support for separator as pseudo-entry; clarified signature;
  4. clarified GUI state; added "Load" button;
  5. clarified file names;
  6. clarified Log_Progress vs. GUI: more like Syslog_Dockable;
  7. clarified signature: more public operations;
  8. tuned signature, following hints by IntelliJ IDEA;
Changeset 76494:9686049ce988 by wenzelm:
more robust selection: avoid duplicates via &quot;batch&quot; number;<br>evade attempts to select separator via keyboard or mouse (non-keyboard), assuming there are no consecutive separators;
The file was modified src/Pure/GUI/gui.scala (diff)
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_sessions.scala (diff)
Changeset 76493:2dfc8885c0ee by wenzelm:
tuned GUI;
The file was modified src/Tools/jEdit/src/jedit_sessions.scala (diff)
Changeset 76492:e228be7cd375 by wenzelm:
clarified GUI.Selector, with support for separator as pseudo-entry;<br>clarified signature;
The file was modified src/Pure/GUI/gui.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/spell_checker.scala (diff)
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_sessions.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_spell_checker.scala (diff)
The file was modified src/Tools/jEdit/src/monitor_dockable.scala (diff)
Changeset 76491:2c37c10d6884 by wenzelm:
clarified GUI state;<br>added &quot;Load&quot; button;
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
Changeset 76490:deded566d423 by wenzelm:
clarified file names;
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
Changeset 76489:8c9830109ab2 by wenzelm:
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
Changeset 76488:1eed7e1300ed by wenzelm:
clarified signature: more public operations;
The file was modified src/Pure/PIDE/session.scala (diff)
The file was modified src/Pure/System/isabelle_process.scala (diff)
The file was modified src/Tools/jEdit/src/main_plugin.scala (diff)
The file was modified src/Tools/jEdit/src/syslog_dockable.scala (diff)
Changeset 76487:304ae1a6e160 by wenzelm:
tuned signature, following hints by IntelliJ IDEA;
The file was modified src/Tools/jEdit/src/pretty_tooltip.scala (diff)