Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
  3. clarified user errors vs. failures, e.g. java.lang.StackOverflowError;
  4. further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt;
  5. proper Exn.capture with check_interrupt (amending a3dcae9a2ebe);
  6. distinguish proper interrupts from Poly/ML RTS breakdown;
  7. tuned;
  8. tuned;
  9. proper Isabelle_Thread.try_catch;
  10. tuned;
  11. proper Exn.capture / Isabelle_Thread.try_catch;
  12. tuned;
  13. clarified signature;
  14. proper Exn.capture;
  15. more robust: avoid race condition;
  16. clarified name;
  17. clarified signature;
  18. clarified comments;
  19. Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts
  20. atin now an abbreviation for atin_within, which has been moved to Abstract_Limits
Changeset 78769:1eb8a5e3fb5f by wenzelm:
merged
Changeset 78768:280a228dc2f1 by wenzelm:
prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
The file was modified src/Pure/Admin/build_log.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/mercurial.scala (diff)
Changeset 78767:aa67309a7960 by wenzelm:
clarified user errors vs. failures, e.g. java.lang.StackOverflowError;
The file was modified src/Pure/System/scala.scala (diff)
Changeset 78766:5578341489cb by wenzelm:
further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt;
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Concurrent/lazy.ML (diff)
The file was modified src/Pure/Concurrent/timeout.ML (diff)
Changeset 78765:f971ccccfd8e by wenzelm:
proper Exn.capture with check_interrupt (amending a3dcae9a2ebe);
The file was modified src/Pure/Concurrent/isabelle_thread.ML (diff)
Changeset 78764:a3dcae9a2ebe by wenzelm:
distinguish proper interrupts from Poly/ML RTS breakdown;
The file was modified NEWS (diff)
The file was modified src/Pure/Concurrent/isabelle_thread.ML (diff)
The file was modified src/Pure/Concurrent/par_exn.ML (diff)
The file was modified src/Pure/General/exn.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/ML/exn_properties.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 78763:b7157c137855 by wenzelm:
tuned;
The file was modified src/Pure/Concurrent/isabelle_thread.ML (diff)
Changeset 78762:89202852e52c by wenzelm:
tuned;
The file was modified src/Pure/Concurrent/isabelle_thread.ML (diff)
Changeset 78761:6b3f13d39612 by wenzelm:
proper Isabelle_Thread.try_catch;
The file was modified src/Pure/ML/ml_compiler0.ML (diff)
Changeset 78760:6ca807f7fed0 by wenzelm:
tuned;
The file was modified src/Pure/Concurrent/future.ML (diff)
Changeset 78759:461e924cc825 by wenzelm:
proper Exn.capture / Isabelle_Thread.try_catch;
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Isar/runtime.ML (diff)
The file was modified src/Pure/ML/ml_compiler.ML (diff)
The file was modified src/Pure/morphism.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 78758:05da36bc806f by wenzelm:
tuned;
The file was modified src/Pure/System/isabelle_process.ML (diff)
Changeset 78757:a094bf81a496 by wenzelm:
clarified signature;
The file was modified src/Pure/Concurrent/event_timer.ML (diff)
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Concurrent/isabelle_thread.ML (diff)
The file was modified src/Pure/Concurrent/lazy.ML (diff)
The file was modified src/Pure/Concurrent/task_queue.ML (diff)
The file was modified src/Pure/Concurrent/timeout.ML (diff)
The file was modified src/Pure/General/exn.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/PIDE/document.ML (diff)
The file was modified src/Pure/PIDE/execution.ML (diff)
The file was modified src/Pure/PIDE/protocol.ML (diff)
The file was modified src/Pure/PIDE/protocol_command.ML (diff)
The file was modified src/Pure/PIDE/query_operation.ML (diff)
The file was modified src/Pure/System/command_line.ML (diff)
The file was modified src/Pure/System/isabelle_process.ML (diff)
The file was modified src/Pure/System/isabelle_system.ML (diff)
The file was modified src/Pure/System/scala.ML (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Tools/build.ML (diff)
The file was modified src/Pure/Tools/simplifier_trace.ML (diff)
Changeset 78756:96b3d13606b1 by wenzelm:
proper Exn.capture;
The file was modified src/Pure/Concurrent/event_timer.ML (diff)
Changeset 78755:42e48ad59cda by wenzelm:
more robust: avoid race condition;
The file was modified src/Pure/Concurrent/isabelle_thread.ML (diff)
Changeset 78754:5838285a8245 by wenzelm:
clarified name;
The file was modified src/HOL/Tools/Sledgehammer/async_manager_legacy.ML (diff)
Changeset 78753:f40b59292288 by wenzelm:
clarified signature;
The file was modified src/HOL/Tools/Sledgehammer/async_manager_legacy.ML (diff)
The file was modified src/Pure/Concurrent/event_timer.ML (diff)
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Concurrent/isabelle_thread.ML (diff)
The file was modified src/Pure/System/message_channel.ML (diff)
The file was modified src/Pure/Tools/build.ML (diff)
Changeset 78752:019cec83b49f by wenzelm:
clarified comments;
The file was modified src/Pure/Concurrent/event_timer.ML (diff)
Changeset 78751:80b4f6a0808d by paulson _lp15@cam.ac.uk_:
Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts
The file was modified src/HOL/Complex_Analysis/Laurent_Convergence.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Laurent_Series.thy (diff)
Changeset 78750:f229090cb8a3 by paulson _lp15@cam.ac.uk_:
atin now an abbreviation for atin_within, which has been moved to Abstract_Limits
The file was modified src/HOL/Analysis/Abstract_Limits.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Urysohn.thy (diff)