Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more operations;
  2. more operations;
  3. support for RDF/XML representation;
  4. tuned according to Scala version;
  5. support for XML name spaces;
  6. uniform XML header;
Changeset 69809:028f61045e8d by wenzelm:
more operations;
The file was modified src/Pure/General/rdf.scala (diff)
Changeset 69808:c64197a224c6 by wenzelm:
more operations;
The file was modified src/Pure/General/rdf.scala (diff)
Changeset 69807:3389fda6cffd by wenzelm:
support for RDF/XML representation;
The file was addedsrc/Pure/General/rdf.scala
The file was modified src/Pure/build-jars (diff)
Changeset 69806:2156053c4ce9 by wenzelm:
tuned according to Scala version;
The file was modified src/Pure/PIDE/xml.ML (diff)
Changeset 69805:a8debe27c36c by wenzelm:
support for XML name spaces;
The file was modified src/Pure/PIDE/xml.scala (diff)
Changeset 69804:9efccbad7d42 by wenzelm:
uniform XML header;
The file was modified src/Pure/PIDE/xml.ML (diff)
The file was modified src/Pure/PIDE/xml.scala (diff)
The file was modified src/Pure/Thy/html.ML (diff)
The file was modified src/Pure/Thy/html.scala (diff)
The file was modified src/Pure/Tools/main.scala (diff)