Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. introduced bst_wrt
  3. less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
  4. tolerate more errors (cf. 1e5ae735e026);
Changeset 66607:a8edca8c4a68 by nipkow:
merged
Changeset 66606:f23f044148d3 by nipkow:
introduced bst_wrt
The file was modified src/HOL/Library/Tree.thy (diff)
Changeset 66605:261dcd52c5a0 by wenzelm:
less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
The file was modified src/Pure/PIDE/line.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
Changeset 66604:1af360d1cad2 by wenzelm:
tolerate more errors (cf. 1e5ae735e026);
The file was modified src/Pure/Thy/sessions.scala (diff)