Jonas Jenwald 65132ba5d8 Handle WorkerTasks, and various PDF document properties, correctly in the "SaveDocument" handler in src/core/worker.js
- Actually register/unregister the `WorkerTask`s, used when saving each page, correctly.
   To prevent issues when terminating the Worker, we purposely wait for all running `WorkerTask`s to complete first. Hence we need to actually handle `WorkerTask`s the same way in "SaveDocument" as in the rest of this file, see e.g. "GetOperatorList" and "GetTextContent".

 - Access `PDFDocument` properties in a generally safe/consistent way.
   While the current code works fine, given how the PDF document is being loaded, it still seems like a very good idea to be *consistent* in how we access these kind of properties (since in general you need to avoid `MissingDataException` everywhere in this file).

 - Change a variable name, since there's essentially no precedent in the code-base for *local* variable names to start with an underscore.
2020-10-13 19:30:43 +02:00
..
2020-04-17 12:24:46 +02:00
2020-04-14 12:28:14 +02:00
2020-04-14 12:28:14 +02:00