Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned signature;
  2. even more robust syntax (amending 122df1fde073);
  3. clarified error for bad session-qualified imports;
  4. clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;
Changeset 66773:0cd29455a5e8 by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/document.scala (diff)
Changeset 66772:a66f11a0b5b1 by wenzelm:
even more robust syntax (amending 122df1fde073);
The file was modified src/Pure/Thy/thy_syntax.scala (diff)
Changeset 66771:925d10a7a610 by wenzelm:
clarified error for bad session-qualified imports;
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/Thy/thy_header.ML (diff)
Changeset 66770:122df1fde073 by wenzelm:
clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Thy/thy_syntax.scala (diff)