Skip to content
Success

Changes

Summary

  1. entries_graph requires acyclic graph, but lazy val allows forming the AFP object nonetheless;
  2. more informative Imports.Report with actual session imports (minimized);
  3. more robust: allow URLs;
  4. more robust: allow Windows file names;
  5. clarified signature;
  6. relaxed assm
Changeset 66852:d20a668b394e by wenzelm:
entries_graph requires acyclic graph, but lazy val allows forming the AFP object nonetheless;
The file was modified src/Pure/Admin/afp.scala (diff)
Changeset 66851:c75769065548 by wenzelm:
more informative Imports.Report with actual session imports (minimized);
The file was modified NEWS (diff)
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/Pure/Tools/imports.scala (diff)
Changeset 66850:a91b6d80c911 by wenzelm:
more robust: allow URLs;
The file was modified src/Pure/PIDE/resources.scala (diff)
Changeset 66849:42311fd08899 by wenzelm:
more robust: allow Windows file names;
The file was modified src/Pure/PIDE/document.scala (diff)
Changeset 66848:982baed14542 by wenzelm:
clarified signature;
The file was modified src/Pure/ML/ml_process.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/imports.scala (diff)
Changeset 66847:e8282131ddf9 by nipkow:
relaxed assm
The file was modified src/HOL/List.thy (diff)