Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned output;
  2. more operations;
  3. removed inaccessible blobs from Document.Nodes;
  4. more accurate JSON parsing according to http://seriot.ch/parsing_json.php
  5. purge hidden nodes more thoroughly: is_hidden may become true only later;
  6. proper synchronized Map: this may be used on multiple threads;
Changeset 67114:3d8626cbaff8 by wenzelm:
tuned output;
The file was modified src/Pure/PIDE/document.scala (diff)
Changeset 67113:79ab935a7e22 by wenzelm:
more operations;
The file was modified src/Pure/PIDE/xml.scala (diff)
Changeset 67112:deb2fcbda16e by wenzelm:
removed inaccessible blobs from Document.Nodes;
The file was modified src/Pure/PIDE/document.scala (diff)
Changeset 67111:42f290d8ccbd by wenzelm:
more accurate JSON parsing according to http://seriot.ch/parsing_json.php
The file was modified src/Pure/General/json.scala (diff)
Changeset 67110:3156faac30a7 by wenzelm:
purge hidden nodes more thoroughly: is_hidden may become true only later;
The file was modified src/Pure/PIDE/document.scala (diff)
Changeset 67109:5fce3a24e476 by wenzelm:
proper synchronized Map: this may be used on multiple threads;
The file was modified src/Pure/PIDE/xml.scala (diff)