Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more options;
  2. clarified default server name;
  3. more uniform output: this may be parsed by another program;
  4. clarified argument formats: explicit Unit, allow XML.Elem as well; tuned messages: prefer single quotes for JSON output;
  5. tuned comments;
  6. convenience to represent XML.Body as single XML.Elem;
  7. clarified AFP partitioning;
Changeset 67823:92cf045c876b by wenzelm:
more options;
The file was modified src/Pure/Tools/server.scala (diff)
Changeset 67822:0e2484df2491 by wenzelm:
clarified default server name;
The file was modified src/Pure/Tools/server.scala (diff)
Changeset 67821:82fb12061069 by wenzelm:
more uniform output: this may be parsed by another program;
The file was modified src/Pure/Tools/server.scala (diff)
Changeset 67820:e30d6368c7c8 by wenzelm:
clarified argument formats: explicit Unit, allow XML.Elem as well;<br>tuned messages: prefer single quotes for JSON output;
The file was modified src/Pure/PIDE/yxml.scala (diff)
The file was modified src/Pure/Tools/server.scala (diff)
The file was modified src/Pure/library.scala (diff)
Changeset 67819:b73d8ed73b35 by wenzelm:
tuned comments;
The file was modified src/Pure/General/json.scala (diff)
Changeset 67818:2457bea123e4 by wenzelm:
convenience to represent XML.Body as single XML.Elem;
The file was modified src/Pure/PIDE/xml.scala (diff)
Changeset 67817:93faefc25fe7 by wenzelm:
clarified AFP partitioning;
The file was modified src/Pure/Admin/afp.scala (diff)