Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. some concrete commands; clarified messages;
  2. tuned signature;
  3. more formal messages;
  4. tuned signature;
  5. separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
  6. more permissive;
  7. tuned;
  8. separate JSON lexer;
  9. clarified command language;
Changeset 66929:c19b17b72777 by wenzelm:
some concrete commands;<br>clarified messages;
The file was modified src/Pure/Tools/server.scala (diff)
Changeset 66928:33f9133bed7c by wenzelm:
tuned signature;
The file was modified src/Pure/General/json.scala (diff)
Changeset 66927:153d7b68e8f8 by wenzelm:
more formal messages;
The file was modified src/Pure/Tools/server.scala (diff)
Changeset 66926:4cf560a6dd84 by wenzelm:
tuned signature;
The file was modified src/Pure/General/json.scala (diff)
Changeset 66925:8b117dc73278 by wenzelm:
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
The file was modified src/Pure/General/json.scala (diff)
Changeset 66924:b4d4027f743b by wenzelm:
more permissive;
The file was modified src/Pure/General/json.scala (diff)
Changeset 66923:914935f8a462 by wenzelm:
tuned;
The file was modified src/Pure/Admin/build_release.scala (diff)
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
The file was modified src/Pure/General/http.scala (diff)
The file was modified src/Pure/General/long_name.scala (diff)
The file was modified src/Pure/General/ssh.scala (diff)
The file was modified src/Pure/PIDE/line.scala (diff)
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Pure/System/numa.scala (diff)
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)
The file was modified src/Tools/jEdit/src/scala_console.scala (diff)
Changeset 66922:5a476a87a535 by wenzelm:
separate JSON lexer;
The file was modified src/Pure/General/json.scala (diff)
The file was modified src/Pure/General/scan.scala (diff)
Changeset 66921:3d3bd0718ef2 by wenzelm:
clarified command language;
The file was modified src/Pure/Tools/server.scala (diff)