Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. clarified module name;
  2. more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
  3. clarified module name;
  4. merged
  5. proper reset of column (amending 01e50039edc9);
  6. added option -T: text length encoding;
  7. more systematic text length wrt. encoding;
  8. tuned;
  9. more systematic text length;
  10. unused;
  11. proper counting of chars;
  12. tuned;
  13. clarified modules;
  14. clarified modules;
  15. tuned;
  16. merge
  17. generalized code (towards nonuniform datatypes)
Changeset 64623:83f012ce2567 by wenzelm:
clarified module name;
The file was addedsrc/Tools/VSCode/src/vscode_resources.scala
The file was modified src/Pure/build-jars (diff)
The file was modified src/Tools/VSCode/src/server.scala (diff)
The file was removedsrc/Tools/VSCode/src/uri_resources.scala
Changeset 64622:529bbb8977c7 by wenzelm:
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
The file was addedsrc/Pure/PIDE/rendering.scala
The file was addedsrc/Tools/VSCode/etc/options
The file was addedsrc/Tools/VSCode/src/vscode_rendering.scala
The file was modified etc/components (diff)
The file was modified src/Pure/build-jars (diff)
The file was modified src/Tools/VSCode/src/document_model.scala (diff)
The file was modified src/Tools/VSCode/src/server.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 64621:7116f2634e32 by wenzelm:
clarified module name;
The file was addedsrc/Tools/jEdit/src/jedit_rendering.scala
The file was modified src/Tools/jEdit/lib/Tools/jedit (diff)
The file was modified src/Tools/jEdit/src/bibtex_jedit.scala (diff)
The file was modified src/Tools/jEdit/src/completion_popup.scala (diff)
The file was modified src/Tools/jEdit/src/document_view.scala (diff)
The file was modified src/Tools/jEdit/src/fold_handling.scala (diff)
The file was modified src/Tools/jEdit/src/graphview_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_lib.scala (diff)
The file was modified src/Tools/jEdit/src/output_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
The file was modified src/Tools/jEdit/src/pretty_text_area.scala (diff)
The file was modified src/Tools/jEdit/src/pretty_tooltip.scala (diff)
The file was modified src/Tools/jEdit/src/rich_text_area.scala (diff)
The file was modified src/Tools/jEdit/src/spell_checker.scala (diff)
The file was modified src/Tools/jEdit/src/text_structure.scala (diff)
The file was modified src/Tools/jEdit/src/token_markup.scala (diff)
The file was removedsrc/Tools/jEdit/src/rendering.scala
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)
Changeset 64608:20ccca53dd73 by blanchet:
merge
Changeset 64607:20f3dbfe4b24 by blanchet:
generalized code (towards nonuniform datatypes)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML (diff)