Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. URIs should normally be "rdf:resource", not string body;
  2. clarified signature;
  3. support for document meta data in PIDE and RDF;
  4. tuned signature;
  5. tuned signature;
  6. tuned signature;
  7. tuned signature;
Changeset 69902:9c697c7ad8d6 by wenzelm:
URIs should normally be "rdf:resource", not string body;
The file was modified src/Pure/General/rdf.scala (diff)
Changeset 69901:20b32ade0024 by wenzelm:
clarified signature;
The file was modified src/Pure/General/url.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
Changeset 69900:18a61caf5e68 by wenzelm:
support for document meta data in PIDE and RDF;
The file was modified src/Pure/General/rdf.scala (diff)
The file was modified src/Pure/PIDE/rendering.scala (diff)
Changeset 69899:27cf4287de43 by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/rendering.scala (diff)
Changeset 69898:990c6e8faf2c by wenzelm:
tuned signature;
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 69897:a9849222844d by wenzelm:
tuned signature;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 69896:be7243b97c41 by wenzelm:
tuned signature;
The file was modified src/Pure/Tools/dump.scala (diff)
The file was modified src/Pure/Tools/update.scala (diff)