Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. Renamed balanced to complete; added balanced; more about both
  3. tuned GUI: modal dialog last;
  4. tuned message;
  5. merged
  6. NEWS;
  7. more robust persistent storage; tuned;
  8. clarified important directories;
  9. separate action; tuned message;
  10. check keymap changes on startup;
  11. tuned message;
  12. clarified GUI; tuned;
  13. actual actions; tuned;
  14. tuned;
  15. clarified;
  16. tuned GUI;
  17. clarified GUI;
  18. tuned GUI;
  19. tuned rendering;
  20. more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
  21. clarified shortcut conflicts; tuned;
  22. clarified (see 019856db2bb6, ea52509f4c42);
  23. some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
  24. added glyph from "Deja Vu Sans Mono" font;
Changeset 63756:6b6bf5c0f9c1 by nipkow:
merged
Changeset 63755:182c111190e5 by nipkow:
Renamed balanced to complete; added balanced; more about both
The file was modified src/HOL/Data_Structures/Balance_List.thy (diff)
The file was modified src/HOL/Library/Tree.thy (diff)
Changeset 63754:23b013b6b2fb by wenzelm:
tuned GUI: modal dialog last;
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
Changeset 63753:c57db6b2befc by wenzelm:
tuned message;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63752:79f11158dcc4 by wenzelm:
merged
Changeset 63751:300f9782cb6f by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 63750:9c8a366778e1 by wenzelm:
more robust persistent storage;<br>tuned;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63749:4fe8cfaeb1fc by wenzelm:
clarified important directories;
The file was modified src/Doc/JEdit/JEdit.thy (diff)
The file was modified src/Pure/Tools/main.scala (diff)
The file was modified src/Tools/jEdit/src/jEdit.props (diff)
Changeset 63748:ebcc70c120a9 by wenzelm:
separate action;<br>tuned message;
The file was modified src/Tools/jEdit/src/actions.xml (diff)
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
Changeset 63747:b9b5a0ab54ee by wenzelm:
check keymap changes on startup;
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
Changeset 63746:962707e50fc0 by wenzelm:
tuned message;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63745:dde79b7faddf by wenzelm:
clarified GUI;<br>tuned;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63744:a406d7ab54ce by wenzelm:
actual actions;<br>tuned;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63743:beebcfc745d3 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63742:1e676fcd7ede by wenzelm:
clarified;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63741:10c08a4d39dd by wenzelm:
tuned GUI;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63740:7b2963b11e4a by wenzelm:
clarified GUI;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63739:352a257fa13a by wenzelm:
tuned GUI;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63738:f215f5f5bd35 by wenzelm:
tuned rendering;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63737:6de6e883c5fb by wenzelm:
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63736:33fb64d7842a by wenzelm:
clarified shortcut conflicts;<br>tuned;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
Changeset 63735:fb0ae6b60491 by wenzelm:
clarified (see 019856db2bb6, ea52509f4c42);
The file was modified src/Tools/jEdit/src/jEdit.props (diff)
Changeset 63734:133e3e84e6fb by wenzelm:
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
The file was addedsrc/Tools/jEdit/src/keymap_merge.scala
The file was modified src/Pure/library.scala (diff)
The file was modified src/Tools/jEdit/lib/Tools/jedit (diff)
Changeset 63733:7dc86a284456 by wenzelm:
added glyph from &quot;Deja Vu Sans Mono&quot; font;
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified etc/symbols (diff)
The file was modified lib/fonts/IsabelleText.sfd (diff)
The file was modified lib/fonts/IsabelleTextBold.sfd (diff)