Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. maintain decorations for document (model) and update it for each editor (view);
  2. clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover); discontinued obsolete "hover_message" decoration;
  3. more robust;
  4. tuned;
  5. proper Text.Range.offside (NB: in Scala ~1 == -2);
  6. tuned;
  7. more general tooltips, with uniform info range handling;
  8. tuned;
  9. more generic colors;
  10. tuned whitespace;
  11. proper color;
  12. more generic colors;
Changeset 65135:158cba86140f by wenzelm:
maintain decorations for document (model) and update it for each editor (view);
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 65134:511bf19348d3 by wenzelm:
clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);<br>discontinued obsolete &quot;hover_message&quot; decoration;
The file was modified src/Tools/VSCode/extension/package.json (diff)
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
The file was modified src/Tools/VSCode/src/server.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)
Changeset 65133:41f80c6978bc by wenzelm:
more robust;
The file was modified src/Pure/PIDE/rendering.scala (diff)
Changeset 65132:60e7072b8dbe by wenzelm:
tuned;
The file was modified src/Pure/PIDE/text.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_rendering.scala (diff)
Changeset 65131:5d35f4bccfa7 by wenzelm:
proper Text.Range.offside (NB: in Scala ~1 == -2);
The file was modified src/Tools/jEdit/src/graphview_dockable.scala (diff)
Changeset 65130:695930882487 by wenzelm:
tuned;
The file was modified src/Pure/General/pretty.scala (diff)
The file was modified src/Tools/jEdit/src/isabelle_sidekick.scala (diff)
Changeset 65129:06a7c2d316cf by wenzelm:
more general tooltips, with uniform info range handling;
The file was modified src/Pure/PIDE/rendering.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 65128:93a1e3b1ede0 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 65127:ce8b8f979afd by wenzelm:
more generic colors;
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 65126:45ccb8ee3d08 by wenzelm:
tuned whitespace;
The file was modified src/Pure/PIDE/rendering.scala (diff)
Changeset 65125:bdd58b74c4a4 by wenzelm:
proper color;
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 65124:759c64c39a6f by wenzelm:
more generic colors;
The file was modified src/Pure/PIDE/rendering.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)