Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. misc tuning and modernization;
  3. support to encode/decode command state; support to merge full contents of command state;
  4. tuned;
  5. more operations;
  6. tuned signature;
  7. eliminated redundant check (see also 27328dcaf64c vs. 9c53198dbb1c);
  8. Corrected affiliation.
Changeset 65337:27144776aefe by wenzelm:
merged
Changeset 65336:8e5274fc0093 by wenzelm:
misc tuning and modernization;
The file was modified src/HOL/Word/Tools/smt_word.ML (diff)
The file was modified src/HOL/Word/Word.thy (diff)
Changeset 65335:7634d33c1a79 by wenzelm:
support to encode/decode command state;<br>support to merge full contents of command state;
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Pure/Isar/token.scala (diff)
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/command_span.scala (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
Changeset 65334:264a3904ab5a by wenzelm:
tuned;
The file was modified src/Pure/PIDE/xml.scala (diff)
Changeset 65333:289561ca4fa3 by wenzelm:
more operations;
The file was modified src/Pure/PIDE/xml.ML (diff)
The file was modified src/Pure/PIDE/xml.scala (diff)
Changeset 65332:7dbb780f24a9 by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
The file was modified src/Tools/jEdit/src/rich_text_area.scala (diff)
Changeset 65331:999864cdf96c by wenzelm:
eliminated redundant check (see also 27328dcaf64c vs. 9c53198dbb1c);
The file was modified src/Tools/jEdit/src/document_view.scala (diff)
Changeset 65330:d83f709b7580 by ballarin:
Corrected affiliation.
The file was modified CONTRIBUTORS (diff)