Diffusion Isabelle 908d8be90533

suppress irrelevant markup for VSCode;
908d8be90533
Actions

Tags

None

Subscribers

None

Description

suppress irrelevant markup for VSCode;

Details

Provenance

Authored on

Parents

rISABELLE93fb59c68052: tuned colors;

Branches

Unknown

Tags

Unknown

Event Timeline

makarius mentioned this in rISABELLE00399e5a6e50: proper argument --- amending 908d8be90533;.Dec 13 2020, 11:17 PM

Changes (6)

Path

Size

src/

Pure/

PIDE/

rendering.scala

Tools/

VSCode/

extension/

src/

src/

vscode_rendering.scala

jEdit/

src/

rich_text_area.scala

rISABELLE908d8be90533

src/Pure/PIDE/markup.scala

Loading...

src/Pure/PIDE/rendering.scala

Loading...

src/Tools/VSCode/extension/package.json

Loading...

src/Tools/VSCode/extension/src/decorations.ts

Loading...

src/Tools/VSCode/src/vscode_rendering.scala

Loading...

src/Tools/jEdit/src/rich_text_area.scala

Loading...