search

m-fleury / isabelle-emacs

Clone of isabelle, with LSP extensions in seperate branches
Other
24 stars 5 forks source link

display problem for BigOr #69

Closed gh-salt closed 1 year ago

gh-salt commented 1 year ago

MWE:

theory Test
  imports Propositional_Proof_Systems.Compactness
begin

  term \<open> BigOr L \<close>

end

in lsp-isar-output, I get: 

"bL"
  :: "'a formula"

where I expected:

"BigOr L"
  :: "'a formula"
m-fleury commented 1 year ago

The issue is due to the fact that the symbol is bold