Summary
- prefer existing operation;
- retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
- clarified signature -- avoid confusion with Resources.is_hidden;
- markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
The file was modified | src/HOL/Library/case_converter.ML (diff) |
The file was modified | src/Pure/PIDE/document.scala (diff) |
The file was modified | src/Pure/PIDE/document.scala (diff) |
The file was modified | src/Tools/jEdit/src/theories_dockable.scala (diff) |
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) |