[isabelle] Minor bug in output from "locale" with notation



In Isabelle 2017, if I load the theory:

theory Barf
imports Main
begin

  locale L =
  fixes X :: "'x ⇒ 'x ⇒ 'x" (infixr "⋅" 55)

end

and then put the mouse over the locale definition, I see the following
in the output window:

locale

L


fixes X :: "'x ⇒ 'x ⇒ 'x"   (infixl "⋅" 55)


That is, it seems to output the fixity incorrectly.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.