Sun, 30 Jun 2024 15:32:39 +0200 lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:39 +0200] rev 81062
lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;
Sun, 30 Jun 2024 15:32:32 +0200 clarified PIDE/line range conversions;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:32 +0200] rev 81061
clarified PIDE/line range conversions;
Sun, 30 Jun 2024 15:32:26 +0200 lsp: refactored conversion from Decoration_List to JSON;
Thomas Lindae <thomas.lindae@in.tum.de> [Sun, 30 Jun 2024 15:32:26 +0200] rev 81060
lsp: refactored conversion from Decoration_List to JSON;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 tip