Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. proper reset of column (amending 01e50039edc9);
  3. added option -T: text length encoding;
  4. more systematic text length wrt. encoding;
  5. tuned;
  6. more systematic text length;
  7. unused;
  8. proper counting of chars;
  9. tuned;
  10. clarified modules;
  11. clarified modules;
  12. tuned;
Changeset 64620:14f938969779 by wenzelm:
merged
Changeset 64619:e3d9a31281f3 by wenzelm:
proper reset of column (amending 01e50039edc9);
The file was modified src/Pure/PIDE/line.scala (diff)
Changeset 64618:c81bd30839a6 by wenzelm:
added option -T: text length encoding;
The file was modified src/Pure/General/length.scala (diff)
The file was modified src/Tools/VSCode/src/server.scala (diff)
Changeset 64617:01e50039edc9 by wenzelm:
more systematic text length wrt. encoding;
The file was addedsrc/Pure/General/length.scala
The file was modified src/Pure/General/codepoint.scala (diff)
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Pure/PIDE/line.scala (diff)
The file was modified src/Pure/System/utf8.scala (diff)
The file was modified src/Pure/build-jars (diff)
Changeset 64616:dc3ec40fe41b by wenzelm:
tuned;
The file was modified src/Pure/Isar/outer_syntax.scala (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
Changeset 64615:fd0d6de380c6 by wenzelm:
more systematic text length;
The file was modified src/Pure/General/codepoint.scala (diff)
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Pure/PIDE/line.scala (diff)
The file was modified src/Pure/System/utf8.scala (diff)
Changeset 64614:88211daacf93 by wenzelm:
unused;
The file was modified src/Pure/PIDE/line.scala (diff)
Changeset 64613:d1ca9ce0d9e4 by wenzelm:
proper counting of chars;
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
Changeset 64612:08e4b1aeac50 by wenzelm:
tuned;
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
Changeset 64611:d72d63d05bdb by wenzelm:
clarified modules;
The file was addedsrc/Pure/PIDE/line.scala
The file was modified src/Pure/build-jars (diff)
The file was removedsrc/Tools/VSCode/src/line.scala
Changeset 64610:1b89608974e9 by wenzelm:
clarified modules;
The file was addedsrc/Pure/General/codepoint.scala
The file was modified src/Pure/Admin/check_sources.scala (diff)
The file was modified src/Pure/General/word.scala (diff)
The file was modified src/Pure/Isar/document_structure.scala (diff)
The file was modified src/Pure/build-jars (diff)
The file was modified src/Tools/VSCode/src/line.scala (diff)
Changeset 64609:7cc4b49be1ea by wenzelm:
tuned;
The file was modified src/Pure/build-jars (diff)