Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned --- fewer warnings;
  2. tuned --- fewer warnings;
  3. more robust error;
  4. tuned --- fewer warnings;
  5. tuned --- fewer warnings;
  6. tuned --- fewer warnings;
  7. updated to scala-2.13.5 (with scala-swing_2.13-3.0.0);
  8. slightly more efficient Term.fastype_of (only little impact in regular applications);
Changeset 73358:78aa7846e91f by wenzelm:
tuned --- fewer warnings;
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
The file was modified src/Tools/jEdit/src/isabelle_sidekick.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
The file was modified src/Tools/jEdit/src/pretty_tooltip.scala (diff)
The file was modified src/Tools/jEdit/src/text_structure.scala (diff)
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/timing_dockable.scala (diff)
Changeset 73357:31d4274f32de by wenzelm:
tuned --- fewer warnings;
The file was modified src/Pure/General/scan.scala (diff)
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/library.scala (diff)
The file was modified src/Tools/Graphview/mutator_dialog.scala (diff)
The file was modified src/Tools/VSCode/src/language_server.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
Changeset 73356:819f6033fb4e by wenzelm:
more robust error;
The file was modified src/Pure/System/scala.scala (diff)
Changeset 73355:ec52a1a6ed31 by wenzelm:
tuned --- fewer warnings;
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Pure/library.scala (diff)
Changeset 73354:79b120d1c1a3 by wenzelm:
tuned --- fewer warnings;
The file was modified src/Tools/jEdit/src/jedit_lib.scala (diff)
Changeset 73353:279e45248e9d by wenzelm:
tuned --- fewer warnings;
The file was modified src/Pure/General/file_watcher.scala (diff)
The file was modified src/Tools/jEdit/src/fold_handling.scala (diff)
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
The file was modified src/Tools/jEdit/src/token_markup.scala (diff)
Changeset 73352:54b43bcf1df3 by wenzelm:
updated to scala-2.13.5 (with scala-swing_2.13-3.0.0);
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified src/Pure/ROOT.scala (diff)
Changeset 73351:88dd8a6a42ba by wenzelm:
slightly more efficient Term.fastype_of (only little impact in regular applications);
The file was modified src/Pure/term.ML (diff)