Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified caret offset; show output at end of file;
  2. tuned signature;
  3. discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
  4. tuned;
  5. misc tuning and simplification;
  6. misc tuning and simplification;
Changeset 65198:76cef38242d2 by wenzelm:
clarified caret offset;<br>show output at end of file;
The file was modified src/Tools/VSCode/src/document_model.scala (diff)
The file was modified src/Tools/VSCode/src/dynamic_output.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
Changeset 65197:8fada74d82be by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/line.scala (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/VSCode/src/vscode_resources.scala (diff)
Changeset 65196:e8760a98db78 by wenzelm:
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
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/General/utf8.scala (diff)
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/line.scala (diff)
The file was modified src/Pure/PIDE/text.scala (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/VSCode/src/vscode_rendering.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
Changeset 65195:ffab6f460a82 by wenzelm:
tuned;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/query_operation.scala (diff)
The file was modified src/Tools/VSCode/src/dynamic_output.scala (diff)
The file was modified src/Tools/jEdit/src/output_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/simplifier_trace_dockable.scala (diff)
Changeset 65194:6dabae94cf57 by wenzelm:
misc tuning and simplification;
The file was modified src/Tools/jEdit/src/output_dockable.scala (diff)
Changeset 65193:352d40b389ef by wenzelm:
misc tuning and simplification;
The file was modified src/Tools/VSCode/src/dynamic_output.scala (diff)