Skip to content
Failed

Changes

Summary

  1. prefer existing operation;
  2. retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
  3. clarified signature -- avoid confusion with Resources.is_hidden;
  4. markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
Changeset 68301:fb5653a7a879 by wenzelm:
prefer existing operation;
The file was modified src/HOL/Library/case_converter.ML (diff)
Changeset 68300:cd8ab1a7a286 by wenzelm:
retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
The file was modified src/Pure/PIDE/document.scala (diff)
Changeset 68299:0b5a23477911 by wenzelm:
clarified signature -- avoid confusion with Resources.is_hidden;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)
Changeset 68298:2c3ce27cf4a8 by wenzelm:
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
The file was modified src/Pure/General/symbol_pos.ML (diff)
The file was modified src/Pure/Isar/token.ML (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)