Re: [isabelle] 2014-RC1 issues



On 30.07.2014 10:26, Peter Lammich wrote:
> Here is a list of issues that I encountered with RC1:
And a completion-related one: In a string context in a ML-context,
symbol completion is enabled. So, changing

setup {*
  ML_Antiquotation.inline @{binding fundef} (Scan.succeed "raise Undefined")
*}

to

setup {*
  ML_Antiquotation.inline @{binding fundef} (Scan.succeed "fn _ => raise
Undefined")
*}

yields

setup {*
  ML_Antiquotation.inline @{binding fundef} (Scan.succeed "fn _ ⇒ raise
Undefined")
*}

instead with the default (immediate completion) settings.




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