Skip to content
Success

Changes

Summary

  1. update documentation on Isabelle/ML exceptions;
  2. misc tuning;
  3. discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);
  4. proper thread context for "isabelle-markup" Sidekick parser (amending 01a7265db76b);
  5. proper Scala version, e.g. for IntelliJ IDEA;
Changeset 78742:b2216709a839 by wenzelm:
update documentation on Isabelle/ML exceptions;
The file was modified src/Doc/Implementation/ML.thy (diff)
Changeset 78741:39498d504f43 by wenzelm:
misc tuning;
The file was modified src/Doc/Implementation/ML.thy (diff)
Changeset 78740:45ff003d337c by wenzelm:
discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);
The file was modified src/Pure/Concurrent/isabelle_thread.ML (diff)
The file was modified src/Pure/ML/ml_init.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 78739:08fedb5bdeb0 by wenzelm:
proper thread context for "isabelle-markup" Sidekick parser (amending 01a7265db76b);
The file was modified src/Tools/jEdit/jedit_main/isabelle_sidekick.scala (diff)
Changeset 78738:323eecf508b4 by wenzelm:
proper Scala version, e.g. for IntelliJ IDEA;
The file was modified src/Pure/Tools/scala_project.scala (diff)